∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : SecondCountableTopology α] [inst_2 : MeasurableSpace α]
  [inst_3 : OpensMeasurableSpace α] [inst_4 : HasBesicovitchCovering α] (μ : MeasureTheory.Measure α)
  [inst_5 : MeasureTheory.SFinite μ] (x : α),
  Filter.Tendsto (fun r => Metric.closedBall x r) (nhdsWithin 0 (Set.Ioi 0)) ((Besicovitch.vitaliFamily μ).filterAt x)