dense_iff — Mathlib

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⟩⟩

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