Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-08 04:50 ce0dc836

View on Github →

feat(set_theory/ordinal/basic): Supremum indexed over an empty / unique type (#13735) This PR contains the following changes:

  • The lemmas sup_unique, bsup_one, lsub_unique, blsub_one.
  • congr lemmas for bsup and blsub
  • Arguments like o = 0 are removed as the congr lemmas now handle this.
  • a + 1 is changed to a.succ in some lemmas (for better rewriting).

Estimated changes

added theorem ordinal.blsub_congr
modified theorem ordinal.blsub_const
added theorem ordinal.blsub_one
modified theorem ordinal.blsub_zero
added theorem ordinal.bsup_congr
added theorem ordinal.bsup_one
modified theorem ordinal.bsup_zero
modified theorem ordinal.lsub_const
modified theorem ordinal.lsub_empty
added theorem ordinal.lsub_unique
modified theorem ordinal.sup_const
modified theorem ordinal.sup_empty
added theorem ordinal.sup_unique