mk_toType

Mathlib.SetTheory.Ordinal.Basic

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

English

There exists a well-order on α whose order type is exactly ord #α.

Русский

Существует удовлетворяющий условию порядок на α, чей тип порядка равен ord #α.

LaTeX

$$$\exists r\ (wo:\IsWellOrder \ α \ r),\ ord(#\α) = @type α r wo$$$

Lean4

@[simp]
theorem mk_toType (o : Ordinal) : #o.toType = o.card :=
  (Ordinal.card_type _).symm.trans <| by rw [Ordinal.type_toType]

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

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

Разделы

Аффилиация

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