Next: List Up: The Natural Numbers Previous: The predicate Even

## Max and Min

The final file for natural numbers defines the functions max and min and proves various theorems about them. It requires most of the other nat library files. The functions min and max are defined explicitly using double iteration rather than by showing that the order relation on nat is complete.

** Module lib_max_min Imports lib_nat_Prop_rels
max = ... : nat->nat->nat
min = ... : nat->nat->nat
max_Le_left = ... : {x,y:nat}Le x (max x y)
max_Le_right = ... : {x,y:nat}Le y (max x y)
max_is_least = ... : {x,y,z:nat}(Le x z)->(Le y z)->Le (max x y) z
min_Le_left = ... : {x,y:nat}Le (min x y) y
min_Le_right = ... : {x,y:nat}Le (min x y) x
min_is_greatest = ... : {x,y,z:nat}(Le z x)->(Le z y)->Le z (min x y)
max_sym = ... : {n,m:nat}Eq (max n m) (max m n)
min_sym = ... : {n,m:nat}Eq (min n m) (min m n)
Le_min_left = ... : {x,y:nat}(Le x y)->Eq (min x y) x
Le_min_right = ... : {x,y:nat}(Le y x)->Eq (min x y) y
Le_max_right = ... : {x,y:nat}(Le x y)->Eq (max x y) y
Le_max_left = ... : {x,y:nat}(Le y x)->Eq (max x y) x
min_idemp = ... : {a:nat}Eq (min a a) a
max_resp_times = ... :
{x,y,a:nat}Eq (max (times a x) (times a y)) (times a (max x y))
min_resp_times = ... :
{x,y,a:nat}Eq (min (times a x) (times a y)) (times a (min x y))
max_resp_plus = ... :
{a,b,x:nat}Eq (max (plus a x) (plus b x)) (plus (max a b) x)
min_resp_plus = ... :
{a,b,x:nat}Eq (min (plus a x) (plus b x)) (plus (min a b) x)

Lego
Fri May 24 19:01:27 BST 1996