Commit 2022-10-08 03:03 052b6cbe
View on Github →feat(topology/algebra/order/left_right): left and right limits (#16551) We define left and right limits of a function, and prove that a monotone function is continuous at a point if and only if its left and right limits coincide. We also refactor the file on Stieltjes functions using this general definition instead of the ad hoc definition that is currently used.