mathlib

17665882 - feat(measure_theory/covering/vitali): Vitali covering theorems (#9680)

feat(measure_theory/covering/vitali): Vitali covering theorems (#9680) The topological and measurable Vitali covering theorems. * topological version: if a space is covered by balls `(B (x_i, r_i))_{i \in I}`, one can extract a disjointed subfamily indexed by `J` such that the space is covered by the balls `B (x_j, 5 r_j)`. * measurable version: if additionally the measure has a doubling-like property, and the covering contains balls of arbitrarily small radius at every point, then the disjointed subfamily one obtains above covers almost all the space. These two statements are particular cases of more general statements that are proved in this PR.