tendsto_measure_iUnion_accumulate

English

For any f: ι → Set α, the measures μ(Accumulate f i) converge to μ(⋃_i f(i)).

Русский

Для любого f: ι → Set α последовательность μ(Accumulate f(i)) сходится к μ(⋃_i f(i)).

LaTeX

$$$$\mathrm{Tendsto}(\lambda i.\mu(\mathrm{Accumulate}(f,i)))\ atTop\ (\mathcal{N}(\mu(\bigcup_i f_i))).$$$$

Lean4

/-- Continuity from below: the measure of the union of a sequence of (not necessarily measurable)
sets is the limit of the measures of the partial unions. -/
theorem tendsto_measure_iUnion_accumulate {α ι : Type*} [Preorder ι] [IsCountablyGenerated (atTop : Filter ι)]
    {_ : MeasurableSpace α} {μ : Measure α} {f : ι → Set α} :
    Tendsto (fun i ↦ μ (Accumulate f i)) atTop (𝓝 (μ (⋃ i, f i))) :=
  by
  refine .of_neBot_imp fun h ↦ ?_
  have := (atTop_neBot_iff.1 h).2
  rw [measure_iUnion_eq_iSup_accumulate]
  exact tendsto_atTop_iSup fun i j hij ↦ by gcongr

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