reflection_trans_reflection — Mathlib

English

Another articulation of involutivity of reflection: reflection is its own inverse under the HasOrthogonalProjection setting.

Русский

Ещё одно выражение инволютности отражения: отражение есть собственная обратная при наличии OrthogonalProjection.

LaTeX

$$$\\text{reflection\_involutive}$$$

Lean4

/-- Reflection is involutive. -/
@[simp]
theorem reflection_trans_reflection : K.reflection.trans K.reflection = LinearIsometryEquiv.refl 𝕜 E :=
  LinearIsometryEquiv.ext <| reflection_involutive K

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