Commit 2022-09-20 09:35 dc680a80

View on Github →

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.

Estimated changes

Modified src/topology/uniform_space/cauchy.lean

added theorem cauchy_seq.totally_bounded_range