Commit 2026-06-27 02:57 0ee7df22

View on Github →

chore: use NeBot in left and right limits (#41079)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

Modified Mathlib/Topology/Order/LeftRightLim.lean

modified theorem Monotone.leftLim_eq_sSup

modified theorem Monotone.rightLim_eq_sInf