isClosed_or_dense_of_isCoatom — Mathlib

English

A maximal proper subspace of a topological module is either closed or dense.

Русский

Максимальное правильное подпространство топологического модуля либо замкнуто, либо плотное.

LaTeX

$$$IsCoatom(S) \Rightarrow (IsClosed(S) \lor Dense(S))$$$

Lean4

/-- A maximal proper subspace of a topological module (i.e a `Submodule` satisfying `IsCoatom`)
is either closed or dense. -/
theorem isClosed_or_dense_of_isCoatom (s : Submodule R M) (hs : IsCoatom s) :
    IsClosed (s : Set M) ∨ Dense (s : Set M) :=
  by
  refine (hs.le_iff.mp s.le_topologicalClosure).symm.imp ?_ dense_iff_topologicalClosure_eq_top.mpr
  exact fun h ↦ h ▸ isClosed_closure

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