orderTopToTypeSucc — Mathlib

English

There is an OrderTop instance on the type (succ o).toType, determined by the natural enum-top relation 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

instance orderTopToTypeSucc (o : Ordinal) : OrderTop (succ o).toType :=
  @OrderTop.mk _ _ (Top.mk _) le_enum_succ

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