norm_lift_le — Mathlib

English

For hf characterizing vanishing on S, the lifted map satisfies ∥lift S f hf∥ ≤ ∥f∥.

Русский

Для hf, задающего нуль на S, лифт отображения удовлетворяет ∥lift S f hf∥ ≤ ∥f∥.

LaTeX

$$$\\|lift S f hf\\| \\le \\|f\\|$$$

Lean4

theorem norm_lift_le {N : Type*} [SeminormedAddCommGroup N] (S : AddSubgroup M) (f : NormedAddGroupHom M N)
    (hf : ∀ s ∈ S, f s = 0) : ‖lift S f hf‖ ≤ ‖f‖ :=
  opNorm_le_bound _ (norm_nonneg f)
    (norm_lift_apply_le f hf)
      -- TODO: deprecate?

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