Cauchy Sequence is a Cauchy Filter?

Stream: Is there code for X?

[Jack McCarthy]

I am working on a theorem about Hilbert spaces (i.e. complete inner-product spaces) and running into some difficulties because the Mathlib "CompleteSpace" is formalized in terms of filters, but my proof uses sequences. I am just looking to prove that my Cauchy sequence "TendsTo" some point in the Hilbert space. I'm wondering if there is any code that reduces the case of filters down to the case of a sequences. Ideally, I'm looking for a theorem like this:

import Mathlib.Probability.Moments.Basic
open Filter

theorem cauchy_sequence [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  {g : ℕ → E}
  (g_cauchy_seq : ∀ (δ : ℝ), δ > 0 → ∃ N : ℕ, ∀ n m : ℕ, n > N → m > N → ‖g n - g m‖ < δ)
  : Cauchy (map g atTop) := sorry

[Moritz Doll]

docs#cauchySeq_tendsto_of_complete and docs#cauchySeq_of_le_tendsto_0 should do the trick

[Moritz Doll]

(deleted)

[Aaron Liu]

That looks like docs#Metric.cauchySeq_iff

[Aaron Liu]

and with docs#dist_eq_norm

[Jack McCarthy]

Thanks so much!