Theorems · Theorem · measure theory

MeasureTheory.measure_iUnion_of_tendsto_zero

∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {ι : Type u_4}
  (μ : F) {s : ι → Set α} (l : Filter ι) [l.NeBot],
  Filter.Tendsto (fun k => μ ((⋃ n, s n) \ s k)) l (nhds 0) → μ (⋃ n, s n) = ⨆ n, μ (s n)

Let μ be an (outer) measure; let s : ι → Set α be a sequence of sets, S = ⋃ n, s n. If μ (S \ s n) tends to zero along some nontrivial filter (usually Filter.atTop on ι = ℕ), then μ S = ⨆ n, μ (s n).

Defined in

Mathlib.MeasureTheory.OuterMeasure.Basic

Cited by

2 results in Mathlib

Foundations

Depth 136 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FunLikeMeasureTheory.OuterMeasureClassFilter.NeBot