maximum of a function

Stream: Is there code for X?

[Adam Topaz]

Suppose I have a function $f : S \to L$ from a type S with [fintype S] to a linearly ordered type L. What's the idiomatic way to obtain the maximum of f? docs#function.max

[Mario Carneiro]

I would use docs#finset.max

[Mario Carneiro]

actually docs#finset.sup is probably more convenient for this

[Adam Topaz]

Thanks.

[Scott Morrison]

docs#finset.sup' is often also convenient