Commit 2022-05-23 01:49 01eda9ab

feat(topology/instances/ennreal): golf, add lemmas about supr_add_supr (#14274)

• add ennreal.bsupr_add' etc that deal with {ι : Sort*} {p : ι → Prop} instead of {ι : Type*} {s : set ι};
• golf some proofs by reusing more powerful generic lemmas;
• add ennreal.supr_add_supr_le, ennreal.bsupr_add_bsupr_le, and ennreal.bsupr_add_bsupr_le'.