top_ne_natCast

Mathlib.Data.ENNReal.Basic

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

English

For any n with AtLeastTwo, ∞ ≠ ENNReal.ofNat(n).

Русский

Для любого n с AtLeastTwo: ∞ ≠ ENNReal.ofNat(n).

LaTeX

$$$$ \infty \neq \operatorname{ofNat}(n). $$$$

Lean4

@[simp]
theorem top_ne_natCast (n : ℕ) : ∞ ≠ n :=
  WithTop.top_ne_natCast n

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

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

Разделы

Аффилиация

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