setLIntegral_iUnion_of_directed — Mathlib

English

If ι is a countable index set and s_i is a directed family of sets, then the lintegral over the union equals the supremum of the integrals over s_i.

Русский

Если индексовая система счётна и семейство s_i упорядочено по включению, то линегральный интеграл по объединению равен верхней границе интегралов по s_i.

LaTeX

$$$$\\int_{a\\in \\bigcup_{i} s_i} f(a) \\, d\\mu = \\sup_{i} \\int_{a\\in s_i} f(a) \\, d\\mu.$$$$

Lean4

theorem setLIntegral_iUnion_of_directed {ι : Type*} [Countable ι] (f : α → ℝ≥0∞) {s : ι → Set α}
    (hd : Directed (· ⊆ ·) s) : ∫⁻ x in ⋃ i, s i, f x ∂μ = ⨆ i, ∫⁻ x in s i, f x ∂μ := by
  simp only [lintegral_def, iSup_comm (ι := ι), SimpleFunc.lintegral_restrict_iUnion_of_directed _ hd]

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