metric.lean

import analysis.metric_space

variables {α : Type*}  [metric_space α] {β : Type*}
open filter

lemma tendsto_nhds_iff (u : β → α) (f : filter β) (a : α) : tendsto u f (nhds a) ↔
  ∀ ε > 0, {n | dist (u n) a < ε} ∈ f.sets := 
⟨λ H ε εpos, H (ball_mem_nhds a εpos),
 λ H s s_nhd, let ⟨ε, εpos, sub⟩ := mem_nhds_iff_metric.1 s_nhd in
 f.sets_of_superset (H ε εpos) (λ b b_in, sub b_in)⟩

lemma seq_tendsto_iff (u : ℕ → α) (a : α) : tendsto u at_top (nhds a) ↔ 
  ∀ ε > 0, ∃ (N : ℕ), ∀ {n}, n ≥ N → dist (u n) a < ε :=
by simp [tendsto_nhds_iff, mem_at_top_sets]