opNorm_add_le — Mathlib

English

The operator norm satisfies the triangle inequality: ‖f + g‖ ≤ ‖f‖ + ‖g‖.

Русский

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

LaTeX

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

Lean4

/-- The operator norm satisfies the triangle inequality. -/
theorem opNorm_add_le : ‖f + g‖ ≤ ‖f‖ + ‖g‖ :=
  mkNormedAddGroupHom_norm_le _ (add_nonneg (opNorm_nonneg _) (opNorm_nonneg _)) _

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