Zulip Chat Archive

Stream: maths

Topic: supr and range


view this post on Zulip Sebastien Gouezel (Nov 13 2018 at 17:22):

There are the following definitions in mathlib:

def supr (s : ι  α) : α := Sup {a : α | i : ι, a = s i}

def range (f : ι  α) : set α := {x | y, f y = x}

You can see that the order after the existential quantifiers is swapped. Therefore, supr fand Sup (range f) are not defeq. Is this on purpose or by accident? More importantly, if I want to unify the two, which one should I choose? I would rather use the first one ∃i, a = s i, which could help the simplifier to rewrite a if at some point we end up with an assumption of the form a = s i, but there might be some reason I am missing for the current definition of range.

view this post on Zulip Sebastien Gouezel (Nov 13 2018 at 17:24):

Additional data point:

def image (f : α  β) (s : set α) : set β := {b |  a, a  s  f a = b}

view this post on Zulip Johannes Hölzl (Nov 13 2018 at 17:29):

oops, I never realized this. I would keep range (as it is similar to image), and change supr.

view this post on Zulip Mario Carneiro (Nov 13 2018 at 17:35):

the variable on the right thing is also consistent with the definition of eq

view this post on Zulip Sebastien Gouezel (Nov 13 2018 at 17:41):

the variable on the right thing is also consistent with the definition of eq

Not sure I get it (too many variables around :). Do you mean that you also think that the definition of supr and image is right, and that I should fix range?

view this post on Zulip Johannes Hölzl (Nov 13 2018 at 17:50):

range and image are the same (the function application is left, and the set-comprehension variable is right). For supr it is the other way round

view this post on Zulip Johan Commelin (Nov 13 2018 at 17:52):

Shouldn't supr be redefined to use range explicitly?

view this post on Zulip Johannes Hölzl (Nov 13 2018 at 17:54):

Yes, def supr (s : ι → α) : α := Sup (range s)

view this post on Zulip Johan Commelin (Nov 13 2018 at 17:55):

Maybe then we should rename infi to infr, and then the r stands for range :upside_down: :see_no_evil:

view this post on Zulip Sebastien Gouezel (Nov 14 2018 at 08:56):

Yes, def supr (s : ι → α) : α := Sup (range s)

Done in #PR474. It was slightly more painful than I expected, as I had to fix the library all over the place...


Last updated: May 06 2021 at 18:20 UTC