measure_iUnion — Mathlib

English

Continuity from above for an antitone family: μ(⋃ i s_i) = ⨆ i μ(s_i) under suitable hypotheses.

Русский

Непрерывность сверху для антитонной последовательности: μ(⋃ i s_i) = ⨆ i μ(s_i) при подходящих предположениях.

LaTeX

$$$ \mu(\bigcup_i s_i) = \uparrow_i μ(s_i) $$$

Lean4

theorem _root_.Antitone.measure_iUnion [Preorder ι] [IsDirected ι (· ≥ ·)] [(atBot : Filter ι).IsCountablyGenerated]
    {s : ι → Set α} (hs : Antitone s) : μ (⋃ i, s i) = ⨆ i, μ (s i) :=
  hs.dual_left.measure_iUnion

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