Theorems · Definition · measure theory

VitaliFamily.FineSubfamilyOn.covering

{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 → X × Set X → Set X

Given h : v.FineSubfamilyOn f s, then h.covering p is a set in the family, for p ∈ h.index, such that these sets form a disjoint covering of almost every s.

Defined in

Mathlib.MeasureTheory.Covering.VitaliFamily

Cited by

13 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace