nat_le_card

Mathlib.SetTheory.Ordinal.Basic

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

English

For every natural n, n < univ.

Русский

Для любого натурального числа n выполняется n < univ.

LaTeX

$${ n \\in \\mathbb{N} \\;\\Rightarrow\\; n < \\mathrm{univ} }$$

Lean4

@[simp]
theorem nat_le_card {o} {n : ℕ} : (n : Cardinal) ≤ card o ↔ (n : Ordinal) ≤ o := by
  rw [← Cardinal.ord_le, Cardinal.ord_nat]

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

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

Разделы

Аффилиация

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