unique_lift — Mathlib

English

Any map g: T2Quotient X → Y that composes with mk to f must equal lift hf.

Русский

Любое отображение g: T2Quotient X → Y, композиция с mk даёт f, то есть g = lift hf.

LaTeX

$$$ \\forall f: X \\to Y\\, (hf: Continuous f)\\, \\forall g:\\, T2Quotient X \\to Y,\\ g \\circ mk = f \\Rightarrow g = lift hf$$$

Lean4

theorem unique_lift {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f)
    {g : T2Quotient X → Y} (hfg : g ∘ mk = f) : g = lift hf :=
  by
  apply surjective_mk X |>.right_cancellable |>.mp <| funext _
  simp [← hfg]

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