iSup_natCast

Mathlib.Data.ENNReal.Operations

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

English

The supremum over natural numbers of their natural-cast into ENNReal is infinity.

Русский

Супремум по натуралам их приведение в ENNReal равен бесконечности.

LaTeX

$$$\\sup_{n\\in\\mathbb{N}} (n : \\mathbb{R}_{\\ge 0\\!\\!\\!\\!∞}) = \\infty$$$

Lean4

theorem iSup_natCast : ⨆ n : ℕ, (n : ℝ≥0∞) = ∞ :=
  (iSup_eq_top _).2 fun _b hb => ENNReal.exists_nat_gt (lt_top_iff_ne_top.1 hb)

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

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

Разделы

Аффилиация

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