principal_add_ord

Mathlib.SetTheory.Cardinal.Ordinal

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

← MathLib Explorer

English

If κ is a cardinal with κ ≥ ℵ0, then addition on ordinals is principal at κ.

Русский

Если кардинал κ не меньше ℵ0, сложение ординалов имеет главную структуру на κ.

LaTeX

$$Principal (· + ·) c.ord$$

Lean4

theorem principal_add_ord {c : Cardinal} (hc : ℵ₀ ≤ c) : Principal (· + ·) c.ord :=
  by
  intro a b ha hb
  rw [lt_ord, card_add] at *
  exact add_lt_of_lt hc ha hb

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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