English
For a linear isometry f: E → E' and a subspace K ⊆ E, the reflection in the mapped subspace equals applying f to the reflection in K of the preimage.
Русский
Для линейного изометрического отображения f: E → E' и подпомешного пространства K ⊆ E отражение в отображённом подппространстве равно применению f к отражению в K от образа x под f^{-1}.
LaTeX
$$$\mathrm{reflection}(K.map(f)) (x) = f\big(\mathrm{reflection}(K)(f^{-1}(x))\big)$$$
Lean4
/-- Reflection in the `Submodule.map` of a subspace. -/
theorem reflection_map_apply {E E' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E]
[InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (x : E') :
reflection (K.map (f.toLinearEquiv : E →ₗ[𝕜] E')) x = f (K.reflection (f.symm x)) := by
simp [two_smul, reflection_apply, starProjection_map_apply f K x]
