Theorems · Theorem · measure theory

Vitali.exists_disjoint_subfamily_covering_enlargement_closedBall

∀ {α : Type u_1} {ι : Type u_2} [inst : PseudoMetricSpace α] (t : Set ι) (x : ι → α) (r : ι → ℝ) (R : ℝ),
  (∀ a ∈ t, r a ≤ R) →
    ∀ (τ : ℝ),
      3 < τ →
        ∃ u ⊆ t,
          (u.PairwiseDisjoint fun a => Metric.closedBall (x a) (r a)) ∧
            ∀ a ∈ t, ∃ b ∈ u, Metric.closedBall (x a) (r a) ⊆ Metric.closedBall (x b) (τ * r b)

Vitali covering theorem, closed balls version: given a family t of closed balls, one can extract a disjoint subfamily u ⊆ t so that all balls in t are covered by the τ-times dilations of balls in u, for some τ > 3.

Defined in

Mathlib.MeasureTheory.Covering.Vitali

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace