%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Sup and Inf of bounded functions  %
%  (require nonempty domain)         %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

real_fun_supinf [ T : NONEMPTY_TYPE FROM real ] : THEORY

  BEGIN

  IMPORTING reals@real_fun_props, reals@real_facts


  f : VAR [T -> real]

  x : VAR T

  a : VAR real

  epsilon : VAR posreal


  %---------------
  %  Sup and Inf 
  %---------------

  g : VAR { f | bounded_above?(f) }

  h : VAR { f | bounded_below?(f) }


  nonempty_image: JUDGEMENT Im(f) HAS_TYPE (nonempty?[real])

  bounded_above_image: JUDGEMENT Im(g) HAS_TYPE (bounded_above?)

  bounded_below_image: JUDGEMENT Im(h) HAS_TYPE (bounded_below?)


  sup(g) : real = lub(Im(g))

  inf(h) : real = glb(Im(h))


  %--------------
  %  Properties
  %--------------

  supfun_is_bound : LEMMA   g(x) <= sup(g)

  supfun_is_sup : LEMMA
 FORALL epsilon : EXISTS x : sup(g) - epsilon < g(x)

  supfun_is_sup2 : LEMMA
 sup(g) <= a  IFF  FORALL x : g(x) <= a
 

  inffun_is_bound : LEMMA   inf(h) <= h(x)

  inffun_is_inf : LEMMA
 FORALL epsilon : EXISTS x : h(x) < inf(h) + epsilon

  inffun_is_inf2 : LEMMA
 a <= inf(h)  IFF  FORALL x : a <= h(x)



  supfun_neg : LEMMA  sup(- h) = - inf(h)

  inffun_neg : LEMMA  inf(- g) = - sup(g)


  %--------------------------------------
  %  Relations with maximum and minimum 
  %--------------------------------------

  max_upper_bound : LEMMA
 is_maximum(x, f) IFF bounded_above?(f) AND sup(f) = f(x)
  

  min_lower_bound : LEMMA
 is_minimum(x, f) IFF bounded_below?(f) AND inf(f) = f(x)

  END real_fun_supinf