Projects.AP.Symmetry.Translation

source

def AP.translate (offset : PointZ) :

sys.Symmetry

Equations

AP.translate offset = AP.mkSym { toFun := fun (x : PointZ) => x + offset, invFun := fun (x : PointZ) => x - offset, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

theorem AP.translate.cnd_initial_fs_iff {offset : PointZ} {s : State} :

sys.Initial ((translate offset).fs s) ↔ sys.Initial s

source

theorem AP.translate.cnd_tr_eq {offset : PointZ} {s : State} {p : PointZ} :

sys.tr s p = Option.map (⇑(translate offset).fs') (sys.tr ((translate offset).fs s) ((translate offset).ft p))

source

@[simp]

instance AP.instWFStatePointZTranslate {offset : PointZ} :

(translate offset).WF

source

@[simp]

instance AP.instBasicSymTranslate {offset : PointZ} :

BasicSym (translate offset)

source

@[simp]

theorem AP.translate_ft_x {p offset : PointZ} :

((translate offset).ft p).x = p.x + offset.x

source

@[simp]

theorem AP.translate_ft_y {p offset : PointZ} :

((translate offset).ft p).y = p.y + offset.y

source

@[simp]

theorem AP.translate_ft'_x {p offset : PointZ} :

((translate offset).ft' p).x = p.x - offset.x

source

@[simp]

theorem AP.translate_ft'_y {p offset : PointZ} :

((translate offset).ft' p).y = p.y - offset.y

source

@[simp]

theorem AP.translate_ft_mk {offset : PointZ} {x y : ℤ} :

(translate offset).ft { x := x, y := y } = { x := x + offset.x, y := y + offset.y }

source

@[simp]

theorem AP.translate_ft_mk' {offset : PointZ} {x y : ℤ} :

(translate offset).ft' { x := x, y := y } = { x := x - offset.x, y := y - offset.y }

source

@[simp]

theorem AP.translate_dist_translate {offset p₁ p₂ : PointZ} :

Point.dist ((translate offset).ft p₁) ((translate offset).ft p₂) = Point.dist p₁ p₂

source

@[simp]

theorem AP.translate_dist_translate' {offset p₁ p₂ : PointZ} :

Point.dist ((translate offset).ft' p₁) ((translate offset).ft' p₂) = Point.dist p₁ p₂