Quelle  real_fun_on_compact_sets.pvs   Sprache: PVS

real_fun_on_compact_sets[T:TYPE+,d:[T,T->nnreal]]: THEORY
%------------------------------------------------------------------------------
% In This Theory, We Prove That A Continuous Real-Valued Function On A
% Compact Subset Of A Metric Space Attains A Maximum
%
%     Authors: Anthony Narkawicz,  NASA Langley
%
%     Version 1.0         8/31/2009  Initial Version
%------------------------------------------------------------------------------
BEGIN

   ASSUMING IMPORTING metric_spaces_def[T,d]
       fullset_metric_space: ASSUMPTION metric_space?[T,d](fullset[T])
   ENDASSUMING

   S: VAR set[T]

   % A continuous function on a compact set realizes a maximum and a minimum


   IMPORTING real_metric_space, continuity_ms_def[T,d,real,real_dist], reals@abs_lems, 
             compactness[T,d]

   f: VAR [T -> real]

   cont_on_compact_max: THEOREM 
      (continuous?(f,S) and compact?(S)) 
      IMPLIES empty?(S) or (EXISTS (s: (S)): FORALL (t: (S)): f(t) <= f(s))

   cont_on_compact_min: THEOREM 
      (continuous?(f,S) and compact?(S)) 
      IMPLIES empty?(S) or (EXISTS (s: (S)): FORALL (t: (S)): f(t) >= f(s))

END real_fun_on_compact_sets