Infimum of a Finite set of values in a linear order

Stream: Is there code for X?

[Antoine Chambert-Loir]

What would be the simplest way to get the infimum of a finite and nonempty family of functions valued in a linear order? (One could use sInf if the linear order were complete.)

[Aaron Liu]

we have docs#Finset.min' for exactly this purpose

[Aaron Liu]

oh it's functions

[Aaron Liu]

then I guess it's not a linear order so use docs#Finset.inf'