Theorems · Theorem · measure theory

IsUnifLocDoublingMeasure.closedBall_mem_vitaliFamily_of_dist_le_mul

∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [inst_2 : IsUnifLocDoublingMeasure μ] [inst_3 : SecondCountableTopology α] [inst_4 : BorelSpace α]
  [inst_5 : MeasureTheory.IsLocallyFiniteMeasure μ] {K : ℝ} {x y : α} {r : ℝ},
  dist x y ≤ K * r → 0 < r → Metric.closedBall y r ∈ (IsUnifLocDoublingMeasure.vitaliFamily μ K).setsAt x

In the Vitali family IsUnifLocDoublingMeasure.vitaliFamily K, the sets based at x contain all balls closedBall y r when dist x y ≤ K * r.

Defined in

Mathlib.MeasureTheory.Covering.DensityTheorem

Cited by

3 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceMeasurableSpaceIsUnifLocDoublingMeasureSecondCountableTopologyBorelSpaceMeasureTheory.IsLocallyFiniteMeasure