English
As centers and radii shrink to 0 along a filter, the sequence of closed balls converges to the Vitali filter at x.
Русский
При сжатии центров и радиусов вдоль фильтра последовательность закр. шаров сходится к фильтру Vitali в точке x.
LaTeX
$$$\text{Tendsto}(j\mapsto \overline{B}(w_j, δ_j))\ l\to (\mathrm{vitaliFamily}\, μ K).\text{filterAt } x.$$$
Lean4
/-- For every point `x`, sufficiently small sets in a Vitali family around `x` have finite measure.
(This is a trivial result, following from the fact that the measure is locally finite). -/
theorem eventually_measure_lt_top [IsLocallyFiniteMeasure μ] (x : α) : ∀ᶠ a in v.filterAt x, μ a < ∞ :=
(μ.finiteAt_nhds x).eventually.filter_mono inf_le_left