iSup_natCast

Mathlib.Data.ENat.Lattice

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

English

Same as above: the supremum of all natural casts is the top element.

Русский

То же: верхний предел всех приводимых натуральных чисел достигает вершины.

LaTeX

$$$\displaystyle \bigl(\bigvee_{n \in \mathbb{N}} (n : \mathbb{N}_\infty)\bigr) = \top$$$

Lean4

theorem iSup_natCast : ⨆ n : ℕ, (n : ℕ∞) = ⊤ :=
  (iSup_eq_top _).2 fun _b hb ↦ ENat.exists_nat_gt (lt_top_iff_ne_top.1 hb)

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

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

Разделы

Аффилиация

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