Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-14 15:50 c992b04d

View on Github →

feat(set_theory/cardinal/cofinality): Cofinality of nfp and deriv (#12556)

Estimated changes

Modified src/set_theory/cardinal/cofinality.lean

added theorem cardinal.deriv_bfamily_lt_ord

added theorem cardinal.deriv_bfamily_lt_ord_lift

added theorem cardinal.deriv_family_lt_ord

added theorem cardinal.deriv_family_lt_ord_lift

added theorem cardinal.deriv_lt_ord

added theorem cardinal.nfp_bfamily_lt_ord_lift_of_is_regular

added theorem cardinal.nfp_bfamily_lt_ord_of_is_regular

added theorem cardinal.nfp_family_lt_ord_lift_of_is_regular

added theorem cardinal.nfp_family_lt_ord_of_is_regular

added theorem cardinal.nfp_lt_ord_of_is_regular

added theorem ordinal.nfp_bfamily_lt_ord

added theorem ordinal.nfp_bfamily_lt_ord_lift

added theorem ordinal.nfp_family_lt_ord

added theorem ordinal.nfp_family_lt_ord_lift

added theorem ordinal.nfp_lt_ord