English
Let f be a linear isometry and p a submodule with HasOrthogonalProjection; then f.map_starProjection p x expresses how starProjection behaves under f.
Русский
Пусть f — линейная изометрия; тогда map_starProjection(p, x) описывает поведение starProjection при применении f.
LaTeX
$$f.map_starProjection p x = ? (see formal statement).$$
Lean4
theorem _root_.LinearIsometry.map_starProjection {E E' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E']
[InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E'] (f : E →ₗᵢ[𝕜] E') (p : Submodule 𝕜 E) [p.HasOrthogonalProjection]
[(p.map f.toLinearMap).HasOrthogonalProjection] (x : E) :
f (p.starProjection x) = (p.map f.toLinearMap).starProjection (f x) :=
by
refine (eq_starProjection_of_mem_of_inner_eq_zero ?_ fun y hy => ?_).symm
· refine Submodule.apply_coe_mem_map _ _
rcases hy with ⟨x', hx', rfl : f x' = y⟩
rw [← f.map_sub, f.inner_map_map, starProjection_inner_eq_zero x x' hx']
