fintype or finset for integer ranges

Stream: maths

[Kevin Buzzard]

example (a b : ℤ) : fintype {z : ℤ // a < z ∧ z < b} := sorry . How do I do this? I'm not very good at finite stuff. Or finset {z : ℤ | a < z ∧ z < b} or whatever. I found finiteness statements for nats but not ints.

[Kevin Buzzard]

ooh I've found set.Ico but

import data.set.intervals data.fintype
example : fintype.card (set.Ico (3 : ℤ) 5) := by apply_instance -- fails

doesn't work.

[Chris Hughes]

Is there a list.ico or finset.ico? That would make it easy to prove.

[Chris Hughes]

You could also prove an equiv with fin

[Kevin Buzzard]

finset.Ico : ℕ → ℕ → finset ℕ

[Kevin Buzzard]

list.Ico : ℕ → ℕ → list ℕ