Commit 2024-09-30 02:32 cdd209aa

View on Github →

feat: When 1 + a ≤ (1 - b) * (1 + c) (#17214) In analysis, we often manipulate quantities near 1 as if they were additive in their difference to 1. This PR adds lemmas supporting that kind of reasoning. From LeanAPAP

Estimated changes