noMaxOrder

Mathlib.SetTheory.Ordinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Cardinal.noMaxOrder

English

For every infinite cardinal c, the type of ord(c) has no maximal element.

Русский

Для любого бесконечного кардинала c тип ord(c) не имеет максимального элемента.

LaTeX

$$$\forall c\, (\aleph_0 \le c) \to NoMaxOrder\, c.ord.toType$$$

Lean4

theorem noMaxOrder {c} (h : ℵ₀ ≤ c) : NoMaxOrder c.ord.toType :=
  toType_noMax_of_succ_lt fun _ ↦ (isSuccLimit_ord h).succ_lt

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

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

Разделы

Аффилиация

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