sup_orthogonal_of_hasOrthogonalProjection

English

If K has an orthogonal projection, then K and K⊥ span the entire space.

Русский

Если у K есть ортогональная проекция, тогда K и K⊥ порождают всё пространство.

LaTeX

$$$K \oplus K^{\perp} = E$$$

Lean4

/-- If `K` admits an orthogonal projection, then `K` and `Kᗮ` span the whole space. -/
theorem sup_orthogonal_of_hasOrthogonalProjection [K.HasOrthogonalProjection] : K ⊔ Kᗮ = ⊤ :=
  by
  convert Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection (le_top : K ≤ ⊤) using 2
  simp

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