toENNReal_eq_top

Mathlib.Data.Real.ENatENNReal

URI: https://scilib.ai/kg/mathlib#ENat.toENNReal_eq_top

English

An ENNReal image is equal to the top element if and only if the original ENat is top.

Русский

Образ в ENNReal равен верхнему элементу тогда и только тогда, когда исходное ENat равно верхнему.

LaTeX

$$$(n : \\mathbb{R}_{\\ge 0,\\infty}) = \\infty \\iff n = \\top.$$$

Lean4

@[simp, norm_cast]
theorem toENNReal_eq_top : (n : ℝ≥0∞) = ∞ ↔ n = ⊤ := by simp [← toENNReal_inj]

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

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

Разделы

Аффилиация

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