[Merged by Bors] - feat(measure_theory/covering) weaken sigma_compact_space to second_countable_topology

[sgouezel]

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.

---

[ocfnash]

Wow, really nice; thanks for doing this.

I wonder if there is a topological condition (implying both sigma compact and second countable) that would unify the two results about existence of a finite spanning
sequence of open sets for a locally finite measure?

bors merge

[sgouezel]

I wonder if there is a topological condition (implying both sigma compact and second countable) that would unify the two results about existence of a finite spanning sequence of open sets for a locally finite measure?

Yes: the fact that any open cover admits a countable subcover. I considered introducing a typeclass for this, but adding several dozens of line to save a small code duplication seemed suboptimal.

[ocfnash]

Yes: the fact that any open cover admits a countable subcover.

Right of course!

I considered introducing a typeclass for this, but adding several dozens of line to save a small code duplication seemed suboptimal.

Agreed.

[urkud]

@ocfnash I have an abandoned PR that adds this typeclass: #11716.

[sgouezel]

I didn't know this had a name!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests