|
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
[ zur Elbe Produktseite wechseln0.0Quellennavigators
Analyse erneut starten
]
|
