mathlib3

d012cd09 - feat(measure_theory/covering) weaken sigma_compact_space to second_countable_topology (#17960)

feat(measure_theory/covering) weaken sigma_compact_space to second_countable_topology (#17960) Currently, theorems on differentiation of measures require the assumption that the space is sigma compact. However, they all hold under the weaker assumption that the space is second-countable, as shown by this PR.