Commit 2026-01-26 12:23 5f8e8670

View on Github →

chore: add atBot version of convergence lemmas, rename original lemma for disambiguation (#34413) Cherry picked from #34055.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Lebesgue/DominatedConvergence.lean

Modified Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/ENNReal.lean

Modified Mathlib/Topology/Order/MonotoneConvergence.lean

added theorem tendsto_atBot_of_antitone

added theorem tendsto_atBot_of_monotone

added theorem tendsto_atTop_of_antitone

added theorem tendsto_atTop_of_monotone

deleted theorem tendsto_of_antitone

deleted theorem tendsto_of_monotone