Theorems · Definition · measure theory

IsUnifLocDoublingMeasure.vitaliFamily

{α : Type u_2} →
  [inst : PseudoMetricSpace α] →
    [inst_1 : MeasurableSpace α] →
      (μ : MeasureTheory.Measure α) →
        [IsUnifLocDoublingMeasure μ] →
          [SecondCountableTopology α] → [BorelSpace α] → [MeasureTheory.IsLocallyFiniteMeasure μ] → ℝ → VitaliFamily μ

A Vitali family in a space with a uniformly locally doubling measure, designed so that the sets at x contain all closedBall y r when dist x y ≤ K * r.

Defined in

Mathlib.MeasureTheory.Covering.DensityTheorem

Cited by

13 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceMeasurableSpaceIsUnifLocDoublingMeasureSecondCountableTopologyBorelSpaceMeasureTheory.IsLocallyFiniteMeasure