Theorems · Theorem · general topology

regularSpace_generateFrom

∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set (Set X)},
  inst = TopologicalSpace.generateFrom s → (RegularSpace X ↔ ∀ t ∈ s, ∀ a ∈ t, Disjoint (nhdsSet tᶜ) (nhds a))

Given a subbasis s, it is enough to check the condition of regularity for complements of sets in s.

Defined in

Mathlib.Topology.Separation.Regular

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace