opNorm_add_le — Mathlib

English

The norm of the product of two continuous multilinear maps equals the maximum of their operator norms.

Русский

Норма произведения двух непрерывных мультилинейных отображений равна максимуму их операторных норм.

LaTeX

$$$$ \\|f.prod g\\| = \\max\\{ \\|f\\|, \\|g\\| \\}.$$$$

Lean4

/-- The operator norm satisfies the triangle inequality. -/
theorem opNorm_add_le (f g : ContinuousMultilinearMap 𝕜 E G) : ‖f + g‖ ≤ ‖f‖ + ‖g‖ :=
  opNorm_le_bound (add_nonneg (opNorm_nonneg f) (opNorm_nonneg g)) fun x =>
    by
    rw [add_mul]
    exact norm_add_le_of_le (le_opNorm _ _) (le_opNorm _ _)

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