English
Projection under a linear isometry equivalence: starProjection_map_apply for Equivalence; the mapped subspace starProjection equals the mapped projection.
Русский
Проекция через эквивариантную изометрию: starProjection_map_apply для эквивалентности; отображение сохранено.
LaTeX
$$starProjection_map_apply (f, p, x) = ...$$
Lean4
/-- Orthogonal projection onto the `Submodule.map` of a subspace. -/
theorem starProjection_map_apply {E E' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E]
[InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (p : Submodule 𝕜 E) [p.HasOrthogonalProjection] (x : E') :
(p.map (f.toLinearEquiv : E →ₗ[𝕜] E')).starProjection x = f (p.starProjection (f.symm x)) := by
simpa only [f.coe_toLinearIsometry, f.apply_symm_apply] using
(f.toLinearIsometry.map_starProjection' p (f.symm x)).symm
