exists_isClosed_isCompl — Mathlib

English

From a non-trivial closed complemented submodule, there exists a complement q that is closed.

Русский

Из замкнуто дополненного подмодуля существует дополнение q, которое также замкнуто.

LaTeX

$$$$ \exists q \; IsClosed(q) \land IsCompl(p,q). $$$$

Lean4

theorem exists_isClosed_isCompl {p : Submodule R M} [T1Space p] (h : ClosedComplemented p) :
    ∃ q : Submodule R M, IsClosed (q : Set M) ∧ IsCompl p q :=
  Exists.elim h fun f hf => ⟨ker f, isClosed_ker f, LinearMap.isCompl_of_proj hf⟩

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