tendsto_measure_iUnion_atBot — Mathlib

English

Let s: ι → Set α be antitone (decreasing). Then μ(⋃_n s(n)) is the limit of μ(s(n)) as n tends to the bottom filter.

Русский

Пусть s: ι → Set α убывает. Тогда μ(⋃_n s(n)) является пределом μ(s(n)) при спуске книзу (atBot).

LaTeX

$$$$\text{Antitone}(s) \Rightarrow \ \mathrm{Tendsto}(\mu \circ s)\ atBot\ (\mathcal{N}(\mu(\bigcup_n s_n))).$$$$

Lean4

theorem tendsto_measure_iUnion_atBot [Preorder ι] [IsCountablyGenerated (atBot : Filter ι)] {s : ι → Set α}
    (hm : Antitone s) : Tendsto (μ ∘ s) atBot (𝓝 (μ (⋃ n, s n))) :=
  tendsto_measure_iUnion_atTop (ι := ιᵒᵈ) hm.dual_left

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