starProjection_comp_starProjection_of_le

English

If ||v|| = 1, then (𝕜 ∙ v).starProjection w = ⟨v,w⟩ v.

Русский

Если ||v|| = 1, то звездная проекция на span{v} равна ⟨v,w⟩ v.

LaTeX

$$$ (\|v\| = 1) \Rightarrow ( (\mathbb{K} \cdot v).starProjection(w) = \langle v,w\rangle \; v ) $$$

Lean4

theorem starProjection_comp_starProjection_of_le {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection]
    [V.HasOrthogonalProjection] (h : U ≤ V) : U.starProjection ∘L V.starProjection = U.starProjection :=
  ContinuousLinearMap.ext fun _ => by
    nth_rw 1 [starProjection]
    simp [orthogonalProjection_starProjection_of_le h]

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