Return type of `finset.sup`

Stream: maths

[Chris Hughes]

Currently the type of finset.sup is

finset.sup :
  Π {α : Type u_1} {β : Type u_2} [_inst_1 : lattice.semilattice_sup_bot α], finset β → (β → α) → α

I think it would make more sense to return a β. There's no function that does this at the moment, and it would be useful.

[Chris Hughes]

I guess the β is not unique though. In my application the function is injective.

[Reid Barton]

The ordering on \a might not be total, in which there is no "corresponding" value of \b to return, if I understand what you want to do

[Mario Carneiro]

You could write a trunc of a value that maps to the sup

[Mario Carneiro]

and in the case where the function is injective you can get the value out

[Reid Barton]

What you're looking for is usually called "argmax"

[Chris Hughes]

Okay, so I'm going to have to write this argmax function. We're kind of inconsistent at the moment with how we handle empty lists on the variants of max list.maximum, finset.sup, finset.max. What should argmax do?

[Mario Carneiro]

If it has a complex type like I suggested, then it's basically a proof procedure, so I think it should be fine to assume the input is nonempty

[Mario Carneiro]

We could also have a more weakly typed version that has some default behavior in that case

[Mario Carneiro]

just so you can write argmax_(x \in S) f x as a term in reasonable conditions