Commit 2024-10-01 20:15 ebdf9cca
View on Github →feat(ENNReal): Convenience lemmas (#17277)
Add a few convenience lemmas using the equality a = b + c to deduce that b is finite from the fact that a is. As shown by the golfs, this is useful.
Also deprecate sub_eq_of_add_eq, which is the "annoyingly swap things around" version of eq_sub_of_add_eq/sub_eq_of_eq_add.
From LeanAPAP