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