Theorem: near_cluster (LCTutorial/Exercises/Topics/SequenceLimits.lean)

State before:
u : ℕ → ℝ
a : ℝ
⊢ cluster_point u a → ∀ ε > 0, ∀ (N : ℕ), ∃ n ≥ N, |u n - a| ≤ ε
Tactic:
sorry
State after:
no goals