Theorems · Definition · measure theory

VitaliFamily.FineSubfamilyOn

{X : Type u_1} →
  [inst : PseudoMetricSpace X] →
    {m0 : MeasurableSpace X} → {μ : MeasureTheory.Measure X} → VitaliFamily μ → (X → Set (Set X)) → Set X → Prop

Given a Vitali family v for a measure μ, a family f is a fine subfamily on a set s if every point x in s belongs to arbitrarily small sets in v.setsAt x ∩ f x. This is precisely the subfamilies for which the Vitali family definition ensures that one can extract a disjoint covering of almost all s.

Defined in

Mathlib.MeasureTheory.Covering.VitaliFamily

Cited by

18 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace