Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-16 20:32 b97bb92f

View on Github →

feat(set_theory/cardinal): lemmas (#9690)

  • swap sides of cardinal.lift_mk, rename it to cardinal.mk_ulift;
  • add cardinal.out_mk_equiv.

Estimated changes

deleted theorem cardinal.lift_mk
added theorem cardinal.mk_ulift