Commit 2024-10-22 17:45 a8d91706

View on Github →

chore(SetTheory/Ordinal/Basic): golf Ordinal.lift lemmas (#17517) We define Ordinal.liftInitialSeg earlier and use it to more easily prove the other theorems on lift.

Estimated changes

modified theorem Ordinal.lift.initialSeg_coe
modified theorem Ordinal.liftInitialSeg_coe
modified theorem Ordinal.lift_card
modified theorem Ordinal.lift_inj
modified theorem Ordinal.lift_le
modified theorem Ordinal.lift_lift
modified theorem Ordinal.lift_lt