Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-10 01:48 7eff2330

View on Github →

feat(set_theory/cofinality): Golf and extend existing results relating cof to sup and bsup (#12321)

Estimated changes

Modified src/set_theory/cofinality.lean

added theorem cardinal.blsub_lt_ord_lift_of_is_regular

added theorem cardinal.blsub_lt_ord_of_is_regular

added theorem cardinal.bsup_lt_ord_lift_of_is_regular

added theorem cardinal.bsup_lt_ord_of_is_regular

added theorem cardinal.lsub_lt_ord_lift_of_is_regular

added theorem cardinal.lsub_lt_ord_of_is_regular

added theorem cardinal.sum_lt_lift_of_is_regular

modified theorem cardinal.sum_lt_of_is_regular

added theorem cardinal.sup_lt_lift_of_is_regular

modified theorem cardinal.sup_lt_of_is_regular

added theorem cardinal.sup_lt_ord_lift_of_is_regular

modified theorem cardinal.sup_lt_ord_of_is_regular

added theorem ordinal.blsub_lt_ord

added theorem ordinal.blsub_lt_ord_lift

added theorem ordinal.bsup_lt_ord

added theorem ordinal.bsup_lt_ord_lift

added theorem ordinal.cof_blsub_le_lift

modified theorem ordinal.cof_bsup_le

modified theorem ordinal.cof_bsup_le_lift

added theorem ordinal.cof_lsub_le_lift

modified theorem ordinal.cof_sup_le

modified theorem ordinal.cof_sup_le_lift

added theorem ordinal.lsub_lt_ord

added theorem ordinal.lsub_lt_ord_lift

modified theorem ordinal.sup_lt

added theorem ordinal.sup_lt_lift

modified theorem ordinal.sup_lt_ord

added theorem ordinal.sup_lt_ord_lift