dense_iff_topologicalClosure_eq_top

English

A subspace is dense iff its topological closure equals the whole space.

Русский

Подпространство плотное тогда и только тогда, когда его топологическое замыкание совпадает с всем пространством.

LaTeX

$$$\text{Dense}(S) \iff S.topologicalClosure = \top$$$

Lean4

/-- A subspace is dense iff its topological closure is the entire space. -/
theorem dense_iff_topologicalClosure_eq_top {s : Submodule R M} : Dense (s : Set M) ↔ s.topologicalClosure = ⊤ :=
  by
  rw [← SetLike.coe_set_eq, dense_iff_closure_eq]
  simp

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