Theorems · Theorem · measure theory

MeasureTheory.Measure.lintegral_join

∀ {α : Type u_1} {mα : MeasurableSpace α} {m : MeasureTheory.Measure (MeasureTheory.Measure α)} {f : α → ENNReal},
  AEMeasurable f m.join → ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : MeasureTheory.Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Defined in

Mathlib.MeasureTheory.Measure.GiryMonad

Cited by

2 results in Mathlib

Foundations

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