Theorems · Definition · general topology

T2Quotient.lift

{X : Type u_3} →
  {Y : Type u_4} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → [T2Space Y] → {f : X → Y} → Continuous f → T2Quotient X → Y

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.

Defined in

Mathlib.Topology.Separation.Hausdorff

Cited by

5 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceT2Space