norm_mul₃_le' — Mathlib

English

For any a,b,c ∈ E, the norm of the triple product is bounded by the sum of the norms: ‖a b c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖.

Русский

Для любых a,b,c ∈ E нормa произведения тройки не превосходит суммы норм: ‖a b c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖.

LaTeX

$$$‖a b c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖$$$

Lean4

/-- **Triangle inequality** for the norm. -/
@[to_additive norm_add₃_le /-- **Triangle inequality** for the norm. -/
    ]
theorem norm_mul₃_le' : ‖a * b * c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ :=
  norm_mul_le_of_le' (norm_mul_le' _ _) le_rfl

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