Commit 2026-01-28 13:42 1ad113ee

View on Github →

feat: more on left and right limits (#34412) Various continuity properties of left and right limit. For instance, the left limit is left-continuous. Also, if a function has a limit at +\infty, then its left-limit and right-limit also tend to the same limit at +\infty. Cherry picked from #34055.

Estimated changes

Modified Mathlib/Topology/Order/LeftRightLim.lean

modified theorem Monotone.tendsto_leftLim

added theorem continuousWithinAt_leftLim_Iic

added theorem continuousWithinAt_rightLim_Ici

added theorem leftLim_eq_of_isBot

added theorem leftLim_eq_of_not_tendsto

added theorem leftLim_leftLim

added theorem leftLim_rightLim

added theorem mapClusterPt_leftLim

added theorem mapClusterPt_rightLim

added theorem rightLim_eq_of_isTop

added theorem rightLim_eq_of_not_tendsto

added theorem rightLim_leftLim

added theorem rightLim_rightLim

added theorem tendsto_atBot_of_mapClusterPt

added theorem tendsto_atTop_of_mapClusterPt

added theorem tendsto_leftLim_atBot_of_tendsto

added theorem tendsto_leftLim_atTop_of_tendsto

added theorem tendsto_leftLim_of_tendsto

added theorem tendsto_rightLim_atBot_of_tendsto

added theorem tendsto_rightLim_atTop_of_tendsto

added theorem tendsto_rightLim_of_tendsto