norm_liftNormedAddGroupHom_le — Mathlib

English

For any f and hf as above, we have ‖liftNormedAddGroupHom f hf‖ ≤ ‖f‖.

Русский

Для любого f и hf, выполняется ‖liftNormedAddGroupHom f hf‖ ≤ ‖f‖.

LaTeX

$$$\\|\\mathrm{liftNormedAddGroupHom} f\\, hf\\| \\leq \\|f\\|$$$

Lean4

/-- For a norm-continuous group homomorphism `f`, its lift to the separation quotient
is bounded by the norm of `f`. -/
theorem norm_liftNormedAddGroupHom_le {N : Type*} [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N)
    (hf : ∀ s, ‖s‖ = 0 → f s = 0) : ‖liftNormedAddGroupHom f hf‖ ≤ ‖f‖ :=
  NormedAddGroupHom.opNorm_le_bound _ (norm_nonneg f) (norm_liftNormedAddGroupHom_apply_le f hf)

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