opNorm_le_iff — Mathlib

English

The operator norm is subadditive: ∥f + g∥ ≤ ∥f∥ + ∥g∥.

Русский

Норма оператора удовлетворяет неравенству треугольника: ∥f + g∥ ≤ ∥f∥ + ∥g∥.

LaTeX

$$$$ \\|f + g\\| \\le \\|f\\| + \\|g\\|.$$$$

Lean4

theorem opNorm_le_iff {f : ContinuousMultilinearMap 𝕜 E G} {C : ℝ} (hC : 0 ≤ C) :
    ‖f‖ ≤ C ↔ ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
  ⟨fun h _ ↦ le_of_opNorm_le h _, opNorm_le_bound hC⟩

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