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