Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-15 15:52 3d1354ce

View on Github →

feat(set_theory/ordinal_arithmetic): Suprema of functions with the same range are equal (#11910)

Estimated changes

Modified src/set_theory/ordinal_arithmetic.lean

added theorem ordinal.blsub_eq_of_brange_eq

added theorem ordinal.blsub_le_of_brange_subset

added def ordinal.brange

added theorem ordinal.brange_bfamily_of_family'

added theorem ordinal.brange_bfamily_of_family

added theorem ordinal.bsup_eq_of_brange_eq

added theorem ordinal.bsup_le_of_brange_subset

added theorem ordinal.lsub_eq_of_range_eq

added theorem ordinal.lsub_le_of_range_subset

added theorem ordinal.mem_brange

added theorem ordinal.mem_brange_self

added theorem ordinal.range_family_of_bfamily'

added theorem ordinal.range_family_of_bfamily

added theorem ordinal.sup_eq_of_range_eq

modified theorem ordinal.sup_eq_sup

added theorem ordinal.sup_le_of_range_subset