Commit 2020-10-11 15:12 33f7870a
View on Github →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_bUnionusesfinset's has_mem, not coercion to set. Also replace tendsto_at_top_supr_natetc with slightly more general versions using a[semilattice_sup β] [nonempty β]instead ofnat`.