continuous_functions_aux[T : TYPE FROM real] : THEORY

BEGIN

  f             : VAR [T -> real]
  x, x0         : VAR T
  n:              VAR nat
  epsilon, delta: VAR posreal

  IMPORTING analysis@continuous_functions[T],
            analysis@convergence_ops

  right_continuous?(f,x0): bool
    = FORALL epsilon: EXISTS delta: FORALL x: x0 <= x AND x - x0 < delta 
                             IMPLIES abs(f(x) - f(x0)) < epsilon

  left_continuous?(f,x0): bool
    = FORALL epsilon: EXISTS delta: FORALL x: x <= x0 AND x0 - x < delta 
                             IMPLIES abs(f(x) - f(x0)) < epsilon


  right_continuous?(f): bool = FORALL x0 : right_continuous?(f, x0)
  left_continuous?(f): bool  = FORALL x0 : left_continuous?(f, x0)

  continuous_lr_def: LEMMA continuous?(f) IFF
                           right_continuous?(f) AND left_continuous?(f)

END continuous_functions_aux