toNNReal_mul_top

Mathlib.Data.ENNReal.Real

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

English

The product with the top element annihilates toNNReal: (a · ∞).toNNReal = 0.

Русский

Произведение с бесконечностью даёт ноль под toNNReal: (a · ∞).toNNReal = 0.

LaTeX

$$$ (a \cdot \infty).\mathrm{toNNReal} = 0$$$

Lean4

theorem toNNReal_mul_top (a : ℝ≥0∞) : ENNReal.toNNReal (a * ∞) = 0 := by simp

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

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

Разделы

Аффилиация

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