liftNormedAddGroupHom_normNoninc — Mathlib

English

If f is NormNoninc, then liftNormedAddGroupHom f hf is NormNoninc.

Русский

Если f нормонеподнимается, то liftNormedAddGroupHom f hf также нормонеподнимается.

LaTeX

$$$ (\\mathrm{liftNormedAddGroupHom} f\\, hf).\\mathrm{NormNoninc} \\\\Rightarrow \\text{(preserved)} $$$

Lean4

theorem liftNormedAddGroupHom_normNoninc {N : Type*} [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N)
    (hf : ∀ s, ‖s‖ = 0 → f s = 0) (fb : f.NormNoninc) : (liftNormedAddGroupHom f hf).NormNoninc := fun x =>
  by
  have fb' : ‖f‖ ≤ 1 := NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.mp fb
  exact le_trans (norm_liftNormedAddGroupHom_apply_le f hf x) (mul_le_of_le_one_left (norm_nonneg x) fb')

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