Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-19 13:44 55a2c1a4

View on Github →

refactor(set_theory/{cardinal,ordinal}): swap the order of universes in lift (#9273) Swap the order of universe arguments in cardinal.lift and ordinal.lift. This way (a) they match the order of arguments in ulift; (b) usually Lean can deduce the second universe level from the argument.

Estimated changes

modified theorem complex.{u}
modified def cardinal.lift
modified theorem cardinal.lift_eq_nat_iff
modified theorem cardinal.lift_mk
modified theorem cardinal.lift_umax
modified theorem cardinal.lift_lt_univ'
modified theorem cardinal.lift_lt_univ
modified theorem cardinal.lift_univ
modified theorem cardinal.lt_univ'
modified theorem cardinal.lt_univ
modified def cardinal.univ
modified def ordinal.lift
modified theorem ordinal.lift_lift
modified theorem ordinal.lift_umax
modified theorem ordinal.lift_univ
modified def ordinal.univ