mk — Mathlib · SciLib

English

The map from a space to its largest T2 quotient is the natural quotient map.

Русский

Отображение пространства в его наибольший T2-предельник является естественным факторизационным отображением.

LaTeX

$$$ mk : X \\to T2Quotient X$ is the quotient map associated to t2Setoid X.$$

Lean4

/-- The map from a topological space to its largest T2 quotient. -/
def mk : X → T2Quotient X :=
  Quotient.mk (t2Setoid X)

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