type_nat_lt

Mathlib.SetTheory.Ordinal.Basic

URI: https://scilib.ai/kg/mathlib#Ordinal.type_nat_lt

English

The type of natural numbers with the usual order has ordinal type ω.

Русский

Тип натуральных чисел с обычным порядком имеет ординальный тип ω.

LaTeX

$$$ \operatorname{type}(\mathbb{N}) = \omega $$$

Lean4

/-- Note that the presence of this lemma makes `simp [omega0]` form a loop. -/
@[simp]
theorem type_nat_lt : typeLT ℕ = ω :=
  (lift_id _).symm

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

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

Разделы

Аффилиация

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