closedComplemented_bot — Mathlib

English

In a topological module M, the zero submodule ⊥ is closed complemented (i.e., there exists a continuous projection onto ⊥ along a closed complement).

Русский

В топологическом модуле M нулевое подпро пространство ⊥ замкнуто дополнено (существует непрерывная проекция на ⊥ вдоль замкнутого дополнения).

LaTeX

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

Lean4

@[simp]
theorem closedComplemented_bot : ClosedComplemented (⊥ : Submodule R M) :=
  ⟨0, fun x => by simp only [zero_apply, eq_zero_of_bot_submodule x]⟩

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