norm_mul_le_of_le — Mathlib

English

If ‖a1‖ ≤ r1 and ‖a2‖ ≤ r2 with r1,r2 ∈ ℝ, then ‖a1 a2‖ ≤ r1 r2.

Русский

Если ‖a1‖ ≤ r1 и ‖a2‖ ≤ r2 с r1,r2 ∈ ℝ, то ‖a1 a2‖ ≤ r1 r2.

LaTeX

$$$\forall a_1,a_2,\ r_1,r_2\in\mathbb{R},\ \|a_1\| \le r_1 \land \|a_2\| \le r_2 \Rightarrow \|a_1 a_2\| \le r_1 r_2.$$$

Lean4

theorem norm_mul_le_of_le {r₁ r₂ : ℝ} (h₁ : ‖a₁‖ ≤ r₁) (h₂ : ‖a₂‖ ≤ r₂) : ‖a₁ * a₂‖ ≤ r₁ * r₂ :=
  (norm_mul_le ..).trans <| mul_le_mul h₁ h₂ (norm_nonneg _) ((norm_nonneg _).trans h₁)

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