Commit 2022-06-26 21:36 f2b108e8

refactor(set_theory/cardinal/*): cardinal.sup → supr (#14569) We remove cardinal.sup in favor of supr. We tweak many other theorems relating to cardinal suprema in the process. A noteworthy consequence is that there's no longer universe constraints on the domain and codomain of the functions one takes the supremum of. When one does still have this constraint, one can use bdd_above_range to immediately prove their range is bounded above.

<!-- Lemmas `lift_sup_le`, `lift_sup_le_iff`, `lift_sup_le_lift_sup`, and `lift_sup_le_lift_sup'` have been removed by virtue of being trivial consequences of basic lemmas on suprema and `lift_supr`. -->

The result of this PR is the following replacements:

• cardinal.sup → supr
• cardinal.le_sup → le_csupr
• cardinal.sup_le → csupr_le'
• cardinal.sup_le_sup → csupr_mono
• cardinal.sup_le_sum → cardinal.supr_le_sum
• cardinal.sum_le_sup → cardinal.sum_le_supr
• cardinal.sum_le_sup_lift → cardinal.sum_le_supr_lift
• cardinal.sup_eq_zero → cardinal.supr_of_empty
• cardinal.le_sup_iff → le_csupr_iff'
• cardinal.lift_sup → cardinal.lift_supr
• cardinal.lift_sup_le → cardinal.lift_supr + csupr_le'
• cardinal.lift_sup_le_iff → cardinal.lift_supr + csupr_le_iff
• cardinal.lift_sup_le_lift_sup → cardinal.lift_supr + csupr_le_iff'
• cardinal.lift_sup_le_lift_sup' → cardinal.lift_supr + csupr_mono'
• cardinal.sup_lt_lift → cardinal.supr_lt_lift
• cardinal.sup_lt → cardinal.supr_lt