measure_iUnion_eq_iSup_accumulate

English

Re-statement: with countable I and s, the measure of the double union equals the supremum over both indices.

Русский

Повторное утверждение: при счётном I и s мера двойного объединения равна supremum по обоим индексам.

LaTeX

$$$ μ(⋃ b ∈ I, ⋃ h ∈ I, s(b)) = \sup_{b ∈ I} μ(⋃_{h ∈ I} s(b)) $$$

Lean4

/-- Continuity from below: the measure of the union of a sequence of
(not necessarily measurable) sets is the supremum of the measures of the partial unions. -/
theorem measure_iUnion_eq_iSup_accumulate [Preorder ι] [IsDirected ι (· ≤ ·)] [(atTop : Filter ι).IsCountablyGenerated]
    {f : ι → Set α} : μ (⋃ i, f i) = ⨆ i, μ (Accumulate f i) :=
  by
  rw [← iUnion_accumulate]
  exact monotone_accumulate.measure_iUnion

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