lift_comp_incl — Mathlib

English

For any f, inclusion composed with the lift of f equals f: incl ∘ lift f = f.

Русский

для любого отображения f вертикальное включение, композиция с продолжением равна f: incl ∘ lift f = f.

LaTeX

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

Lean4

theorem lift_comp_incl {V W : SemiNormedGrp} [CompleteSpace W] [T0Space W] (f : V ⟶ W) :
    completion.incl ≫ completion.lift f = f :=
  ext <| NormedAddGroupHom.extension_coe _

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