norm_mul_le_of_le' — Mathlib

English

For any a,b ∈ E, the difference of norms is bounded by the norm of their product: ‖a‖ − ‖b‖ ≤ ‖a b‖.

Русский

Для любых a,b ∈ E разность норм ограничена нормой произведения: ‖a‖ − ‖b‖ ≤ ‖a b‖.

LaTeX

$$$\|a\| - \|b\| \le \|a b\|$$$

Lean4

/-- **Triangle inequality** for the norm. -/
@[to_additive norm_add_le_of_le /-- **Triangle inequality** for the norm. -/
    ]
theorem norm_mul_le_of_le' (h₁ : ‖a₁‖ ≤ r₁) (h₂ : ‖a₂‖ ≤ r₂) : ‖a₁ * a₂‖ ≤ r₁ + r₂ :=
  (norm_mul_le' a₁ a₂).trans <| add_le_add h₁ h₂

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