midpoint_eq_iff — Mathlib

English

The midpoint equality with z is equivalent to the pointReflection relation: midpoint(R,x,y)=z iff pointReflection(R,z,x)=y.

Русский

Середина между x и y равна z тогда и только тогда, когда отражение точки z в x равно y.

LaTeX

$$$ \\operatorname{midpoint}(R,x,y) = z \\;\\iff\\; \\operatorname{pointReflection}(R,z)(x) = y $$$

Lean4

theorem midpoint_eq_iff {x y z : P} : midpoint R x y = z ↔ pointReflection R z x = y :=
  eq_comm.trans
    ((injective_pointReflection_left_of_module R x).eq_iff' (AffineEquiv.pointReflection_midpoint_left x y)).symm

Похожие утверждения