mathlib

66285c9f - feat(topology/instances/ennreal): if a tsum is finite, then the tsum over the complement of a finset tends to 0 at top (#9665)

feat(topology/instances/ennreal): if a tsum is finite, then the tsum over the complement of a finset tends to 0 at top (#9665) Together with minor tweaks of the library: * rename `bounded.subset` to `bounded.mono` * remove `bUnion_subset_bUnion_right`, which is exactly the same as `bUnion_mono`. Same for intersections. * add `bUnion_congr` and `bInter_congr` * introduce lemma `null_of_locally_null`: if a set has zero measure in a neighborhood of each of its points, then it has zero measure in a second-countable space.