integral_iUnion_fintype — Mathlib

English

The integral over the empty set is zero for any f.

Русский

Интеграл по пустому множеству равен нулю для любого f.

LaTeX

$$$\\int_{x \\in \\emptyset} f(x) \\,d\\mu = 0$$$

Lean4

theorem integral_iUnion_fintype {ι : Type*} [Fintype ι] {s : ι → Set X} (hs : ∀ i, MeasurableSet (s i))
    (h's : Pairwise (Disjoint on s)) (hf : ∀ i, IntegrableOn f (s i) μ) :
    ∫ x in ⋃ i, s i, f x ∂μ = ∑ i, ∫ x in s i, f x ∂μ :=
  by
  convert integral_biUnion_finset Finset.univ (fun i _ => hs i) _ fun i _ => hf i
  · simp
  · simp [pairwise_univ, h's]

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