Proving seq continuity implies continuity

Stream: new members

[Gareth Ma]

UPDATE: Nevermind, I think I found my mistake. My fx definition is wrong (mathematically, not "lean"-wise).

---

Hi, I am still quite new to lean, and I am struggling to finish this proof. Currently I have these primitives, the main one being H:

f: ℝ → ℝ
x₀ε: ℝ
ε_pos: ε > 0
δ: ℕ → ℝ := λ (n : ℕ), 1 / (n + 1)
fx: ℕ → ℝ := λ (n : ℕ), f (x₀ + δ n)
H: ∀ (n : ℕ), ∃ (x : ℝ), |x - x₀| ≤ 1 / (n + 1) ∧ ε < |f x - f x₀|
⊢ ¬seq_limit fx (f x₀)

H is a special case of f not being pointwise convergence at x0. The idea is that since I can find x closer and closer to x0 yet is not epsilon-close to f x0, it means it cannot be sequential convergence, since {x} -> x0 yet {f x} does not -> x0. However, I can't seem to finish off the proof. Can someone help? Here is my code:

-- 0074
example :
  (∀ u : ℕ → ℝ, seq_limit u x₀ → seq_limit (f ∘ u) (f x₀)) →
  continuous_at_pt f x₀ :=
begin
  intro h,
  unfold continuous_at_pt,
  by_contradiction, push_neg at h,
  rcases h with ⟨ε, ε_pos, h'⟩,

  -- "approaching functions" definitions
  let δ : ℕ → ℝ := λ n, 1 / (n + 1),
  let fx : ℕ → ℝ := λ n, f (x₀ + δ n),

  -- auxillary lemma
  have H : ∀ n : ℕ, ∃ (x : ℝ), |x - x₀| ≤ 1 / (n + 1) ∧ ε < |f x - f x₀|,
  { intro n, exact h' (δ n) (by apply nat.one_div_pos_of_nat), },

  -- convergence lemmas
  have f_x_conv : seq_limit fx (f x₀),
  { from h (λ n, x₀ + δ n) (limit_const_add_inv_succ x₀), },

  have f_x_not_conv : ¬seq_limit fx (f x₀),
  {
    clear h f_x_conv h',
    unfold seq_limit,
    push_neg,
    use ε,
    split,
    { exact ε_pos, },
    {
      -- ???
    }
  }
end