closedComplemented_iff_isClosed_exists_isClosed_isCompl

English

A subspace p is ClosedComplemented if and only if p is closed as a subset and there exists a closed subspace q with p ⊕ q = E.

Русский

Подпространство p является ClosedComplemented тогда и только тогда, когда оно замкнуто как множество и существует замкнутое q такое, что p ⊕ q = E.

LaTeX

$$$p.ClosedComplemented \iff (IsClosed(p) \wedge \exists q\, IsClosed(q) \wedge IsCompl(p,q))$$$

Lean4

theorem closedComplemented_iff_isClosed_exists_isClosed_isCompl :
    p.ClosedComplemented ↔ IsClosed (p : Set E) ∧ ∃ q : Submodule 𝕜 E, IsClosed (q : Set E) ∧ IsCompl p q :=
  ⟨fun h => ⟨h.isClosed, h.exists_isClosed_isCompl⟩, fun ⟨hp, ⟨_, hq, hpq⟩⟩ => .of_isCompl_isClosed hpq hp hq⟩

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