def EuclidGeom.pt_flip {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (O : P) : P

Equations

• EuclidGeom.pt_flip A O = EuclidGeom.Vec.mkPtPt A O +ᵥ O

theorem EuclidGeom.pt_flip_symm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {O : P} (h : B = EuclidGeom.pt_flip A O) : A = EuclidGeom.pt_flip B O

theorem EuclidGeom.pt_flip_vec_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {O : P} (h : B = EuclidGeom.pt_flip A O) : EuclidGeom.Vec.mkPtPt A O = EuclidGeom.Vec.mkPtPt O B

theorem EuclidGeom.pt_flip_vec_eq_half_vec {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {O : P} (h : B = EuclidGeom.pt_flip A O) : EuclidGeom.Vec.mkPtPt A O = (1 / 2) • EuclidGeom.Vec.mkPtPt A B