mathlib documentation

measure_theory.covering.one_dim

Covering theorems for Lebesgue measure in one dimension #

We have a general theory of covering theorems for doubling measures, developed notably in density_theorems.lean. In this file, we expand the API for this theory in one dimension, by showing that intervals belong to the relevant Vitali family.