A metastable dominated convergence theorem.

by Jeremy Avigad, Edward T Dean, Jason Rute.

We prove the equivalence between the two first displayed equations mentioned on page 2.

theorem metastableEquiv (a : ℕ → ℝ) : (∀ ε > 0, ∃ (m : ℕ), ∀ n ≥ m, ∀ n' ≥ m, |a n - a n'| < ε) ↔ ∀ ε > 0, ∀ (F : ℕ → ℕ), ∃ (m : ℕ), ∀ n ∈ Set.Icc m (F m), ∀ n' ∈ Set.Icc m (F m), |a n - a n'| < ε