ord_card

Mathlib.SetTheory.Cardinal.Aleph

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

English

If o is initial, then o.card.ord = o.

Русский

Если o — начальный, то o.card.ord = o.

LaTeX

$$$\\\\forall o \\\\text{IsInitial}(o), \\\\operatorname{ord}_{o.card} = o.$$$

Lean4

theorem ord_card {o : Ordinal} (h : IsInitial o) : o.card.ord = o :=
  h

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

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

Разделы

Аффилиация

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