environ
vocabularies HIDDEN, NUMBERS, SEQ_1, SUBSET_1, FUNCT_1, XXREAL_0, ORDINAL2, RELAT_1, XXREAL_2, RSSPACE, TARSKI, XBOOLE_0, NAT_1, CARD_1, RLSUB_1, REAL_1, RLVECT_1, VALUED_1, ARYTM_3, ALGSTR_0, COMPLEX1, SEQ_4, NORMSP_1, STRUCT_0, SUPINF_2, ARYTM_1, ZFMISC_1, REALSET1, PRE_TOPC, MEMBER_1, RSSPACE3, SEQ_2, FUNCOP_1, FUNCSDOM, FUNCT_2, LOPBAN_1, REWRITE1, RSSPACE4, METRIC_1, RELAT_2, NORMSP_0, FUNCT_7, ASYMPT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, PRE_TOPC, DOMAIN_1, FUNCOP_1, REALSET1, XXREAL_0, XXREAL_2, XCMPLX_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, XREAL_0, NUMBERS, FUNCT_1, RELSET_1, FUNCT_2, INTEGRA2, RLVECT_1, NORMSP_0, NORMSP_1, VALUED_1, SEQ_1, SEQ_2, SEQ_4, RLSUB_1, PARTFUN1, RSSPACE, RSSPACE3, LOPBAN_1;
definitions TARSKI, XBOOLE_0, NORMSP_1, NORMSP_0, XXREAL_2;
theorems RELAT_1, TARSKI, ABSVALUE, ZFMISC_1, XBOOLE_0, NAT_1, FUNCOP_1, SEQ_1, SEQ_2, SEQM_3, SEQ_4, FUNCT_1, FUNCT_2, RLVECT_1, RLSUB_1, NORMSP_1, XREAL_0, XCMPLX_0, INTEGRA2, RSSPACE, RSSPACE3, RFUNCT_2, RSSPACE2, LOPBAN_1, COMPLEX1, XREAL_1, XXREAL_0, VALUED_0, ORDINAL1, MEASURE6, NORMSP_0;
schemes SEQ_1, FUNCT_2, XBOOLE_0;
registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED, REALSET1, STRUCT_0, RLVECT_1, RFUNCT_1, SEQ_2, NORMSP_1, RSSPACE3, VALUED_0, RSSPACE, VALUED_1, SEQ_4, NORMSP_0, RELSET_1, NAT_1, SEQ_1;
constructors HIDDEN, REAL_1, COMPLEX1, REALSET1, RLSUB_1, INTEGRA2, RSSPACE3, LOPBAN_1, RVSUM_1, SEQ_4, RELSET_1, BINOP_2, SEQ_2, SERIES_1, COMSEQ_2, BINOP_1, SEQ_1, FUNCSDOM;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities XBOOLE_0, RLVECT_1, BINOP_1, REALSET1, STRUCT_0, ALGSTR_0, VALUED_1, NORMSP_0, RSSPACE, SEQ_1, FUNCSDOM;
expansions TARSKI, XBOOLE_0, NORMSP_1, NORMSP_0, XXREAL_2;
Lm1:
for rseq being Real_Sequence
for K being Real st ( for n being Nat holds rseq . n <= K ) holds
upper_bound (rng rseq) <= K
Lm2:
for rseq being Real_Sequence st rseq is bounded holds
for n being Nat holds rseq . n <= upper_bound (rng rseq)
Lm3:
RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is Subspace of Linear_Space_of_RealSequences
by RSSPACE:11;
registration
coherence
( RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is Abelian & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is add-associative & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is right_zeroed & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is right_complementable & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is vector-distributive & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-distributive & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-associative & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-unital )
by RSSPACE:11;
end;
Lm4:
( RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is Abelian & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is add-associative & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is right_zeroed & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is right_complementable & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is vector-distributive & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-distributive & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-associative & RLSStruct(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)) #) is scalar-unital )
;
Lm5:
for rseq being Real_Sequence st ( for n being Nat holds rseq . n = In (0,REAL) ) holds
( rseq is bounded & upper_bound (rng (abs rseq)) = 0 )
Lm6:
for rseq being Real_Sequence st rseq is bounded & upper_bound (rng (abs rseq)) = 0 holds
for n being Nat holds rseq . n = 0
registration
coherence
( NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is Abelian & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is add-associative & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is right_zeroed & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is right_complementable & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is vector-distributive & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is scalar-distributive & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is scalar-associative & NORMSTR(# the_set_of_BoundedRealSequences,(Zero_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences)),linfty_norm #) is scalar-unital )
by Lm4, RSSPACE3:2;
end;
theorem
for
X being non
empty set for
Y being
RealNormSpace holds
RLSStruct(#
(BoundedFunctions (X,Y)),
(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),
(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),
(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is
Subspace of
RealVectSpace (
X,
Y)
by Th6, RSSPACE:11;
registration
let X be non
empty set ;
let Y be
RealNormSpace;
cluster RLSStruct(#
(BoundedFunctions (X,Y)),
(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),
(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),
(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #)
-> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is Abelian & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is add-associative & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is right_zeroed & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is right_complementable & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is vector-distributive & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is scalar-distributive & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is scalar-associative & RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is scalar-unital )
by Th6, RSSPACE:11;
end;
definition
let X be non
empty set ;
let Y be
RealNormSpace;
func R_VectorSpace_of_BoundedFunctions (
X,
Y)
-> RealLinearSpace equals
RLSStruct(#
(BoundedFunctions (X,Y)),
(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),
(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),
(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #);
coherence
RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #) is RealLinearSpace
;
end;
::
deftheorem defines
R_VectorSpace_of_BoundedFunctions RSSPACE4:def 6 :
for X being non empty set
for Y being RealNormSpace holds R_VectorSpace_of_BoundedFunctions (X,Y) = RLSStruct(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))) #);
definition
let X be non
empty set ;
let Y be
RealNormSpace;
existence
ex b1 being Function of (BoundedFunctions (X,Y)),REAL st
for x being object st x in BoundedFunctions (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y)))
uniqueness
for b1, b2 being Function of (BoundedFunctions (X,Y)),REAL st ( for x being object st x in BoundedFunctions (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being object st x in BoundedFunctions (X,Y) holds
b2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds
b1 = b2
end;
definition
let X be non
empty set ;
let Y be
RealNormSpace;
func R_NormSpace_of_BoundedFunctions (
X,
Y)
-> non
empty NORMSTR equals
NORMSTR(#
(BoundedFunctions (X,Y)),
(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),
(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),
(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),
(BoundedFunctionsNorm (X,Y)) #);
coherence
NORMSTR(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(BoundedFunctionsNorm (X,Y)) #) is non empty NORMSTR
;
end;
::
deftheorem defines
R_NormSpace_of_BoundedFunctions RSSPACE4:def 10 :
for X being non empty set
for Y being RealNormSpace holds R_NormSpace_of_BoundedFunctions (X,Y) = NORMSTR(# (BoundedFunctions (X,Y)),(Zero_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Add_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(Mult_ ((BoundedFunctions (X,Y)),(RealVectSpace (X,Y)))),(BoundedFunctionsNorm (X,Y)) #);
registration
let X be non
empty set ;
let Y be
RealNormSpace;
coherence
( R_NormSpace_of_BoundedFunctions (X,Y) is reflexive & R_NormSpace_of_BoundedFunctions (X,Y) is discerning & R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace-like & R_NormSpace_of_BoundedFunctions (X,Y) is vector-distributive & R_NormSpace_of_BoundedFunctions (X,Y) is scalar-distributive & R_NormSpace_of_BoundedFunctions (X,Y) is scalar-associative & R_NormSpace_of_BoundedFunctions (X,Y) is scalar-unital & R_NormSpace_of_BoundedFunctions (X,Y) is Abelian & R_NormSpace_of_BoundedFunctions (X,Y) is add-associative & R_NormSpace_of_BoundedFunctions (X,Y) is right_zeroed & R_NormSpace_of_BoundedFunctions (X,Y) is right_complementable )
by Th23;
end;
Lm7:
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