Zulip Chat Archive

Stream: new members

Topic: sequence 1/n converges, "type mismatch"


Luca Seemungal (Oct 03 2019 at 15:05):

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 (Oct 03 2019 at 15:08):

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

Luca Seemungal (Oct 03 2019 at 15:09):

cheers, that works.


Last updated: Dec 20 2023 at 11:08 UTC