Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-05 23:45 b67857e7

View on Github →

refactor(set_theory/ordinal_arithmetic): Reworked sup and bsup API (#11048) This PR does two things:

  • It reworks and matches, for the most part, the API for ordinal.sup and ordinal.bsup.
  • It introduces ordinal.lsub and ordinal.blsub for (bounded) least strict upper bounds, and proves the expected results.

Estimated changes

added theorem ordinal.succ_ne_self
added theorem ordinal.typein_lt_self
modified theorem ordinal.typein_lt_type
added def ordinal.blsub
added theorem ordinal.blsub_eq_lsub
added theorem ordinal.blsub_id
added theorem ordinal.blsub_type
added theorem ordinal.bsup_eq_blsub
added theorem ordinal.bsup_eq_sup
added theorem ordinal.bsup_le_blsub
modified theorem ordinal.is_normal.bsup
added def ordinal.lsub
added theorem ordinal.lsub_eq_blsub
added theorem ordinal.lsub_le_iff_lt
added theorem ordinal.lt_blsub
modified theorem ordinal.lt_bsup
added theorem ordinal.lt_lsub
added theorem ordinal.sup_eq_bsup
added theorem ordinal.sup_eq_lsub
added theorem ordinal.sup_le_lsub
deleted theorem ordinal.sup_succ