## Stream: maths

### Topic: fintype or finset for integer ranges

#### Kevin Buzzard (Sep 19 2019 at 21:07):

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 (Sep 19 2019 at 21:17):

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 (Sep 19 2019 at 22:17):

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

#### Chris Hughes (Sep 19 2019 at 22:17):

You could also prove an equiv with fin

#### Kevin Buzzard (Sep 19 2019 at 22:17):

finset.Ico : ℕ → ℕ → finset ℕ

#### Kevin Buzzard (Sep 19 2019 at 22:18):

list.Ico : ℕ → ℕ → list ℕ

Last updated: May 10 2021 at 07:15 UTC