Quelle  riesz_function_sets.pvs

riesz_function_sets[a:real,b: {bb:real | a < bb}]: THEORY
%------------------------------------------------------------------------------
%  Bounded linear functionals on a subtype of [real->real]. This is in direct
%  support of the Riesz representation theorem.
%------------------------------------------------------------------------------

BEGIN

IMPORTING riesz_interval_funs[a,b]


Fnz: VAR set[[INTab->real]]


   funs_sum_closed?(Fnz) : bool   =   FORALL (f,g:(Fnz)): Fnz(f+g)
   funs_const_closed?(Fnz): bool   =   FORALL (f:(Fnz),c:real): Fnz(c*f)
   funs_bounded?(Fnz): bool   =   FORALL (f:(Fnz)): bounded_on_int?(f)
   funs_contain_constants?(Fnz): bool   =   FORALL (c:real): Fnz(LAMBDA (y:INTab):c)
   funs_contain_continuous?(Fnz): bool  =   FORALL (f:[INTab->real]): continuous_on_int?(f) IMPLIES Fnz(f)

   bounded_linear_subspace?(Fnz): bool = 
         funs_sum_closed?(Fnz) AND
      funs_const_closed?(Fnz) AND
      funs_bounded?(Fnz) AND
      funs_contain_constants?(Fnz) AND
      funs_contain_continuous?(Fnz)




END riesz_function_sets