toENNReal_ne_top

Mathlib.Data.Real.ENatENNReal

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

English

The image is not equal to infinity if and only if the original ENat is not top.

Русский

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

LaTeX

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

Lean4

@[norm_cast]
theorem toENNReal_ne_top : (n : ℝ≥0∞) ≠ ∞ ↔ n ≠ ⊤ := by simp

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

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

Разделы

Аффилиация

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