Theorems · Definition · measure theory

VitaliFamily.FineSubfamilyOn.index

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

Given h : v.FineSubfamilyOn f s, then h.index is a set parametrizing a disjoint covering of almost every s.

Defined in

Mathlib.MeasureTheory.Covering.VitaliFamily

Cited by

14 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace