Theorems · Theorem · measure theory

Vitali.exists_disjoint_subfamily_covering_enlargement

∀ {α : Type u_1} {ι : Type u_2} (B : ι → Set α) (t : Set ι) (δ : ι → ℝ) (τ : ℝ),
  1 < τ →
    (∀ a ∈ t, 0 ≤ δ a) →
      ∀ (R : ℝ),
        (∀ a ∈ t, δ a ≤ R) →
          (∀ a ∈ t, (B a).Nonempty) →
            ∃ u ⊆ t, u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b

Vitali covering theorem: given a set t of subsets of a type, one may extract a disjoint subfamily u such that the τ-enlargement of this family covers all elements of t, where τ > 1 is any fixed number. When t is a family of balls, the τ-enlargement of ball x r is ball x ((1+2τ) r). In general, it is expressed in terms of a function δ (think "radius" or "diameter"), positive and bounded on all elements of t. The condition is that every element a of t should intersect an element b of u of size larger than that of a up to τ, i.e., δ b ≥ δ a / τ. We state the lemma slightly more generally, with an indexed family of sets B a for a ∈ t, for wider applicability.

Defined in

Mathlib.MeasureTheory.Covering.Vitali

Cited by

3 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound