orthogonalProjection_starProjection_of_le

English

The starProjection of w onto span{v} equals ⟨v,w⟩/⟨v,v⟩ times v (for v ≠ 0).

Русский

Звёздная проекция w на span{v} равна ⟨v,w⟩/⟨v,v⟩ умножить на v (для v ≠ 0).

LaTeX

$$$ (\mathrm{starProjection}_{\mathbb{K}v})(w) = \dfrac{\langle v,w\rangle}{\langle v,v\rangle} \; v \quad (v \neq 0) $$$

Lean4

/-- If `U ≤ V`, then projecting on `V` and then on `U` is the same as projecting on `U`. -/
theorem orthogonalProjection_starProjection_of_le {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection]
    [V.HasOrthogonalProjection] (h : U ≤ V) (x : E) :
    U.orthogonalProjection (V.starProjection x) = U.orthogonalProjection x :=
  Eq.symm <| by
    simpa only [sub_eq_zero, map_sub] using
      orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero
        (Submodule.orthogonal_le h (sub_starProjection_mem_orthogonal x))

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