of_isCompl_isClosed — Mathlib

English

If p and q are complementary subspaces of E and the ambient space is complete, then p is ClosedComplemented provided p and q are closed.

Русский

Если p и q — дополнение пространства E, а E завершено, то p является Submodule.ClosedComplemented при условии, что p и q замкнуты.

LaTeX

$$p.ClosedComplemented$$

Lean4

theorem of_isCompl_isClosed (h : IsCompl p q) (hp : IsClosed (p : Set E)) (hq : IsClosed (q : Set E)) :
    p.ClosedComplemented :=
  ⟨p.linearProjOfClosedCompl q h hp hq, Submodule.linearProjOfIsCompl_apply_left h⟩

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