mathlib

33f7870a - chore(measure_theory/measurable_space): add `finset.is_measurable_bUnion` etc (#4553)

chore(measure_theory/measurable_space): add `finset.is_measurable_bUnion` etc (#4553) I always forget how to convert `finset` or `set.finite` to `set.countable. Also `finset.is_measurable_bUnion` uses `finset`'s `has_mem`, not coercion to `set`. Also replace `tendsto_at_top_supr_nat` etc with slightly more general versions using a `[semilattice_sup β] [nonempty β]` instead of `nat`.