reflection_symm — Mathlib

English

The inverse of the reflection transformation is the reflection itself.

Русский

Обратное отображение отражения — само отражение.

LaTeX

$$$$ (\mathrm{reflection}_s)^{-1} = \mathrm{reflection}_s. $$$$

Lean4

/-- Reflection is its own inverse. -/
@[simp]
theorem reflection_symm (s : AffineSubspace ℝ P) [Nonempty s] [s.direction.HasOrthogonalProjection] :
    (reflection s).symm = reflection s := by
  ext
  rw [← (reflection s).injective.eq_iff]
  simp

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