Theorems · Theorem · measure theory

VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae

∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {v : VitaliFamily μ} {f : X → Set (Set X)} {s : Set X},
  v.FineSubfamilyOn f s →
    ∃ t,
      (∀ p ∈ t, p.1 ∈ s) ∧
        (t.PairwiseDisjoint fun p => p.2) ∧ (∀ p ∈ t, p.2 ∈ v.setsAt p.1 ∩ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0

Defined in

Mathlib.MeasureTheory.Covering.VitaliFamily

Cited by

5 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace