iUnion_of_tendsto_zero — Mathlib

English

A restatement of the union-tends-to-zero principle under a monotone decomposition with tail differences vanishing; μ(⋃ n s_n) = sup μ(s_n).

Русский

Переформулирование принципа схождения объединения к нулю при монотонном разложении и исчезании хвостовых разностей; μ(⋃ n s_n) = sup μ(s_n).

LaTeX

$$$\\\\mu\\\\left\\\$\\\\\\\\bigcup_{n} s_n\\\\right\\\$ = \\\\sup_{n} μ(s_n)$$$

Lean4

/-- If `s : ι → Set α` is a sequence of sets, `S = ⋃ n, s n`, and `m (S \ s n)` tends to zero along
some nontrivial filter (usually `atTop` on `ι = ℕ`), then `m S = ⨆ n, m (s n)`. -/
theorem iUnion_of_tendsto_zero {ι} (m : OuterMeasure α) {s : ι → Set α} (l : Filter ι) [NeBot l]
    (h0 : Tendsto (fun k => m ((⋃ n, s n) \ s k)) l (𝓝 0)) : m (⋃ n, s n) = ⨆ n, m (s n) :=
  measure_iUnion_of_tendsto_zero m l h0

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