mu-Operator

Let  be a function such that for any , ..., , there is at least one  such that . Then the -operator  gives the least number  such that . More generally, for a relation , the -operator gives the least , if any, such that  is true, and this least value of  is denoted  (Mendelson 1997, p. 175).

For example, given a criterion crit and a list x1, x2, ..., xn, the -operator could be written in the Wolfram Language as Select[Sort[x1, x2, ..., xn], crit, 1].

REFERENCES:

Mendelson, E. Introduction to Mathematical Logic, 4th ed. London: Chapman & Hall, 1997.