Theorem: Section2sheet3.tendsTo_def (FormalisingMathematics2024/Section02reals/Sheet3.lean)

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