Commit 2022-06-17 01:10 d21469e4

View on Github →

feat(set_theory/ordinal/basic): improve docs on lift, add simp lemmas (#14599) This is pretty much the same thing as #14596, just on ordinal.lift instead of cardinal.lift.

Estimated changes

Modified src/set_theory/ordinal/basic.lean

modified theorem ordinal.lift_id'

modified theorem ordinal.lift_lift

added theorem ordinal.lift_umax'

modified theorem ordinal.lift_umax

added theorem ordinal.lift_uzero