Theorems · Theorem · measure theory

IsUnifLocDoublingMeasure.tendsto_closedBall_filterAt

∀ {α : 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 : α} {ι : Type u_2} {l : Filter ι} (w : ι → α)
  (δ : ι → ℝ),
  Filter.Tendsto δ l (nhdsWithin 0 (Set.Ioi 0)) →
    (∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)) →
      Filter.Tendsto (fun j => Metric.closedBall (w j) (δ j)) l ((IsUnifLocDoublingMeasure.vitaliFamily μ K).filterAt x)

Defined in

Mathlib.MeasureTheory.Covering.DensityTheorem

Cited by

3 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceMeasurableSpaceIsUnifLocDoublingMeasureSecondCountableTopologyBorelSpaceMeasureTheory.IsLocallyFiniteMeasure