explicitCokernelDesc_normNoninc — Mathlib

English

If g.hom is NormNoninc, then (explicitCokernelDesc w).hom is NormNoninc.

Русский

Если g.hom NormNoninc, то (explicitCokernelDesc w).hom NormNoninc.

LaTeX

$$$(\\\\mathrm{g}.\\\\mathrm{hom}).\\\\mathrm{NormNoninc} \\\\Rightarrow (\\\\mathrm{explicitCokernelDesc}(w)).\\\\mathrm{hom}.\\\\mathrm{NormNoninc}.$$$

Lean4

theorem explicitCokernelDesc_normNoninc {X Y Z : SemiNormedGrp.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} {cond : f ≫ g = 0}
    (hg : g.hom.NormNoninc) : (explicitCokernelDesc cond).hom.NormNoninc :=
  by
  refine NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.2 ?_
  rw [← NNReal.coe_one]
  exact explicitCokernelDesc_norm_le_of_norm_le cond 1 (NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.1 hg)

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