next up previous contents
Next: Division 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)
  max_assoc = ... : {m,n,o:nat}Eq (max (max m n) o) (max m (max n o))
  max_suc_pred = ... :
    {m,n:nat}Eq (max m (suc n)) (suc (max (pred 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
1998-06-15