mathlib

260d472e - feat(order/topology/**/uniform*): Lemmas about uniform convergence (#14587)

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. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>