Theorems · Theorem · measure theory

MeasureTheory.tendsto_setIntegral_of_monotone

∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} {ι : Type u_5} [inst_2 : Preorder ι] [Filter.atTop.IsCountablyGenerated]
  {s : ι → Set X},
  (∀ (i : ι), MeasurableSet (s i)) →
    Monotone s →
      MeasureTheory.IntegrableOn f (⋃ n, s n) μ →
        Filter.Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) Filter.atTop (nhds (∫ (x : X) in ⋃ n, s n, f x ∂μ))

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Set

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpacePreorderFilter.IsCountablyGenerated