T2Quotient — Mathlib

English

Every property P that holds for mk x for all x ∈ X also holds for every q ∈ T2Quotient X.

Русский

Любое свойство, которому удовлетворяют mk x для всех x, переносится на любой элемент T2Quotient X.

LaTeX

$$$ \\forall q:\\, T2Quotient X,\\ (\\forall x:X, P(T2Quotient.mk\\ x)) \\Rightarrow P(q)$$$

Lean4

/-- The largest T2 quotient of a topological space. This construction is left-adjoint to the
inclusion of T2 spaces into all topological spaces. -/
def T2Quotient :=
  Quotient (t2Setoid X)

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