Argmax for Finset

Stream: general

[Konstantin Weitz]

I have a Finset of type A, and would like to get the largest element with respect to a function f : A -> Real. What's the best way to do this? I know about Finset.max and Finset.max', but didn't see an Finset.argmax or something like that.

[Aaron Liu]

docs#Finset.image it and then max maybe

[Yaël Dillies]

docs#Finset.sup' is the idiomatic spellingSorry, I see you want the index with maximal value, not the maximal value itself

[Aaron Liu]

or maybe docs#List.argmax with some docs#Finset.toList

[Konstantin Weitz]

Thanks. I also see that Finset.max takes a LinearOrder. Is there an easy way to instantiate a linear order with a mapping from the set to Real (like my function f)?

[Aaron Liu]

If it's injective you can pull back the linear order from Real

[Aaron Liu]

docs#LinearOrder.lift'

[Yaël Dillies]

You really shouldn't be pulling any linear order back! What Konstantin wants is simply the existence of an argument with maximal value + choice to actually get one

[Bhavik Mehta]

docs#Finset.exists_max_image is the usual way to get this existence