type_toType

Mathlib.SetTheory.Ordinal.Basic

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

English

For any o, the type corresponding to o is the same as o; i.e., the order-type of o's underlying type equals o.

Русский

Пусть имеет место то, что соответствующий o тип совпадает с o; то есть порядковый тип основы o равен o.

LaTeX

$$$\mathrm{typeL T}(o.\text{toType}) = o$$$

Lean4

@[simp]
theorem type_toType (o : Ordinal) : typeLT o.toType = o :=
  o.out_eq

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

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

Разделы

Аффилиация

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