Go up to 4.7 Arithmetic Notions Go forward to 4.7.2 Arithmetic Quantifiers

4.7.1 Minimum and Maximum

minx F;

maxx F.

minx F := such x: F /\  (forall y: F[x <- y] => x <= y);

maxx F := such x: F /\  (forall y: F[x <- y] => x >= y).

Usually the variable x is dropped and has to be deduced from the context.

We can use this notion to define corresponding functions on sets as follows.

min(S)	:=	minx x in S;
max(S)	:=	maxx x in S;

Please note that the definition of "min" and "max" depends on the choice of the predicate <= . Furthermore, minimum and maximum are not necessarily defined.

• We have

  max_x (prime(x) /\  x | 100) = 5.

• The value of

  min({1/x: x in N_{> 0}})

  is undefined because for every x in {1/1, 1/2, 1/3, 1/4, ...} there is always an y in this set with y < x, namely 1/(x+1).