lift_unique — Mathlib

English

If incl ≫ g = f for some g, then g = lift f.

Русский

Если incl ≫ g = f, тогда g = lift f.

LaTeX

$$$\\\\mathrm{incl} \\\\circ g = f \\\\Rightarrow \\\\ g = \\\\mathrm{lift}(f).$$$

Lean4

theorem lift_unique {V W : SemiNormedGrp} [CompleteSpace W] [T0Space W] (f : V ⟶ W) (g : completion.obj V ⟶ W) :
    completion.incl ≫ g = f → g = completion.lift f := fun h =>
  SemiNormedGrp.hom_ext (NormedAddGroupHom.extension_unique _ fun v => ((SemiNormedGrp.ext_iff.1 h) v).symm).symm

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