mathlib3

9fa14a60 - feat(topology/uniform_space): properties of uniform convergence (#9958)

feat(topology/uniform_space): properties of uniform convergence (#9958) * From the sphere eversion project * multiple proofs were golfed by @PatrickMassot * Probably some proofs can be golfed quite heavily Co-authored by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Patrick Massot <patrickmassot@free.fr>