Theorem: Section2sheet3solutions.tendsTo_def (FormalisingMathematics2024/Solutions/Section02reals/Sheet3.lean)

State before:
a : ℕ → ℝ
t : ℝ
⊢ TendsTo a t ↔ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
Tactic:
rfl
State after:
no goals