isCompl_orthogonal_of_hasOrthogonalProjection

English

If K admits an orthogonal projection, then K and K⊥ are complementary subspaces.

Русский

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

LaTeX

$$IsCompl K K^{\perp}$$

Lean4

/-- If `K` admits an orthogonal projection, `K` and `Kᗮ` are complements of each other. -/
theorem isCompl_orthogonal_of_hasOrthogonalProjection [K.HasOrthogonalProjection] : IsCompl K Kᗮ :=
  ⟨K.orthogonal_disjoint, codisjoint_iff.2 Submodule.sup_orthogonal_of_hasOrthogonalProjection⟩

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