mathlib

3a3ec6c3 - feat(measure_theory): each set has a measurable superset of the same measure (#5688)

feat(measure_theory): each set has a measurable superset of the same measure (#5688) * generalize `outer_measure.exists_is_measurable_superset_of_trim_eq_zero` to `outer_measure.exists_is_measurable_superset_eq_trim`; * generalize `exists_is_measurable_superset_of_null` to `exists_is_measurable_superset`; * define `to_measurable mu s` to be a measurable superset `t ⊇ s` with `μ t = μ s`; * prove `countable_cover_nhds`: in a `second_countable_topology`, if `f` sends each point `x` to a neighborhood of `x`, then some countable subfamily of neighborhoods `f x` cover the whole space. * `sigma_finite_of_countable` no longer assumes that all sets `s ∈ S` are measurable.