Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-08 19:25 fc1fd3dc

View on Github →

feat(set_theory/cofinality): sum_lt_of_is_regular

Estimated changes

Modified set_theory/cardinal.lean

modified theorem cardinal.sup_le

Modified set_theory/cofinality.lean

added theorem cardinal.sum_lt_of_is_regular

added theorem cardinal.sup_lt_of_is_regular

Modified set_theory/ordinal.lean

added theorem cardinal.add_lt_of_lt

added theorem cardinal.mul_lt_of_lt

added theorem ordinal.sup_ord