range_starProjection — Mathlib

English

For a LinearIsometryEquiv f between E and E', the starProjection on the mapped subspace corresponds to the starProjection on the original via f and f^{-1}.

Русский

Для линейной изометрной эквивариантности f между E и E' проекция на отображение сохраняется через f и f^{-1}.

LaTeX

$$P_{(p.map f.toLinearMap)}^{*}(x) = f(P_p^{*}(f^{-1}(x))).$$

Lean4

@[simp]
theorem range_starProjection (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : LinearMap.range U.starProjection = U :=
  by
  ext x
  exact ⟨fun ⟨y, hy⟩ ↦ hy ▸ coe_mem (U.orthogonalProjection y), fun h ↦ ⟨x, starProjection_eq_self_iff.mpr h⟩⟩

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