continuity_interval [ a : real, b : {x : real | a <= x }] : THEORY
%-----------------------------------------------------------------
%  continuous functions on a closed interval                     
%-----------------------------------------------------------------
BEGIN

  %-----------------------------
  %  Interval [a, b] as a type
  %-----------------------------

  x : VAR real
  J : NONEMPTY_TYPE = { x | a <= x AND x <= b}
  f : VAR [J -> real]
  u : VAR sequence[J]
  c : VAR J
  n, i : VAR nat

  IMPORTING continuity_props

  %-----------------------------------------------
  %  Reformulation of Bolzano/Weirstrass theorem
  %-----------------------------------------------

  bolz_weier : LEMMA   EXISTS c : accumulation(u, c)


  %-------------------------------------
  %  If f is continuous, it is bounded
  %-------------------------------------

  unbounded_sequence : LEMMA bounded_above?(f) OR 
                               EXISTS u : FORALL n : f(u(n)) > n

  bounded_from_above : LEMMA continuous?(f) IMPLIES bounded_above?(f)

  bounded_from_below : LEMMA continuous?(f) IMPLIES bounded_below?(f)


  %--------------------------------------
  %  f has a maximum and a minimum in J
  %--------------------------------------

  max_extraction : LEMMA continuous?(f) IMPLIES
                    EXISTS u : FORALL n : sup(f) - f(u(n)) < 1/(n+1)

  sup_is_reached : LEMMA continuous?(f) IMPLIES EXISTS c : f(c) = sup(f)

  maximum_exists : LEMMA continuous?(f) IMPLIES EXISTS c : is_maximum(c, f)

  max_pt(f:{f|continuous?(f)}): {xj: J | is_maximum(xj,f)}     % ADDED BY RWB

  inf_is_reached : LEMMA continuous?(f) IMPLIES EXISTS c : f(c) = inf(f)

  minimum_exists : LEMMA continuous?(f) IMPLIES EXISTS c : is_minimum(c, f)

  min_pt(f:{f|continuous?(f)}): {xj: J | is_minimum(xj,f)}     % ADDED BY RWB


  %-------------------------------
  %  Intermediate value theorem
  %-------------------------------

  intermediate_value1 : LEMMA continuous?(f) AND f(a) < x AND x < f(b)
                         IMPLIES EXISTS c : f(c) = x

  intermediate_value2 : LEMMA continuous?(f) AND f(a) <= x AND x <= f(b)
                         IMPLIES EXISTS c : f(c) = x

  intermediate_value3 : LEMMA continuous?(f) AND f(b) < x AND x < f(a)
                         IMPLIES EXISTS c : f(c) = x

  intermediate_value4 : LEMMA continuous?(f) AND f(b) <= x AND x <= f(a)
                         IMPLIES EXISTS c : f(c) = x

END continuity_interval