Theorems · Theorem · general topology

regularSpace_TFAE

∀ (X : Type u) [inst : TopologicalSpace X],
  [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure s, Disjoint (nhdsSet s) (nhds x),
      ∀ (x : X) (s : Set X), Disjoint (nhdsSet s) (nhds x) ↔ x ∉ closure s,
      ∀ (x : X), ∀ s ∈ nhds x, ∃ t ∈ nhds x, IsClosed t ∧ t ⊆ s, ∀ (x : X), (nhds x).lift' closure ≤ nhds x,
      ∀ (x : X), (nhds x).lift' closure = nhds x].TFAE

Defined in

Mathlib.Topology.Separation.Regular

Cited by

6 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace