Covering theorems for Lebesgue measure in one dimension

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

theorem Real.Icc_mem_vitaliFamily_at_right {x y : ℝ} (hxy : x < y) : Set.Icc x y ∈ (IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1).setsAt x

theorem Real.tendsto_Icc_vitaliFamily_right (x : ℝ) : Filter.Tendsto (fun (y : ℝ) => Set.Icc x y) (nhdsWithin x (Set.Ioi x)) ((IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1).filterAt x)

theorem Real.Icc_mem_vitaliFamily_at_left {x y : ℝ} (hxy : x < y) : Set.Icc x y ∈ (IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1).setsAt y

theorem Real.tendsto_Icc_vitaliFamily_left (x : ℝ) : Filter.Tendsto (fun (y : ℝ) => Set.Icc y x) (nhdsWithin x (Set.Iio x)) ((IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1).filterAt x)