starProjection_orthogonal_val — Mathlib

English

The projection onto the orthogonal complement K^⊥ equals the difference between the identity and the projection onto K: P_{K^⊥}(u) = u − P_K(u).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem starProjection_orthogonal_val (u : E) : Kᗮ.starProjection u = u - K.starProjection u :=
  eq_starProjection_of_mem_orthogonal' (sub_starProjection_mem_orthogonal _)
      (K.le_orthogonal_orthogonal (K.orthogonalProjection u).2) <|
    (sub_add_cancel _ _).symm

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