Commit 2022-06-17 17:39 260d472e

feat(order/topology/**/uniform*): Lemmas about uniform convergence (#14587) To prove facts about uniform convergence, it is often useful to manipulate the various functions without dealing with the ε's and δ's. To do so, you need auxiliary lemmas about adding/muliplying/etc Cauchy sequences. This commit adds several such lemmas. It supports #14090, which we're slowly transforming to use these lemmas instead of doing direct ε/δ manipulation.