Theorem: tends_to_def (FM2023Exrcise/section02_reals/sheet3.lean)

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