toReal_ofReal_mul — Mathlib

English

For real c and ENNReal a with c ≥ 0, toReal(ofReal(c) · a) = c · toReal(a).

Русский

Для действительного c ≥ 0 и ENNReal a: toReal(ofReal(c) · a) = c · toReal(a).

LaTeX

$$$c \in \mathbb{R}, a \in \mathbb{R}_{\ge 0}^{\infty}, c \ge 0 \Rightarrow \mathrm{toReal}(\operatorname{ofReal}(c) \cdot a) = c \cdot \mathrm{toReal}(a)$$$

Lean4

theorem toReal_ofReal_mul (c : ℝ) (a : ℝ≥0∞) (h : 0 ≤ c) :
    ENNReal.toReal (ENNReal.ofReal c * a) = c * ENNReal.toReal a := by rw [ENNReal.toReal_mul, ENNReal.toReal_ofReal h]

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