Commit 2024-08-26 00:19 fb8f2f97

feat(UniformSpace.Basic): define product of uniformities (#14718) Define a product of uniformities (UniformityProd) and prove a couple of lemmas (ball_prod, and the dubiously-named UniformityProd_of_uniform_prod). The goal is to make the manipulation of uniformities in product spaces more user-friendly. The statement of another lemmas is reworded to use UniformityProd. I also reformulated a few lemmas to make them easier to grasp in the documentation. Zulip thread Edit: Paging Patrick, since you contributed to this file.