reflection_involutive — Mathlib

English

The reflection map is an involution; composing it with itself yields the identity map.

Русский

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

LaTeX

$$$$\mathrm{reflection}_s \circ \mathrm{reflection}_s = \mathrm{id}.$$$$

Lean4

/-- Reflection is involutive. -/
theorem reflection_involutive (s : AffineSubspace ℝ P) [Nonempty s] [s.direction.HasOrthogonalProjection] :
    Function.Involutive (reflection s) :=
  reflection_reflection s

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