liftNormedAddGroupHom_norm_le — Mathlib

English

For f, hf as above, and any c in NNReal, if ‖f‖ ≤ c, then ‖liftNormedAddGroupHom f hf‖ ≤ c.

Русский

Для mножителя f, hf, и любого c ∈ ℝ≥0, если ‖f‖ ≤ c, то ‖liftNormedAddGroupHom f hf‖ ≤ c.

LaTeX

$$$\\|\\mathrm{liftNormedAddGroupHom} f\\, hf\\| \\le c \\quad\\text{given } \\|f\\| \\le c$$

Lean4

theorem liftNormedAddGroupHom_norm_le {N : Type*} [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N)
    (hf : ∀ s, ‖s‖ = 0 → f s = 0) {c : ℝ≥0} (fb : ‖f‖ ≤ c) : ‖liftNormedAddGroupHom f hf‖ ≤ c :=
  (norm_liftNormedAddGroupHom_le f hf).trans fb

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