closedComplemented_top — Mathlib

English

The top submodule ⊤ is closed complemented; there exists a continuous projection onto ⊤.

Русский

Верхнее подпро пространство ⊤ замкнуто дополнено; существует непрерывная проекция на ⊤.

LaTeX

$$$\exists p: M \to_L[R] M\; (\operatorname{range}(p) = M \land p^2 = p)$$$

Lean4

@[simp]
theorem closedComplemented_top : ClosedComplemented (⊤ : Submodule R M) :=
  ⟨(ContinuousLinearMap.id R M).codRestrict ⊤ fun _x => trivial, fun x => Subtype.ext_iff.2 <| by simp⟩

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