Covering theorems for Lebesgue measure in one dimension #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

theorem real.Icc_mem_vitali_family_at_right {x y : ℝ} (hxy : x < y) :

set.Icc x y ∈ (is_unif_loc_doubling_measure.vitali_family measure_theory.measure_space.volume 1).sets_at x

source

theorem real.tendsto_Icc_vitali_family_right (x : ℝ) :

filter.tendsto (λ (y : ℝ), set.Icc x y) (nhds_within x (set.Ioi x)) ((is_unif_loc_doubling_measure.vitali_family measure_theory.measure_space.volume 1).filter_at x)

source

theorem real.Icc_mem_vitali_family_at_left {x y : ℝ} (hxy : x < y) :

set.Icc x y ∈ (is_unif_loc_doubling_measure.vitali_family measure_theory.measure_space.volume 1).sets_at y

source

theorem real.tendsto_Icc_vitali_family_left (x : ℝ) :

filter.tendsto (λ (y : ℝ), set.Icc y x) (nhds_within x (set.Iio x)) ((is_unif_loc_doubling_measure.vitali_family measure_theory.measure_space.volume 1).filter_at x)