Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-02 16:48 c235c612

View on Github →

refactor(set_theory/ordinal_arithmetic): Simpler bsup definition (#11386) We also simplify some existing proofs.

Estimated changes

Modified src/set_theory/ordinal_arithmetic.lean

modified def ordinal.bsup

added theorem ordinal.comp_bfamily_of_family'

added theorem ordinal.comp_bfamily_of_family

added theorem ordinal.comp_family_of_bfamily'

added theorem ordinal.comp_family_of_bfamily

modified theorem ordinal.lsub_eq_lsub

modified theorem ordinal.sup_eq_sup