environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, FUNCT_1, ZFMISC_1, FUNCOP_1, SUBSET_1, FUNCT_2, RELAT_1, PARTFUN1, ALGSTR_0, BINOP_1, STRUCT_0, RLVECT_1, REAL_1, SUPINF_2, ARYTM_3, ARYTM_1, FUNCSDOM, MONOID_0, TARSKI, MSSUBFAM, UNIALG_1, RLSUB_1, RSSPACE, NORMSP_1, NAT_1, PRE_TOPC, SEQ_2, ORDINAL2, XXREAL_0, CARD_1, COMPLEX1, XXREAL_2, SEQ_4, REWRITE1, RSSPACE3, SEQ_1, VALUED_1, LOPBAN_1, METRIC_1, RELAT_2, FCONT_1, ASYMPT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_3, PRE_TOPC, DOMAIN_1, FUNCOP_1, BINOP_1, XXREAL_0, XXREAL_2, XCMPLX_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, XREAL_0, NUMBERS, MONOID_0, RLVECT_1, RLSUB_1, NORMSP_0, NORMSP_1, RSSPACE, RSSPACE3, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, FUNCSDOM, VECTSP_1;
definitions FUNCT_1, ALGSTR_0, VECTSP_1, NORMSP_0, XXREAL_2;
theorems XBOOLE_0, TARSKI, ABSVALUE, RLVECT_1, FUNCOP_1, XREAL_0, XCMPLX_0, SEQ_1, SEQ_2, FUNCT_1, NAT_1, FUNCT_2, RLSUB_1, NORMSP_1, SEQ_4, FUNCT_3, RSSPACE, RSSPACE3, MONOID_0, XREAL_1, COMPLEX1, XXREAL_0, VECTSP_1, NORMSP_0, ORDINAL1;
schemes BINOP_1, SEQ_1, FUNCT_2, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, RLVECT_1, NORMSP_1, MONOID_0, RSSPACE3, VALUED_1, VALUED_0, SEQ_4, FUNCT_1, NORMSP_0, NAT_1, SEQ_1, SEQ_2;
constructors HIDDEN, DOMAIN_1, FUNCT_3, XXREAL_0, REAL_1, NAT_1, COMPLEX1, SEQM_3, RLSUB_1, FUNCSDOM, MONOID_0, MEASURE6, RSSPACE3, XXREAL_2, NORMSP_1, SEQ_4, RELSET_1, BINOP_2, RVSUM_1, SEQ_2, COMSEQ_2, SEQ_1, NUMBERS;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RLVECT_1, BINOP_1, STRUCT_0, ALGSTR_0, NORMSP_0;
expansions FUNCT_1, BINOP_1, NORMSP_0;
definition
let X be non
empty set ;
let Y be non
empty addLoopStr ;
existence
ex b1 being BinOp of (Funcs (X, the carrier of Y)) st
for f, g being Element of Funcs (X, the carrier of Y) holds b1 . (f,g) = the addF of Y .: (f,g)
uniqueness
for b1, b2 being BinOp of (Funcs (X, the carrier of Y)) st ( for f, g being Element of Funcs (X, the carrier of Y) holds b1 . (f,g) = the addF of Y .: (f,g) ) & ( for f, g being Element of Funcs (X, the carrier of Y) holds b2 . (f,g) = the addF of Y .: (f,g) ) holds
b1 = b2
end;
definition
let X be non
empty set ;
let Y be
RealLinearSpace;
existence
ex b1 being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st
for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b1 . [a,f]) . x = a * (f . x)
uniqueness
for b1, b2 being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st ( for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b1 . [a,f]) . x = a * (f . x) ) & ( for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b2 . [a,f]) . x = a * (f . x) ) holds
b1 = b2
end;
Lm1:
for A, B being non empty set
for x being Element of A
for f being Function of A,B holds x in dom f
theorem Th4:
for
X being non
empty set for
Y being
RealLinearSpace for
f,
g,
h being
Element of
Funcs (
X, the
carrier of
Y) holds
(FuncAdd (X,Y)) . (
f,
((FuncAdd (X,Y)) . (g,h)))
= (FuncAdd (X,Y)) . (
((FuncAdd (X,Y)) . (f,g)),
h)
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
theorem Th9:
for
X being non
empty set for
Y being
RealLinearSpace for
f being
Element of
Funcs (
X, the
carrier of
Y)
for
a,
b being
Real holds
(FuncAdd (X,Y)) . (
((FuncExtMult (X,Y)) . [a,f]),
((FuncExtMult (X,Y)) . [b,f]))
= (FuncExtMult (X,Y)) . [(a + b),f]
Lm2:
for X being non empty set
for Y being RealLinearSpace
for f, g being Element of Funcs (X, the carrier of Y)
for a being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]
theorem
for
X,
Y being
RealLinearSpace holds
RLSStruct(#
(LinearOperators (X,Y)),
(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),
(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),
(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is
Subspace of
RealVectSpace ( the
carrier of
X,
Y)
by Th14, RSSPACE:11;
registration
let X,
Y be
RealLinearSpace;
cluster RLSStruct(#
(LinearOperators (X,Y)),
(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),
(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),
(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #)
-> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is Abelian & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is add-associative & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is right_zeroed & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is right_complementable & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is vector-distributive & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-distributive & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-associative & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-unital )
by Th14, RSSPACE:11;
end;
definition
let X,
Y be
RealLinearSpace;
func R_VectorSpace_of_LinearOperators (
X,
Y)
-> RealLinearSpace equals
RLSStruct(#
(LinearOperators (X,Y)),
(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),
(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),
(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #);
coherence
RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is RealLinearSpace
;
end;
::
deftheorem defines
R_VectorSpace_of_LinearOperators LOPBAN_1:def 7 :
for X, Y being RealLinearSpace holds R_VectorSpace_of_LinearOperators (X,Y) = RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #);
theorem
for
X,
Y being
RealNormSpace holds
RLSStruct(#
(BoundedLinearOperators (X,Y)),
(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),
(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),
(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is
Subspace of
R_VectorSpace_of_LinearOperators (
X,
Y)
by Th22, RSSPACE:11;
registration
let X,
Y be
RealNormSpace;
cluster RLSStruct(#
(BoundedLinearOperators (X,Y)),
(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),
(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),
(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #)
-> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is Abelian & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is add-associative & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is right_zeroed & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is right_complementable & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is vector-distributive & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-distributive & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-associative & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-unital )
by Th22, RSSPACE:11;
end;
definition
let X,
Y be
RealNormSpace;
func R_VectorSpace_of_BoundedLinearOperators (
X,
Y)
-> RealLinearSpace equals
RLSStruct(#
(BoundedLinearOperators (X,Y)),
(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),
(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),
(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #);
coherence
RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is RealLinearSpace
;
end;
::
deftheorem defines
R_VectorSpace_of_BoundedLinearOperators LOPBAN_1:def 10 :
for X, Y being RealNormSpace holds R_VectorSpace_of_BoundedLinearOperators (X,Y) = RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #);
definition
let X,
Y be
RealNormSpace;
existence
ex b1 being Function of (BoundedLinearOperators (X,Y)),REAL st
for x being object st x in BoundedLinearOperators (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y)))
uniqueness
for b1, b2 being Function of (BoundedLinearOperators (X,Y)),REAL st ( for x being object st x in BoundedLinearOperators (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being object st x in BoundedLinearOperators (X,Y) holds
b2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds
b1 = b2
end;
definition
let X,
Y be
RealNormSpace;
func R_NormSpace_of_BoundedLinearOperators (
X,
Y)
-> non
empty NORMSTR equals
NORMSTR(#
(BoundedLinearOperators (X,Y)),
(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),
(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),
(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),
(BoundedLinearOperatorsNorm (X,Y)) #);
coherence
NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #) is non empty NORMSTR
;
end;
::
deftheorem defines
R_NormSpace_of_BoundedLinearOperators LOPBAN_1:def 14 :
for X, Y being RealNormSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) = NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #);
registration
let X,
Y be
RealNormSpace;
coherence
( R_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & R_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace-like & R_NormSpace_of_BoundedLinearOperators (X,Y) is vector-distributive & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-distributive & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-associative & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-unital & R_NormSpace_of_BoundedLinearOperators (X,Y) is Abelian & R_NormSpace_of_BoundedLinearOperators (X,Y) is add-associative & R_NormSpace_of_BoundedLinearOperators (X,Y) is right_zeroed & R_NormSpace_of_BoundedLinearOperators (X,Y) is right_complementable )
by Th39;
end;
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