begin
theorem Th1:
theorem Th2:
definition
let X be non
empty set ;
let Y be non
empty addLoopStr ;
func FuncAdd X,
Y -> BinOp of
Funcs X,the
carrier of
Y means :
Def1:
for
f,
g being
Element of
Funcs X,the
carrier of
Y holds
it . f,
g = the
addF of
Y .: f,
g;
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
by Th1;
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;
:: deftheorem Def1 defines FuncAdd LOPBAN_1:def 1 :
definition
let X be non
empty set ;
let Y be
RealLinearSpace;
func FuncExtMult X,
Y -> Function of
[:REAL ,(Funcs X,the carrier of Y):],
Funcs X,the
carrier of
Y means :
Def2:
for
a being
Real for
f being
Element of
Funcs X,the
carrier of
Y for
x being
Element of
X holds
(it . [a,f]) . x = a * (f . x);
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)
by Th2;
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;
:: deftheorem Def2 defines FuncExtMult LOPBAN_1:def 2 :
:: deftheorem defines FuncZero LOPBAN_1:def 3 :
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 Th3:
theorem
canceled;
theorem Th5:
theorem Th6:
theorem Th7:
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
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
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 Th13:
definition
let X be non
empty set ;
let Y be
RealLinearSpace;
func RealVectSpace X,
Y -> RealLinearSpace equals
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #);
coherence
RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is RealLinearSpace
by Th13;
end;
:: deftheorem defines RealVectSpace LOPBAN_1:def 4 :
theorem
theorem
theorem
begin
:: deftheorem Def5 defines additive LOPBAN_1:def 5 :
:: deftheorem Def6 defines homogeneous LOPBAN_1:def 6 :
:: deftheorem Def7 defines LinearOperators LOPBAN_1:def 7 :
theorem Th17:
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 Th17, RSSPACE:13;
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 RealLinearSpace-like ;
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 RealLinearSpace-like )
by Th17, RSSPACE:13;
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 8 :
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
canceled;
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
begin
theorem Th24:
:: deftheorem Def9 defines bounded LOPBAN_1:def 9 :
theorem Th25:
:: deftheorem Def10 defines BoundedLinearOperators LOPBAN_1:def 10 :
theorem Th26:
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 Th26, RSSPACE:13;
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 RealLinearSpace-like ;
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 RealLinearSpace-like )
by Th26, RSSPACE:13;
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 11 :
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)) #);
theorem
canceled;
theorem Th29:
theorem Th30:
theorem Th31:
:: deftheorem Def12 defines modetrans LOPBAN_1:def 12 :
:: deftheorem defines PreNorms LOPBAN_1:def 13 :
theorem Th32:
theorem
theorem Th34:
definition
let X,
Y be
RealNormSpace;
func BoundedLinearOperatorsNorm X,
Y -> Function of
BoundedLinearOperators X,
Y,
REAL means :
Def14:
for
x being
set st
x in BoundedLinearOperators X,
Y holds
it . x = sup (PreNorms (modetrans x,X,Y));
existence
ex b1 being Function of BoundedLinearOperators X,Y, REAL st
for x being set st x in BoundedLinearOperators X,Y holds
b1 . x = sup (PreNorms (modetrans x,X,Y))
by Th34;
uniqueness
for b1, b2 being Function of BoundedLinearOperators X,Y, REAL st ( for x being set st x in BoundedLinearOperators X,Y holds
b1 . x = sup (PreNorms (modetrans x,X,Y)) ) & ( for x being set st x in BoundedLinearOperators X,Y holds
b2 . x = sup (PreNorms (modetrans x,X,Y)) ) holds
b1 = b2
end;
:: deftheorem Def14 defines BoundedLinearOperatorsNorm LOPBAN_1:def 14 :
theorem Th35:
theorem Th36:
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 15 :
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) #);
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
begin
:: deftheorem Def16 defines complete LOPBAN_1:def 16 :
Lm3:
for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e holds
lim seq <= e
theorem Th47:
theorem Th48:
theorem Th49: