supr and range

Stream: maths

[Sebastien Gouezel]

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.

[Sebastien Gouezel]

Additional data point:

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

[Johannes Hölzl]

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

[Mario Carneiro]

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

[Sebastien Gouezel]

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?

[Johannes Hölzl]

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

[Johan Commelin]

Shouldn't supr be redefined to use range explicitly?

[Johannes Hölzl]

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

[Johan Commelin]

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

[Sebastien Gouezel]

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...