Zulip Chat Archive

Stream: maths

Topic: fintype or finset for integer ranges


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Sep 19 2019 at 22:17):

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

view this post on Zulip Chris Hughes (Sep 19 2019 at 22:17):

You could also prove an equiv with fin

view this post on Zulip Kevin Buzzard (Sep 19 2019 at 22:17):

finset.Ico : ℕ → ℕ → finset ℕ

view this post on Zulip Kevin Buzzard (Sep 19 2019 at 22:18):

list.Ico : ℕ → ℕ → list ℕ


Last updated: May 10 2021 at 07:15 UTC