eventually_measure_lt_top — Mathlib

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

Похожие утверждения