Skip to content

[Merged by Bors] - feat: another version of dominated convergence for AEMeasurable functions#39768

Closed
mathlib-splicebot[bot] wants to merge 1 commit into
masterfrom
splice-bot/pr-39517-Mathlib-MeasureTheory-Integral-Lebesgue-DominatedConvergence.lean-c45c887233-3tiupl5
Closed

[Merged by Bors] - feat: another version of dominated convergence for AEMeasurable functions#39768
mathlib-splicebot[bot] wants to merge 1 commit into
masterfrom
splice-bot/pr-39517-Mathlib-MeasureTheory-Integral-Lebesgue-DominatedConvergence.lean-c45c887233-3tiupl5