Commit 2024-11-16 02:46 46215793

feat: continuousAt_iff_isLittleO (#19051) This is another PR breaking #9598 into smaller pieces. We prove the theorem continuousAt_iff_isLittleO, that a function f is continuous at a point x iff f y - f x is little-o of 1.