pointReflection_symm — Mathlib

English

The point reflection about x is an involution; applying it twice yields the identity.

Русский

Отражение точки относительно x является инвольюцией; применение дважды дает тождественное отображение.

LaTeX

$$({\mathrm{pointReflection}(x)})^2 = \mathrm{id}_P$$

Lean4

@[simp]
theorem pointReflection_symm (x : P) : (pointReflection x).symm = pointReflection x :=
  ext <| by simp [pointReflection]

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