principal_add

Mathlib.SetTheory.Cardinal.Ordinal

URI: https://scilib.ai/kg/mathlib#Ordinal.IsInitial.principal_add

← MathLib Explorer

English

If o is initial and ω ≤ o, then addition on o is principal.

Русский

Если o является начальным и ω ≤ o, то сложение на o — главная операция.

LaTeX

$$Principal (· + ·) o$$

Lean4

theorem principal_add {o : Ordinal} (h : IsInitial o) (ho : ω ≤ o) : Principal (· + ·) o :=
  by
  rw [← h.ord_card]
  apply principal_add_ord
  rwa [aleph0_le_card]

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

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

Разделы

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

Аффилиация

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