lift_normNoninc — Mathlib

English

The same bound as above holds in the normalized/lifted setting: ∥lift S f hf∥ ≤ ∥f∥.

Русский

Для лифта в нормированном виде верно: ∥lift S f hf∥ ≤ ∥f∥.

LaTeX

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

Lean4

theorem lift_normNoninc {N : Type*} [SeminormedAddCommGroup N] (S : AddSubgroup M) (f : NormedAddGroupHom M N)
    (hf : ∀ s ∈ S, f s = 0) (fb : f.NormNoninc) : (lift S f hf).NormNoninc := fun x =>
  by
  have fb' : ‖f‖ ≤ (1 : ℝ≥0) := NormNoninc.normNoninc_iff_norm_le_one.mp fb
  simpa using le_of_opNorm_le _ (f.lift_norm_le _ _ fb') _

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