intro ε ε_pos
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε