Commit 2026-06-02 08:57 13cbaf84

View on Github →

chore: move dominated convergence to general versions for setToFun (#40104)

Estimated changes

Modified Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

added theorem MeasureTheory.hasSum_setToFun_of_dominated_convergence

added theorem MeasureTheory.setToFun_tsum

added theorem MeasureTheory.tendsto_setToFun_filter_of_norm_le_const