Go up to 4.7 Arithmetic Notions Go forward to 4.7.2 Arithmetic Quantifiers |
The value of the first term is the smallest value of x such that F holds; the value of the second term is the largest such value, i.e.,
min_{x} F; max_{x} F.
min_{x} F := such x: F /\ (forall y: F[x <- y] => x <= y); max_{x} 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) := min_{x} x in S; max(S) := max_{x} 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.
max_{x} (prime(x) /\ x | 100) = 5.
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).