Commit 2024-11-04 14:05 95041c9c

View on Github →

feat(SetTheory/Ordinal/FixedPoint): generalize universes of nfpFamily (#17751) We generalize nfpFamily to indexed families of universes with an index in an arbitrary universe, instead taking Small hypotheses for the theorems that need it. We're thus able to deprecate nfpBFamily, which is a specific case of this.

Estimated changes

added theorem Ordinal.iSup_eq_bsup
modified theorem Ordinal.apply_le_nfpFamily
modified theorem Ordinal.apply_lt_nfpFamily
modified def Ordinal.derivBFamily
modified def Ordinal.derivFamily
modified theorem Ordinal.derivFamily_fp
modified theorem Ordinal.deriv_limit
modified theorem Ordinal.foldr_le_nfpFamily
modified theorem Ordinal.fp_iff_derivFamily
deleted theorem Ordinal.fp_unbounded
modified theorem Ordinal.le_iff_derivFamily
modified theorem Ordinal.le_nfpFamily
modified theorem Ordinal.lt_nfpFamily
modified def Ordinal.nfpBFamily
modified def Ordinal.nfpFamily
modified theorem Ordinal.nfpFamily_eq_self
modified theorem Ordinal.nfpFamily_eq_sup
modified theorem Ordinal.nfpFamily_fp
modified theorem Ordinal.nfpFamily_le
modified theorem Ordinal.nfpFamily_le_apply
modified theorem Ordinal.nfpFamily_le_iff
modified theorem Ordinal.nfpFamily_monotone
modified theorem Ordinal.nfp_mul_one