mk_Iio_ordinal

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

The cardinality of the initial segment Iio(o) equals lift(o.card).

Русский

Кардинал начального отрезка Iio(o) равен lift(o.card).

LaTeX

$$$$ \#(Iio(o)) = \operatorname{lift}(o.\mathrm{card}) $$$$

Lean4

theorem mk_Iio_ordinal (o : Ordinal.{u}) : #(Iio o) = Cardinal.lift.{u + 1} o.card :=
  by
  rw [lift_card, ← typein_ordinal]
  rfl

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

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

Разделы

Аффилиация

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