Theorems · Inductive type · general topology

T0Space

(X : Type u) → [TopologicalSpace X] → Prop

A T₀ space, also known as a Kolmogorov space, is a topological space such that for every pair x ≠ y, there is an open set containing one but not the other. We formulate the definition in terms of the Inseparable relation.

Defined in

Mathlib.Topology.Separation.Basic

Cited by

179 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

TopologicalSpace