pointReflection_involutive — Mathlib

English

For each x ∈ P, the map y ↦ pointReflection 𝕜 x y is an involution on P; applying it twice yields the identity map.

Русский

Для каждого x ∈ P отображение y ↦ pointReflection 𝕜 x y является инволюторным на P; применение два раза возвращает исходное значение.

LaTeX

$$Function.Involutive (\( y \mapsto \operatorname{pointReflection}_{\mathbb{k}}(x)(y))$$

Lean4

theorem pointReflection_involutive (x : P) : Function.Involutive (pointReflection 𝕜 x) :=
  Equiv.pointReflection_involutive x

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