ofReal_mul' — Mathlib

English

For real p and q with q ≥ 0, ENNReal.ofReal(p q) = ENNReal.ofReal(p) · ENNReal.ofReal(q).

Русский

Для действительных p, q с q ≥ 0: ENNReal.ofReal(p q) = ENNReal.ofReal(p) · ENNReal.ofReal(q).

LaTeX

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

Lean4

theorem ofReal_mul' {p q : ℝ} (hq : 0 ≤ q) : ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q := by
  rw [mul_comm, ofReal_mul hq, mul_comm]

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