orthogonalProjection_orthogonal — Mathlib

English

The orthogonal projection onto K⊥ equals u minus its projection onto K: P_{K⊥}(u) = u − P_K(u).

Русский

Ортогональная проекция на K⊥ равна u минус проекция на K: P_{K⊥}(u) = u − P_K(u).

LaTeX

$$P_{K^{\perp}}(u) = u - P_K(u).$$

Lean4

theorem orthogonalProjection_orthogonal (u : E) :
    Kᗮ.orthogonalProjection u = ⟨u - K.starProjection u, sub_starProjection_mem_orthogonal _⟩ :=
  Subtype.eq <| starProjection_orthogonal_val _

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