top_ne_ofNat

Mathlib.Data.ENNReal.Basic

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

English

Simp lemma: ∞ ≠ ofNat(n) for n with AtLeastTwo.

Русский

Упрощение: ∞ ≠ ofNat(n) для n с AtLeastTwo.

LaTeX

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

Lean4

@[simp]
theorem top_ne_ofNat {n : ℕ} [n.AtLeastTwo] : ∞ ≠ ofNat(n) :=
  ofNat_ne_top.symm

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

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

Разделы

Аффилиация

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