smul_toNNReal — Mathlib

English

For a ∈ ℝ≥0 and b ∈ ENNReal, (a • b).toNNReal = a * b.toNNReal.

Русский

Для a ∈ ℝ≥0 и b ∈ ENNReal выполняется (a • b).toNNReal = a * b.toNNReal.

LaTeX

$$$ (a \cdot b).toNNReal = a \cdot b.toNNReal. $$$

Lean4

@[simp]
theorem smul_toNNReal (a : ℝ≥0) (b : ℝ≥0∞) : (a • b).toNNReal = a * b.toNNReal :=
  by
  change ((a : ℝ≥0∞) * b).toNNReal = a * b.toNNReal
  simp only [ENNReal.toNNReal_mul, ENNReal.toNNReal_coe]

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