explicitCokernelDesc_norm_le_of_norm_le

English

If f ≫ g = 0 and ||g|| ≤ c, then ||explicitCokernelDesc w|| ≤ c.

Русский

Если f ≫ g = 0 и ||g|| ≤ c, тогда ||explicitCokernelDesc w|| ≤ c.

LaTeX

$$$\\\\|explicitCokernelDesc w\\\\| \\\\le c \\\\text{ whenever } \\\\|g\\\\| \\\\le c \\\\text{ and } (f \\\\gg g = 0).$$$

Lean4

theorem explicitCokernelDesc_norm_le_of_norm_le {X Y Z : SemiNormedGrp.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (w : f ≫ g = 0)
    (c : ℝ≥0) (h : ‖g‖ ≤ c) : ‖explicitCokernelDesc w‖ ≤ c :=
  NormedAddGroupHom.lift_norm_le _ _ _ h

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