mathlib3

feat(topology/uniform_space/uniform_convergence_topology): prove completeness

#18017

Open