English
As above: induction on T2Quotient X.
Русский
Как выше: индукция по T2Quotient X.
LaTeX
$$$ \\forall q:\\, T2Quotient X,\\ (\\forall x:X, P(T2Quotient.mk x)) \\Rightarrow P(q)$$$
Lean4
/-- The universal property of the largest T2 quotient of a topological space `X`: any continuous
map from `X` to a T2 space `Y` uniquely factors through `T2Quotient X`. This declaration builds the
factored map. Its continuity is `T2Quotient.continuous_lift`, the fact that it indeed factors the
original map is `T2Quotient.lift_mk` and uniqueness is `T2Quotient.unique_lift`. -/
def lift {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) :
T2Quotient X → Y :=
Quotient.lift f (T2Quotient.compatible hf)
