mem_closure_iff — Mathlib

English

Let B be a topological basis. For any a ∈ α and any s ⊆ α, a lies in the closure of s if and only if every basis neighborhood of a intersects s.

Русский

Пусть B — топологический базис. Точка a принадлежит замыканию множества s тогда и только тогда, когда каждый базисный окрестность a пересекает s.

LaTeX

$$$a \in \overline{s} \iff \forall o \in B,\ a \in o \to (o \cap s) \neq \emptyset.$$$

Lean4

/-- A point `a` is in the closure of `s` iff all basis sets containing `a` intersect `s`. -/
theorem mem_closure_iff {b : Set (Set α)} (hb : IsTopologicalBasis b) {s : Set α} {a : α} :
    a ∈ closure s ↔ ∀ o ∈ b, a ∈ o → (o ∩ s).Nonempty :=
  (mem_closure_iff_nhds_basis' hb.nhds_hasBasis).trans <| by simp only [and_imp]

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