mathlib

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

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'`.