Cauchy sequences are totally bounded

Stream: Is there code for X?

[Moritz Doll]

Do we have the statement that the image of a Cauchy sequence (on ℕ) is totally bounded? I only found docs#totally_bounded_iff_filter but this is not to prove anything about sequences.

[Matt Diamond]

docs#cau_seq.bounded perhaps?

[Matt Diamond]

actually that might be the wrong one since it uses cau_seq instead of cauchy_seq

[Moritz Doll]

#16563 in case anyone is interested in seeing a proof