Next: Specification and development of Up: The Integers Previous: Propositional relations on integers

## Max and min on integers

In this section max and min are defined on integers and a number of theorems proved about them.

``` ** Module lib_int_max_min Imports lib_int_basics_thms lib_int_Prop_rels
lib_max_min
min_zed = ... : int.1->int.1->int.1
max_zed = ... : int.1->int.1->int.1
max_resp_eq = ... :
{a,b,x,y:int.1}(eq a b)->(eq x y)->eq (max_zed a x) (max_zed b y)
min_resp_eq = ... :
{a,b,x,y:int.1}(eq a b)->(eq x y)->eq (min_zed a x) (min_zed b y)
max_Le_left_zed = ... : {x,y:int.1}Le_zed x (max_zed x y)
max_Le_right_zed = ... : {x,y:int.1}Le_zed y (max_zed x y)
min_Le_left_zed = ... : {x,y:int.1}Le_zed (min_zed x y) x
min_Le_right_zed = ... : {x,y:int.1}Le_zed (min_zed x y) y
max_is_least_zed = ... :
{x,y,z:int.1}(Le_zed x z)->(Le_zed y z)->Le_zed (max_zed x y) z
min_is_greatest_zed = ... :
{x,y,z:int.1}(Le_zed z x)->(Le_zed z y)->Le_zed z (min_zed x y)
max_resp_plus_zed = ... :
{x,y,z:int.1}
eq (max_zed (plus_zed z x) (plus_zed z y))
(plus_zed z (max_zed x y))
min_resp_plus_zed = ... :
{x,y,z:int.1}
eq (min_zed (plus_zed z x) (plus_zed z y))
(plus_zed z (min_zed x y))
Le_min_left_zed = ... : {x,y:int.1}(Le_zed x y)->eq (min_zed x y) x
Le_min_right_zed = ... : {x,y:int.1}(Le_zed y x)->eq (min_zed x y) y
Le_max_right_zed = ... : {x,y:int.1}(Le_zed x y)->eq (max_zed x y) y
Le_max_left_zed = ... : {x,y:int.1}(Le_zed y x)->eq (max_zed x y) x
max_resp_times_zed = ... :
{x,y,a:int.1}(Le_zed zero_zed a)->
eq (max_zed (times_zed a x) (times_zed a y))
(times_zed a (max_zed x y))
min_resp_times_zed = ... :
{x,y,a:int.1}(Le_zed zero_zed a)->
eq (min_zed (times_zed a x) (times_zed a y))
(times_zed a (min_zed x y))
max_sym_zed = ... : {x,y:int.1}eq (max_zed x y) (max_zed y x)
min_sym_zed = ... : {x,y:int.1}eq (min_zed x y) (min_zed y x)
min_zed_idemp = ... : {a|zed}Eq_zed (min_zed a a) a
```

Conor McBride
11/13/1998