lt_ord_succ_card

Mathlib.SetTheory.Ordinal.Basic

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

English

For any ordinal o, o < (succ o.card).ord.

Русский

Для любого ординала o выполняется o < (succ o.card).ord.

LaTeX

$$$\,o < (\operatorname{succ} o.card).\ord$$$

Lean4

theorem lt_ord_succ_card (o : Ordinal) : o < (succ o.card).ord :=
  lt_ord.2 <| lt_succ _

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

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

Разделы

Аффилиация

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