sequence 1/n converges, "type mismatch"

Stream: new members

[Luca Seemungal]

Hi, I have the code below:

import data.real.basic

namespace learning
-- Sequences

def seq_conv_to (a : ℕ → ℝ) (l : ℝ) :=
∀ ε > 0, ∃ N, ∀ n > N, abs(a n - l) < ε

example : seq_conv_to (λ x, 1/x) (0) :=
begin
rw seq_conv_to,
intros,
simp,
existsi ceil(1/ε),
sorry
end

end learning

and I get the error

existsi tactic failed, type mismatch between given term witness and expected type
state:
ε : ℝ,
H : ε > 0
⊢ ∀ (n : ℕ), ⌈1 / ε⌉ + 1 < n → abs (↑n)⁻¹ < ε

on the line existsi ceil(1/ε)

Home come? ceil gives a natural number, and that's what N should be, right? Where's the type mismatch?

[Rob Lewis]

ceil gives an integer, not a natural. You may want to use nat_ceil instead.

[Luca Seemungal]

cheers, that works.