Zulip Chat Archive

Stream: Is there code for X?

Topic: range(n,m)


view this post on Zulip Rémy Degenne (Dec 11 2020 at 10:22):

I just wrote several lemmas involving sums and products over finset.range(m)\finset.range(n) and now I am thinking that maybe those exist somewhere. Is there a type for the natural numbers j verifying n <= j < m? Even if there is no such type, is there a file with lemmas like the following:

lemma prod_range_sdiff_offset {α} [comm_monoid α] (N r : ) (f :   α) :
  ( (n : ) in (finset.range (N + r) \ finset.range N), f n)
    =  (n : ) in finset.range (r), f (N + n) := sorry

view this post on Zulip Eric Wieser (Dec 11 2020 at 10:24):

docs#list.range', perhaps? I guess that's not quite there either

view this post on Zulip Eric Wieser (Dec 11 2020 at 10:25):

docs#set.Ico?

view this post on Zulip Rémy Degenne (Dec 11 2020 at 10:34):

Thanks for giving me the Ico idea : I just found algebra.big_operators.intervals

view this post on Zulip Rémy Degenne (Dec 11 2020 at 10:34):

my lemma above looks similar to finset.prod_Ico_eq_prod_range

view this post on Zulip Rémy Degenne (Dec 11 2020 at 10:36):

and apparently there is a finset.Ico. The finset part of mathlib really is the scary part to me. it feels like there are 100 different types and that making them interact is not that easy

view this post on Zulip Kevin Buzzard (Dec 11 2020 at 13:17):

I have been worrying on and off about these lemmas for i=ab\sum_{i=a}^b for years now, and my current gut feeling is that finset.Ico works great and summing/prodding over that finset should be the default way to express stuff.


Last updated: May 17 2021 at 15:13 UTC