English
Let B be a topological basis. A subset s is dense in α if and only if every nonempty basis element o ∈ B meets s.
Русский
Пусть B — топологический базис. Образование s плотным подмножеством в α эквивалентно тому, что каждое непустое базисное множество o ∈ B пересекает s.
LaTeX
$$$\text{Dense}(s) \iff \forall o \in B,\ o \neq \emptyset \to (o \cap s) \neq \emptyset.$$$
Lean4
/-- A set is dense iff it has non-trivial intersection with all basis sets. -/
theorem dense_iff {b : Set (Set α)} (hb : IsTopologicalBasis b) {s : Set α} :
Dense s ↔ ∀ o ∈ b, Set.Nonempty o → (o ∩ s).Nonempty :=
by
simp only [Dense, hb.mem_closure_iff]
exact ⟨fun h o hb ⟨a, ha⟩ => h a o hb ha, fun h a o hb ha => h o hb ⟨a, ha⟩⟩