Commit 2022-01-11 11:13 624cb707

View on Github →

feat(set_theory/ordinal_arithmetic): Extra lemmas about suprema (#11178) Proved lemmas pertaining to when suprema or least strict upper bounds are zero.

Estimated changes

Modified src/set_theory/ordinal.lean

added theorem ordinal.eq_zero_of_out_empty

added theorem ordinal.out_empty_iff_eq_zero

Modified src/set_theory/ordinal_arithmetic.lean

added theorem ordinal.blsub_eq_zero

added theorem ordinal.blsub_eq_zero_iff

added theorem ordinal.blsub_pos

added theorem ordinal.bsup_eq_zero_iff

added theorem ordinal.lsub_eq_zero

added theorem ordinal.lsub_eq_zero_iff

added theorem ordinal.lsub_pos

added theorem ordinal.sup_eq_zero_iff