nnnorm_le_mul_nnnorm_add' — Mathlib

English

Analogous left-variant: ‖b‖₊ ≤ ‖a·b‖₊ + ‖a‖₊ for a,b ∈ E.

Русский

Аналогичная левая версия: ‖b‖₊ ≤ ‖a·b‖₊ + ‖a‖₊.

LaTeX

$$$$ \\|b\\|_{+} \\leq \\|a \\cdot b\\|_{+} + \\|a\\|_{+} $$$$

Lean4

/-- An analogue of `nnnorm_le_mul_nnnorm_add` for the multiplication from the left. -/
@[to_additive /-- An analogue of `nnnorm_le_add_nnnorm_add` for the addition from the left. -/
    ]
theorem nnnorm_le_mul_nnnorm_add' (a b : E) : ‖b‖₊ ≤ ‖a * b‖₊ + ‖a‖₊ :=
  norm_le_mul_norm_add' _ _

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