Theorems · Theorem · general topology

T2Space.t2

∀ {X : Type u} {inst : TopologicalSpace X} [self : T2Space X],
  Pairwise fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Every two points in a Hausdorff space admit disjoint open neighbourhoods.

Defined in

Mathlib.Topology.Separation.Hausdorff

Cited by

1 results in Mathlib

Foundations

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

Assumes

T2Space