norm_lift_apply_le — Mathlib

English

For any f: M → N that vanishes on S, the lift of f has norm bounded by ‖f‖ times ‖x‖ on the quotient.

Русский

Для любого отображения f: M → N, нулевого на S, нормa лифта f не превышает ‖f‖ · ‖x‖ на фактор‑модуле.

LaTeX

$$$‖lift\, S\, f\, hf\, x‖ \\le ‖f‖ \\cdot ‖x‖$$$

Lean4

theorem _root_.QuotientAddGroup.norm_lift_apply_le {S : AddSubgroup M} (f : NormedAddGroupHom M N)
    (hf : ∀ x ∈ S, f x = 0) (x : M ⧸ S) : ‖lift S f.toAddMonoidHom hf x‖ ≤ ‖f‖ * ‖x‖ := by
  cases (norm_nonneg f).eq_or_lt' with
  | inl h =>
    rcases mk_surjective x with ⟨x, rfl⟩
    simpa [h] using le_opNorm f x
  | inr h =>
    rw [← not_lt, ← lt_div_iff₀' h, norm_lt_iff]
    rintro ⟨x, rfl, hx⟩
    exact ((lt_div_iff₀' h).1 hx).not_ge (le_opNorm f x)

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