Theorems · Theorem · measure theory

VitaliFamily.covering

∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (self : VitaliFamily μ) (s : Set X) (f : X → Set (Set X)),
  (∀ x ∈ s, f x ⊆ self.setsAt x) →
    (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ Metric.closedBall x ε) →
      ∃ t, (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p => p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0

Consider a (possibly non-measurable) set s, and for any x in s a subfamily f x of setsAt x containing sets of arbitrarily small diameter. Then one can extract a disjoint subfamily covering almost all s.

Defined in

Mathlib.MeasureTheory.Covering.VitaliFamily

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace