English
Let s: ι → Set α be monotone (increasing). Then the measures μ(s(i)) converge to μ(⋃_n s(n)) as i tends to the top filter.
Русский
Пусть s: ι → Set α возрастает. Тогда μ(s(i)) стремится к μ(⋃_n s(n)) при направлении к бесконечности.
LaTeX
$$$$\text{Monotone}(s) \Rightarrow \ \mathrm{Tendsto}(\mu \circ s)\ atTop\ (\mathcal{N}(\mu(\bigcup_n s_n))).$$$$
Lean4
/-- Continuity from below: the measure of the union of an increasing sequence of (not necessarily
measurable) sets is the limit of the measures. -/
theorem tendsto_measure_iUnion_atTop [Preorder ι] [IsCountablyGenerated (atTop : Filter ι)] {s : ι → Set α}
(hm : Monotone s) : Tendsto (μ ∘ s) atTop (𝓝 (μ (⋃ n, s n))) :=
by
refine .of_neBot_imp fun h ↦ ?_
have := (atTop_neBot_iff.1 h).2
rw [hm.measure_iUnion]
exact tendsto_atTop_iSup fun n m hnm => measure_mono <| hm hnm
