instSuccOrderToType

Mathlib.SetTheory.Ordinal.Basic

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

English

If α is empty, then type r = 0 for any well-order r on α.

Русский

Если α пустое, то для любого полного порядка r на α имеет место type r = 0.

LaTeX

$$$type(r) = 0$ при условии [IsEmpty α] и [IsWellOrder α r].$$

Lean4

noncomputable instance (o : Ordinal) : SuccOrder o.toType :=
  SuccOrder.ofLinearWellFoundedLT o.toType

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

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

Разделы

Аффилиация

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