Commit 2021-10-12 17:00 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) 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.