ofReal_mul — Mathlib

English

For p ≥ 0 and any q ∈ ℝ, ENNReal.ofReal(p q) = ENNReal.ofReal(p) · ENNReal.ofReal(q).

Русский

Для p ≥ 0 и любого q ∈ ℝ выполняется ENNReal.ofReal(p q) = ENNReal.ofReal(p) · ENNReal.ofReal(q).

LaTeX

$$$p \ge 0 \Rightarrow \operatorname{ofReal}(p q) = \operatorname{ofReal}(p) \cdot \operatorname{ofReal}(q)$$$

Lean4

@[simp]
theorem ofReal_mul {p q : ℝ} (hp : 0 ≤ p) : ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q := by
  simp only [ENNReal.ofReal, ← coe_mul, Real.toNNReal_mul hp]

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