continuous_ball_props.pvs

continuous_ball_props [T: TYPE FROM real]
  : THEORY % Welcome

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%| Basic properties of continuity|%
%| needed for later results      |%
%  related to analytic functions |%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Written By:                   JTS

%-----     %
  BEGIN
%     -----%

%-------------------------------------------
%% Importing definition of continuity 
%-------------------------------------------

 IMPORTING analysis@continuous_functions[T]

%-------------------------------------------
%% If a continuous function is positive
%  at a point, it is positive for some
%  delta ball around that point 
%-------------------------------------------

posball: LEMMA
  FORALL(x0:T,f:[T->real]):
  (continuous?(f,x0)
  AND
  f(x0)>0)
  IMPLIES
  EXISTS(delta:posreal):
  FORALL(x:T):
  abs(x-x0) < delta
  IMPLIES
  f(x) > 0

%-------------------------------------------
%% If a continuous function is negative
%  at a point, it is negative for some
%  delta ball around that point 
%-------------------------------------------

negball: LEMMA
  FORALL(x0:T,f:[T->real]):
  (continuous?(f,x0)
  AND
  f(x0)<0)
  IMPLIES
  EXISTS(delta:posreal):
  FORALL(x:T):
  abs(x-x0) < delta
  IMPLIES
  f(x) < 0
  
   %~~~   The End      ~~~%
  END continuous_ball_props