English
Let s(r) be a decreasing family indexed by a linear order with dense ordering and first-countable topology; then the measure tends to μ(⋂_{r>a} s(r)) as r ↓ a.
Русский
Пусть s(r) — убывающее семейство по линейному порядку с плотной связью и первой счётностью; тогда мера сходится к μ(⋂_{r>a} s(r)) при r ↓ a.
LaTeX
$$$$\mathrm{Tendsto}(\mu\circ s)(\mathcal{nhdsWithin\ a}(\mathrm{Ioi}\ a))\ (\mathcal{nhds}(μ(\bigcap_{r>a} s(r)))).$$$$
Lean4
/-- Some version of continuity of a measure in the empty set using the intersection along a set of
sets. -/
theorem exists_measure_iInter_lt {α ι : Type*} {_ : MeasurableSpace α} {μ : Measure α} [SemilatticeSup ι] [Countable ι]
{f : ι → Set α} (hm : ∀ i, NullMeasurableSet (f i) μ) {ε : ℝ≥0∞} (hε : 0 < ε) (hfin : ∃ i, μ (f i) ≠ ∞)
(hfem : ⋂ n, f n = ∅) : ∃ m, μ (⋂ n ≤ m, f n) < ε :=
by
let F m := μ (⋂ n ≤ m, f n)
have hFAnti : Antitone F := fun i j hij => measure_mono (biInter_subset_biInter_left fun k hki => le_trans hki hij)
suffices Filter.Tendsto F Filter.atTop (𝓝 0) by
let _ := hfin.nonempty
rw [ENNReal.tendsto_atTop_zero_iff_lt_of_antitone hFAnti] at this
exact this ε hε
have hzero : μ (⋂ n, f n) = 0 := by simp only [hfem, measure_empty]
rw [← hzero]
exact tendsto_measure_iInter_le hm hfin
