Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-05 06:48 8991f28d

View on Github →

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.

Estimated changes