map_normNoninc — Mathlib

English

If a map f: V → W has NormNoninc, then the induced map on completions has NormNoninc.

Русский

Если отображение f: V → W нормонереступает, то индуцированное отображение на завершениях тоже нормонейтрально не увеличивает норму.

LaTeX

$$$\\\\big( \\\\mathrm{completion.map}(f) \\\\big).\\\\mathrm{hom}.\\\\mathrm{NormNoninc}.$$$

Lean4

theorem map_normNoninc {V W : SemiNormedGrp} {f : V ⟶ W} (hf : f.hom.NormNoninc) : (completion.map f).hom.NormNoninc :=
  NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.2 <|
    (NormedAddGroupHom.norm_completion f.hom).le.trans <| NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.1 hf

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