cof_add

Mathlib.SetTheory.Cardinal.Cofinality

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

← MathLib Explorer

English

If b ≠ 0 then cof(a+b) = cof(b).

Русский

Если b ≠ 0, то cof(a+b) = cof(b).

LaTeX

$$$$ b \neq 0 \Rightarrow cof(a+b)=cof(b). $$$$

Lean4

@[simp]
theorem cof_add (a b : Ordinal) : b ≠ 0 → cof (a + b) = cof b := fun h =>
  by
  rcases zero_or_succ_or_isSuccLimit b with (rfl | ⟨c, rfl⟩ | hb)
  · contradiction
  · rw [add_succ, cof_succ, cof_succ]
  · exact (isNormal_add_right a).cof_eq hb

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

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

Разделы

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

Аффилиация

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