limits of measures on reals

Stream: Is there code for X?

[Floris van Doorn]

We have docs#MeasureTheory.tendsto_measure_iInter which shows that measures converge along countable limits in certain cases. Often you take a limit indexed by the real numbers which has a countable dense subset, which should be just as good. Do we have results in this direction in Mathlib? Here is an example that shows what I roughly want (though I'm not interested in this particular theorem) :

import Mathlib

open MeasureTheory Metric Topology

theorem tendsto_measure_ball_zero {α : Type*} [MeasurableSpace α] [MetricSpace α]
  [BorelSpace α] [ProperSpace α]
  {μ : Measure α} [IsFiniteMeasureOnCompacts μ] {x : α} :
  Filter.Tendsto (fun r ↦ μ (ball x r)) (𝓝[>] 0) (𝓝 (μ {x})) := by sorry

[Floris van Doorn]

Ah, I found docs#MeasureTheory.tendsto_measure_biInter_gt . Perfect! @Leo Diedering: this will be useful for you.