top_ne_ofReal

Mathlib.Data.ENNReal.Basic

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

English

∞ is not equal to ENNReal.ofReal r for any real r.

Русский

∞ не равно ENNReal.ofReal r для любого действительного r.

LaTeX

$$$$ \infty \neq ENNReal.ofReal r. $$$$

Lean4

@[simp]
theorem top_ne_ofReal {r : ℝ} : ∞ ≠ ENNReal.ofReal r :=
  top_ne_coe

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

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

Разделы

Аффилиация

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