Commit 2022-01-13 21:10 e830348b

View on Github →

feat(set_theory/ordinal_arithmetic): Families of ordinals (#11278) This PR introduces some API to convert from ι → β indexed families to Π o < b, β indexed families. This simplifies and contextualizes some existing results.

Estimated changes

Modified src/set_theory/cofinality.lean

Modified src/set_theory/ordinal_arithmetic.lean

added def ordinal.bfamily_of_family'

added theorem ordinal.bfamily_of_family'_typein

added def ordinal.bfamily_of_family

added theorem ordinal.bfamily_of_family_typein

added theorem ordinal.blsub_eq_blsub

added theorem ordinal.blsub_eq_lsub'

modified theorem ordinal.blsub_eq_lsub

added theorem ordinal.bsup_eq_bsup

added theorem ordinal.bsup_eq_sup'

modified theorem ordinal.bsup_eq_sup

deleted theorem ordinal.bsup_type

added def ordinal.family_of_bfamily'

added theorem ordinal.family_of_bfamily'_enum

added def ordinal.family_of_bfamily

added theorem ordinal.family_of_bfamily_enum

added theorem ordinal.lsub_eq_blsub'

modified theorem ordinal.lsub_eq_blsub

added theorem ordinal.lsub_eq_lsub

added theorem ordinal.sup_eq_bsup'

modified theorem ordinal.sup_eq_bsup

added theorem ordinal.sup_eq_sup