## Stream: maths

### Topic: Return type of finset.sup

#### Chris Hughes (Jun 28 2019 at 12:46):

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 (Jun 28 2019 at 12:49):

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

#### Reid Barton (Jun 28 2019 at 12:51):

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 (Jun 28 2019 at 12:51):

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

#### Mario Carneiro (Jun 28 2019 at 12:52):

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

#### Reid Barton (Jun 28 2019 at 12:52):

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

#### Chris Hughes (Jun 28 2019 at 13:03):

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 (Jun 28 2019 at 13:05):

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 (Jun 28 2019 at 13:07):

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

#### Mario Carneiro (Jun 28 2019 at 13:08):

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

Last updated: May 18 2021 at 07:19 UTC