mathlib

8991f28d - feat(measure_theory/covering/vitali_family): define Vitali families (#10057)

feat(measure_theory/covering/vitali_family): define Vitali families (#10057) Vitali families are families of sets (for instance balls around each point in vector spaces) that satisfy covering theorems. Their main feature is that differentiation of measure theorems hold along Vitali families. This PR is a stub defining Vitali families, and giving examples of them thanks to the Besicovitch and Vitali covering theorems. The differentiation theorem is left for another PR.