toNNReal_mul_nnnorm — Mathlib

English

For x ∈ ℝ and y ∈ ℝ with y ≥ 0, x.toNNReal · ‖y‖₊ = ‖x·y‖₊.

Русский

Для x ∈ ℝ и y ∈ ℝ, если y ≥ 0, то x.toNNReal · ‖y‖₊ = ‖xy‖₊.

LaTeX

$$$ x^{\mathrm{toNNReal}} \cdot \|y\|_+ = \|xy\|_+ \quad (\text{when } y \ge 0) $$$

Lean4

theorem toNNReal_mul_nnnorm {x : ℝ} (y : ℝ) (hx : 0 ≤ x) : x.toNNReal * ‖y‖₊ = ‖x * y‖₊ :=
  by
  ext
  simp only [NNReal.coe_mul, nnnorm_mul, coe_nnnorm, Real.toNNReal_of_nonneg, norm_of_nonneg, hx, NNReal.coe_mk]

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