SeparationQuotient — Mathlib

English

The Separation Quotient is the quotient of a topological space by its inseparable setoid; this quotient is a T0 space.

Русский

Разделение пространства — это фактор-пространство по отношению инсемпарабельной эквивалентности; полученное пространство является T0.

LaTeX

$$SeparationQuotient(X) = X / inseparableSetoid(X)$$

Lean4

/-- The quotient of a topological space by its `inseparableSetoid`.
This quotient is guaranteed to be a T₀ space. -/
def SeparationQuotient :=
  Quotient (inseparableSetoid X)

Похожие утверждения