Theorems · Theorem · measure theory

MeasureTheory.AECover.lintegral_tendsto_of_countably_generated

∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [l.IsCountablyGenerated] {φ : ι → Set α},
  MeasureTheory.AECover μ l φ →
    ∀ {f : α → ENNReal},
      AEMeasurable f μ → Filter.Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (nhds (∫⁻ (x : α), f x ∂μ))

Defined in

Mathlib.MeasureTheory.Integral.IntegralEqImproper

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceFilter.IsCountablyGenerated