mathlib

dc680a80 - feat(topology/uniform_space): Every Cauchy sequence over ℕ is totally bounded (#16563)

feat(topology/uniform_space): Every Cauchy sequence over ℕ is totally bounded (#16563) This PR proves that the image of every Cauchy sequence `ℕ → α` is totally bounded. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>