toReal_smul

Mathlib.Data.ENNReal.Action

URI: https://scilib.ai/kg/mathlib#ENNReal.toReal_smul

English

For r ∈ ℝ≥0 and s ∈ ENNReal, (r • s).toReal = r • s.toReal.

Русский

Для r ∈ ℝ≥0 и s ∈ ENNReal, (r • s).toReal = r • s.toReal.

LaTeX

$$$ \operatorname{toReal}(r \cdot s) = r \cdot \operatorname{toReal}(s). $$$

Lean4

theorem toReal_smul (r : ℝ≥0) (s : ℝ≥0∞) : (r • s).toReal = r • s.toReal :=
  by
  rw [ENNReal.smul_def, smul_eq_mul, toReal_mul, coe_toReal]
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru