ordinalPred_eq

Mathlib.SetTheory.Ordinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Order.IsSuccLimit.ordinalPred_eq

English

There is an OrderTop instance on (succ o).toType defined by le_enum_succ.

Русский

Существует экземпляр OrderTop на (succ o).toType, задаваемый le_enum_succ.

LaTeX

$$$$ \mathrm{OrderTop}((\mathrm{succ}\ o).\mathrm{toType}) \text{ defined by } \mathrm{Top.mk} \text{ with } \mathrm{le\_enum\_succ} $$$$

Lean4

theorem _root_.Order.IsSuccLimit.ordinalPred_eq {o} (ho : IsSuccLimit o) : pred o = o :=
  ho.isSuccPrelimit.ordinalPred_eq

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

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

Разделы

Аффилиация

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