Theorems · Definition · measure theory

VitaliFamily.enlarge

{X : Type u_1} →
  [inst : PseudoMetricSpace X] →
    {m0 : MeasurableSpace X} → {μ : MeasureTheory.Measure X} → VitaliFamily μ → (δ : ℝ) → 0 < δ → VitaliFamily μ

One can enlarge a Vitali family by adding to the sets f x at x all sets which are not contained in a δ-neighborhood on x. This does not change the local filter at a point, but it can be convenient to get a nicer global behavior.

Defined in

Mathlib.MeasureTheory.Covering.VitaliFamily

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace