def AP.flipH : sys.Symmetry

Equations

• AP.flipH = AP.mkSym { toFun := fun (p : PointZ) => { x := -p.x, y := p.y }, invFun := fun (p : PointZ) => { x := -p.x, y := p.y }, left_inv := AP.flipH._proof_1, right_inv := AP.flipH._proof_1 }

def AP.flipV : sys.Symmetry

Equations

• AP.flipV = AP.mkSym { toFun := fun (p : PointZ) => { x := p.x, y := -p.y }, invFun := fun (p : PointZ) => { x := p.x, y := -p.y }, left_inv := AP.flipV._proof_1, right_inv := AP.flipV._proof_1 }

theorem AP.flipH.cnd_initial_fs_iff {s : State} : sys.Initial (flipH.fs s) ↔ sys.Initial s

theorem AP.flipV.cnd_initial_fs_iff {s : State} : sys.Initial (flipV.fs s) ↔ sys.Initial s

theorem AP.flipH.cnd_tr_eq {s : State} {p : PointZ} : sys.tr s p = Option.map (⇑flipH.fs') (sys.tr (flipH.fs s) (flipH.ft p))

theorem AP.flipV.cnd_tr_eq {s : State} {p : PointZ} : sys.tr s p = Option.map (⇑flipV.fs') (sys.tr (flipV.fs s) (flipV.ft p))

@[simp]

instance AP.instWFStatePointZFlipH : flipH.WF

@[simp]

instance AP.instWFStatePointZFlipV : flipV.WF

@[simp]

theorem AP.flipH_ft_x {p : PointZ} : (flipH.ft p).x = -p.x

@[simp]

theorem AP.flipH_ft_y {p : PointZ} : (flipH.ft p).y = p.y

@[simp]

theorem AP.flipH_ft'_x {p : PointZ} : (flipH.ft' p).x = -p.x

@[simp]

theorem AP.flipH_ft'_y {p : PointZ} : (flipH.ft' p).y = p.y

@[simp]

theorem AP.flipV_ft_x {p : PointZ} : (flipV.ft p).x = p.x

@[simp]

theorem AP.flipV_ft_y {p : PointZ} : (flipV.ft p).y = -p.y

@[simp]

theorem AP.flipV_ft'_x {p : PointZ} : (flipV.ft' p).x = p.x

@[simp]

theorem AP.flipV_ft'_y {p : PointZ} : (flipV.ft' p).y = -p.y

@[simp]

theorem AP.flipH_dist_flipH {p₁ p₂ : PointZ} : Point.dist (flipH.ft p₁) (flipH.ft p₂) = Point.dist p₁ p₂

@[simp]

theorem AP.flipH_dist_flipH' {p₁ p₂ : PointZ} : Point.dist (flipH.ft' p₁) (flipH.ft' p₂) = Point.dist p₁ p₂

@[simp]

theorem AP.flipV_dist_flipV {p₁ p₂ : PointZ} : Point.dist (flipV.ft p₁) (flipV.ft p₂) = Point.dist p₁ p₂

@[simp]

theorem AP.flipV_dist_flipV' {p₁ p₂ : PointZ} : Point.dist (flipV.ft' p₁) (flipV.ft' p₂) = Point.dist p₁ p₂

@[simp]

instance AP.instBasicSymFlipH : BasicSym flipH

@[simp]

instance AP.instBasicSymFlipV : BasicSym flipV

theorem AP.inv_flipH : flipH⁻¹ = flipH

theorem AP.inv_flipV : flipV⁻¹ = flipV

instance AP.instSelfInverseStatePointZFlipH : flipH.SelfInverse

instance AP.instSelfInverseStatePointZFlipV : flipV.SelfInverse

@[simp]

theorem AP.flipH_ft_mk {x y : ℤ} : flipH.ft { x := x, y := y } = { x := -x, y := y }

@[simp]

theorem AP.flipV_ft_mk {x y : ℤ} : flipV.ft { x := x, y := y } = { x := x, y := -y }

@[simp]

theorem AP.flipH_mul_flipV : flipH * flipV = rot180

@[simp]

theorem AP.flipV_mul_flipH : flipV * flipH = rot180

@[simp]

theorem AP.flipH_mul_rot180 : flipH * rot180 = flipV

@[simp]

theorem AP.rot180_mul_flipH : rot180 * flipH = flipV

@[simp]

theorem AP.flipV_mul_rot180 : flipV * rot180 = flipH

@[simp]

theorem AP.rot180_mul_flipV : rot180 * flipV = flipH

@[simp]

theorem AP.flipH_ft_flipV_ft {p : PointZ} : flipH.ft (flipV.ft p) = rot180.ft p

@[simp]

theorem AP.flipV_ft_flipH_ft {p : PointZ} : flipV.ft (flipH.ft p) = rot180.ft p

@[simp]

theorem AP.flipH_ft_rot180_ft {p : PointZ} : flipH.ft (rot180.ft p) = flipV.ft p

@[simp]

theorem AP.rot180_ft_flipH_ft {p : PointZ} : rot180.ft (flipH.ft p) = flipV.ft p

@[simp]

theorem AP.flipV_ft_rot180_ft {p : PointZ} : flipV.ft (rot180.ft p) = flipH.ft p

@[simp]

theorem AP.rot180_ft_flipV_ft {p : PointZ} : rot180.ft (flipV.ft p) = flipH.ft p