argmin in mathlib

Stream: general

[Frederick Pu]

are there any existing definitions in mathlib that simulate an argmin, that is ArgMin f s x means that x is the value in the set s where the value of the function f is minimzed

[Aaron Liu]

Are you looking for docs#IsMinOn

[Violeta Hernández]

Do you mean docs#Function.argmin ?

[Violeta Hernández]

Do note I make a breaking change to said function on #20777, so you might want to wait a few days until that drops.

[Yury G. Kudryashov]

Are you looking for a predicate or a function?

[Frederick Pu]

predicate

[Yury G. Kudryashov]

Then IsMinOn