Theorems · Theorem · measure theory

MeasureTheory.lintegral_iInf_directed_of_measurable

∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [Countable β] {f : β → α → ENNReal}
  {μ : MeasureTheory.Measure α},
  μ ≠ 0 →
    (∀ (b : β), Measurable (f b)) →
      (∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤) →
        Directed (fun x1 x2 => x1 ≥ x2) f → ∫⁻ (a : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ

Monotone convergence theorem for an infimum over a directed family and indexed by a countable type.

Defined in

Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceCountable