nnnorm_mul_le_of_le — Mathlib

English

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

Русский

Если ‖a1‖₊ ≤ r1 и ‖a2‖₊ ≤ r2, тогда ‖a1 a2‖₊ ≤ r1 r2.

LaTeX

$$$\forall a_1,a_2,\ r_1,r_2 \ (r_1,r_2 \in \mathbb{R}_{\ge 0}),\ \|a_1\|_{+} \le r_1 \land \|a_2\|_{+} \le r_2 \Rightarrow \|a_1 a_2\|_{+} \le r_1 r_2.$$$

Lean4

theorem nnnorm_mul_le_of_le {r₁ r₂ : ℝ≥0} (h₁ : ‖a₁‖₊ ≤ r₁) (h₂ : ‖a₂‖₊ ≤ r₂) : ‖a₁ * a₂‖₊ ≤ r₁ * r₂ :=
  (nnnorm_mul_le ..).trans <| mul_le_mul' h₁ h₂

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