toENNReal_mul' — Mathlib

English

For x,y ∈ EReal, 0 ≤ y → (x*y).toENNReal = x.toENNReal * y.toENNReal.

Русский

Для x,y ∈ EReal, если 0 ≤ y, то (x*y).toENNReal = x.toENNReal * y.toENNReal.

LaTeX

$$$0 \le y \Rightarrow (x \cdot y).toENNReal = x.toENNReal * y.toENNReal$$$

Lean4

/-- `EReal.toENNReal` is multiplicative. For the version with the nonnegativity
hypothesis on the first variable, see `EReal.toENNReal_mul`. -/
theorem toENNReal_mul' {x y : EReal} (hy : 0 ≤ y) : (x * y).toENNReal = x.toENNReal * y.toENNReal := by
  rw [EReal.mul_comm, toENNReal_mul hy, mul_comm]

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