theorem MeasureTheory.lintegral_eq_iSup_eapprox_lintegral' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) : ∫⁻ (a : α), f a ∂μ = ⨆ (n : ℕ), (SimpleFunc.eapprox (AEMeasurable.mk f hf) n).lintegral μ

Generalization of MeasureTheory.lintegral_eq_iSup_eapprox_lintegral assuming a.e. measurability of f

theorem MeasureTheory.lintegral_comp' {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [MeasurableSpace β] {f : β → ENNReal} {g : α → β} (hf : AEMeasurable f (Measure.map g μ)) (hg : AEMeasurable g μ) : lintegral μ (f ∘ g) = ∫⁻ (a : β), f a ∂Measure.map g μ

Generalization of MeasureTheory.lintegral_comp assuming a.e. measurability of f and g