starProjection_add_starProjection_orthogonal

English

If K has an orthogonal projection, then any w ∈ E splits as the sum of its projections onto K and onto the orthogonal complement of K.

Русский

Если у подпространства K есть ортогональная проекция, то любой вектор w ∈ E раскладывается на сумму проекций на K и на ортогональное дополнение K.

LaTeX

$$$ w = P_K(w) + P_{K^{\perp}}(w). $$$

Lean4

/-- If the orthogonal projection to `K` is well-defined, then a vector splits as the sum of its
orthogonal projections onto a complete submodule `K` and onto the orthogonal complement of `K`. -/
theorem starProjection_add_starProjection_orthogonal [K.HasOrthogonalProjection] (w : E) :
    K.starProjection w + Kᗮ.starProjection w = w := by simp

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