mk_ord_toType

Mathlib.SetTheory.Ordinal.Basic

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

English

For any cardinal c, the cardinal of c.ord.toType equals c.

Русский

Для любого кардинала c кардинал #(c.ord.toType) равен c.

LaTeX

$$$ \#(c.ord.toType) = c $$$

Lean4

theorem mk_ord_toType (c : Cardinal) : #c.ord.toType = c := by simp

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

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

Разделы

Аффилиация

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