Commit 2024-08-27 18:38 ef5a7617

View on Github →

chore(SetTheory/Ordinal/*): o.out.α → o.toType (#16161) It's often desirable to get a concrete type in universe Type u that's order isomorphic to o : Ordinal.{u}. The way we've done this is by using the non-documented (Quotient.out o).α. We rename this to Ordinal.toType o for discoverability, and to hide what frankly should remain an implementation detail. This also entails renaming a bunch of theorems that made reference to out in some form.

Estimated changes

modified theorem Cardinal.noMaxOrder
modified theorem SetTheory.PGame.nim_def
modified theorem Ordinal.toPGame_def
modified theorem Ordinal.toPGame_leftMoves
modified theorem Ordinal.lsub_typein
deleted theorem Cardinal.mk_ord_out
added theorem Cardinal.mk_ord_toType
deleted theorem Cardinal.mk_ordinal_out
added theorem Cardinal.mk_toType
modified theorem Ordinal.enum_zero_le'
modified theorem Ordinal.le_enum_succ
deleted theorem Ordinal.one_out_eq
added theorem Ordinal.one_toType_eq
added def Ordinal.toType
modified theorem Ordinal.type_lt
modified theorem Ordinal.type_out
modified theorem Ordinal.typein_le_typein'
modified theorem Ordinal.typein_le_typein
modified theorem Ordinal.typein_lt_self
deleted theorem Ordinal.typein_one_out