reflection_map — Mathlib

English

The reflection in the mapped subspace equals the conjugation of the original reflection by the isometry f.

Русский

Отражение в отображённом подппространстве эквивалентно сопряжению исходного отражения изометрией f.

LaTeX

$$$\mathrm{reflection}(K.map f) = f^{-1} \circ (K.reflection) \circ f$$$

Lean4

/-- Reflection in the `Submodule.map` of a subspace. -/
theorem reflection_map {E E' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E]
    [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] :
    reflection (K.map (f.toLinearEquiv : E →ₗ[𝕜] E')) = f.symm.trans (K.reflection.trans f) :=
  LinearIsometryEquiv.ext <| reflection_map_apply f K

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