Commit 2022-12-15 18:06 d012cd09
View on Github →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.