|
riesz_linear_functionals[a:real,b: {bb:real | a < bb},
(importing riesz_function_sets[a,b]) Funs:TYPE FROM [INTab->real]]: THEORY
%------------------------------------------------------------------------------
% Linear functionals on a subtype of [[a,b]->real]. This is in direct support
% of the Riesz representation theorem.
%------------------------------------------------------------------------------
BEGIN
ASSUMING IMPORTING real_metric_space
funs_sum_closed : ASSUMPTION FORALL (f,g:Funs): Funs_pred(f+g)
funs_const_closed: ASSUMPTION FORALL (f:Funs,c:real): Funs_pred(c*f)
funs_contain_zero: ASSUMPTION Funs_pred(LAMBDA (y:INTab): 0)
ENDASSUMING
h,f,g: VAR Funs
c,y: VAR real
M: VAR nnreal
Operator: TYPE = [Funs->real]
L : VAR Operator
additive_op?(L) : bool = (FORALL (f,g): L(f+g) = L(f)+L(g))
const_inv_op?(L) : bool = (FORALL (f:Funs,c:real): L(c*f) = c*L(f))
linear_op?(L) : bool = additive_op?(L) AND const_inv_op?(L)
linear_op_zero: LEMMA linear_op?(L) IMPLIES L(LAMBDA (y:INTab): 0) = 0
END riesz_linear_functionals
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
