environ
vocabularies HIDDEN, RLSUB_1, HAHNBAN, HAHNBAN1, UNIALG_1, MONOID_0, DUALSP01, RLVECT_1, ARYTM_1, RELAT_1, FUNCT_1, RSSPACE, RSSPACE3, VECTSP_1, REAL_1, TARSKI, MSSUBFAM, STRUCT_0, REALSET1, SEQ_1, FUNCOP_1, FCONT_1, NORMSP_0, SEQ_2, FUNCSDOM, LOPBAN_1, ORDINAL2, ARYTM_3, ALGSTR_0, NORMSP_1, FUNCT_2, PRE_TOPC, SUBSET_1, ZFMISC_1, NUMBERS, SEQ_4, XBOOLE_0, CARD_1, SUPINF_2, MESFUNC1, COMPLEX1, XXREAL_0, XXREAL_2, NAT_1, REWRITE1, VALUED_1, METRIC_1, RELAT_2, ASYMPT_1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, REALSET1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_2, XREAL_0, NAT_1, COMPLEX1, VALUED_1, SEQ_1, SEQ_2, SEQ_4, STRUCT_0, ALGSTR_0, NORMSP_0, NORMSP_1, PRE_TOPC, RLVECT_1, RLSUB_1, VECTSP_1, FUNCSDOM, MONOID_0, HAHNBAN, RSSPACE, RSSPACE3, LOPBAN_1, HAHNBAN1;
definitions ALGSTR_0, FUNCT_1, RLVECT_1, VECTSP_1, HAHNBAN, HAHNBAN1, XXREAL_2;
theorems SEQ_4, FUNCT_1, SEQ_1, SEQ_2, ABSVALUE, ALGSTR_0, COMPLEX1, TARSKI, RSSPACE3, XREAL_0, XXREAL_0, FUNCSDOM, NORMSP_1, LOPBAN_1, FUNCT_2, XBOOLE_0, XREAL_1, XCMPLX_0, RLVECT_1, FUNCOP_1, VECTSP_1, HAHNBAN, HAHNBAN1, RLSUB_1, RSSPACE, MONOID_0, NORMSP_0, ORDINAL1, NAT_1, SUBSET_1;
schemes SEQ_1, FUNCT_2, XBOOLE_0;
registrations STRUCT_0, XREAL_0, ALGSTR_0, NUMBERS, ORDINAL1, MEMBERED, RELAT_1, XXREAL_0, VALUED_0, MONOID_0, RLVECT_1, VECTSP_1, FUNCT_2, VALUED_1, FUNCOP_1, SEQ_4, HAHNBAN, HAHNBAN1, RELSET_1, FUNCT_1, XCMPLX_0, NORMSP_0, NAT_1, NORMSP_1, SEQ_2;
constructors HIDDEN, REAL_1, REALSET1, RSSPACE3, BINOP_2, RLSUB_1, LOPBAN_2, SEQ_1, SEQ_2, SEQ_4, HAHNBAN, HAHNBAN1, MONOID_0, COMSEQ_2;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities XBOOLE_0, BINOP_1, RLVECT_1, STRUCT_0, REALSET1, ALGSTR_0, NORMSP_0, SEQ_1, VECTSP_1, FUNCSDOM;
expansions FUNCT_1, RLSUB_1, TARSKI, XBOOLE_0, FUNCT_2, SEQ_2, NORMSP_0, NORMSP_1, VECTSP_1, RLVECT_1, ALGSTR_0;
registration
let X be
RealLinearSpace;
coherence
( RLSStruct(# (LinearFunctionals X),(Zero_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Add_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Mult_ ((LinearFunctionals X),(RealVectSpace the carrier of X))) #) is Abelian & RLSStruct(# (LinearFunctionals X),(Zero_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Add_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Mult_ ((LinearFunctionals X),(RealVectSpace the carrier of X))) #) is add-associative & RLSStruct(# (LinearFunctionals X),(Zero_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Add_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Mult_ ((LinearFunctionals X),(RealVectSpace the carrier of X))) #) is right_zeroed & RLSStruct(# (LinearFunctionals X),(Zero_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Add_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Mult_ ((LinearFunctionals X),(RealVectSpace the carrier of X))) #) is right_complementable & RLSStruct(# (LinearFunctionals X),(Zero_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Add_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Mult_ ((LinearFunctionals X),(RealVectSpace the carrier of X))) #) is scalar-distributive & RLSStruct(# (LinearFunctionals X),(Zero_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Add_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Mult_ ((LinearFunctionals X),(RealVectSpace the carrier of X))) #) is vector-distributive & RLSStruct(# (LinearFunctionals X),(Zero_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Add_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Mult_ ((LinearFunctionals X),(RealVectSpace the carrier of X))) #) is scalar-associative & RLSStruct(# (LinearFunctionals X),(Zero_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Add_ ((LinearFunctionals X),(RealVectSpace the carrier of X))),(Mult_ ((LinearFunctionals X),(RealVectSpace the carrier of X))) #) is scalar-unital )
by Th17, RSSPACE:11;
end;
Th21X:
for X being RealNormSpace
for F being Functional of X st F = the carrier of X --> 0 holds
( F is linear-Functional of X & F is Lipschitzian )
registration
let X be
RealNormSpace;
coherence
( RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is Abelian & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is add-associative & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is right_zeroed & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is right_complementable & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is vector-distributive & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is scalar-distributive & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is scalar-associative & RLSStruct(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))) #) is scalar-unital )
by Th22, RSSPACE:11;
end;
Th27:
for X being RealNormSpace
for g being Lipschitzian linear-Functional of X holds PreNorms g is bounded_above
Lm3:
for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Nat st
for i being Nat st k <= i holds
seq . i <= e holds
lim seq <= e