pointReflection_involutive — Mathlib

English

For every x ∈ P, the map (pointReflection x) is an involution on P; applying it twice yields the identity on P.

Русский

Для любого x ∈ P отображение (pointReflection x) является инволюцией на P; при повторном применении получается тождественное отображение на P.

LaTeX

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

Lean4

theorem pointReflection_involutive (x : P) : Involutive (pointReflection x : P → P) := fun y =>
  (Equiv.apply_eq_iff_eq_symm_apply _).2 <| by rw [pointReflection_symm]

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