Theorems · Definition · general topology

SeparationQuotient

(X : Type u_1) → [TopologicalSpace X] → Type u_1

The quotient of a topological space by its inseparableSetoid. Also called the Kolmogorov quotient. This quotient is guaranteed to be a T₀ space.

Defined in

Mathlib.Topology.Defs.Filter

Cited by

128 results in Mathlib

Foundations

Depth 30 from the axioms, rests on 190 definitions · uses propext, Quot.sound

Assumes

TopologicalSpace