Commit 2021-01-12 13:08 3a3ec6c3

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.