CSSPACE4: Complex Banach Space of Bounded Complex Sequences

canceled;

for seq being Complex_Sequence holds
( ( seq is bounded & upper_bound (rng |.seq.|) = 0 ) iff for n being Element of NAT holds seq . n = 0c ) by Lm8, Lm11;

( the carrier of Complex_linfty_Space = the_set_of_BoundedComplexSequences & ( for x being set holds
( x is VECTOR of Complex_linfty_Space iff ( x is Complex_Sequence & seq_id x is bounded ) ) ) & 0. Complex_linfty_Space = CZeroseq & ( for u being VECTOR of Complex_linfty_Space holds u = seq_id u ) & ( for u, v being VECTOR of Complex_linfty_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for c being Complex
for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u) ) & ( for u being VECTOR of Complex_linfty_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of Complex_linfty_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of Complex_linfty_Space holds seq_id v is bounded ) & ( for v being VECTOR of Complex_linfty_Space holds ||.v.|| = upper_bound (rng |.(seq_id v).|) ) )

for x, y being Point of Complex_linfty_Space
for c being Complex holds
( ( ||.x.|| = 0 implies x = 0. Complex_linfty_Space ) & ( x = 0. Complex_linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(c * x).|| = |.c.| * ||.x.|| )

for vseq being sequence of Complex_linfty_Space st vseq is CCauchy holds
vseq is convergent

Complex_linfty_Space is ComplexBanachSpace by Th5, CLOPBAN1:def 14;

for X being non empty set
for Y being ComplexNormSpace
for f being Function of X, the carrier of Y st ( for x being Element of X holds f . x = 0. Y ) holds
f is bounded

for X being non empty set
for Y being ComplexNormSpace holds ComplexBoundedFunctions (X,Y) is linearly-closed

for X being non empty set
for Y being ComplexNormSpace holds CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is Subspace of ComplexVectSpace (X,Y) by Th8, CSSPACE:13;

canceled;

for X being non empty set
for Y being ComplexNormSpace
for f, g, h being VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )

for X being non empty set
for Y being ComplexNormSpace
for f, h being VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for c being Complex holds
( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) )

for X being non empty set
for Y being ComplexNormSpace holds 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y)

for X being non empty set
for Y being ComplexNormSpace
for g being bounded Function of X, the carrier of Y holds PreNorms g is bounded_above

for X being non empty set
for Y being ComplexNormSpace
for g being Function of X, the carrier of Y holds
( g is bounded iff PreNorms g is bounded_above )

for X being non empty set
for Y being ComplexNormSpace ex NORM being Function of (ComplexBoundedFunctions (X,Y)),REAL st
for f being set st f in ComplexBoundedFunctions (X,Y) holds
NORM . f = upper_bound (PreNorms (modetrans (f,X,Y)))

for X being non empty set
for Y being ComplexNormSpace
for f being bounded Function of X, the carrier of Y holds modetrans (f,X,Y) = f

for X being non empty set
for Y being ComplexNormSpace
for f being bounded Function of X, the carrier of Y holds (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)

for X being non empty set
for Y being ComplexNormSpace holds X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions (X,Y))

for X being non empty set
for Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for g being bounded Function of X, the carrier of Y st g = f holds
for t being Element of X holds ||.(g . t).|| <= ||.f.||

for X being non empty set
for Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.||

for X being non empty set
for Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) st f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) holds
0 = ||.f.||

for X being non empty set
for Y being ComplexNormSpace
for f, g, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )

for X being non empty set
for Y being ComplexNormSpace
for f, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for c being Complex holds
( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) )

for X being non empty set
for Y being ComplexNormSpace
for f, g being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for c being Complex holds
( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

for X being non empty set
for Y being ComplexNormSpace holds
( C_NormSpace_of_BoundedFunctions (X,Y) is reflexive & C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like )

for X being non empty set
for Y being ComplexNormSpace holds C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace

for X being non empty set
for Y being ComplexNormSpace
for f, g, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )

for X being non empty set
for Y being ComplexNormSpace st Y is complete holds
for seq being sequence of (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is CCauchy holds
seq is convergent

for X being non empty set
for Y being ComplexBanachSpace holds C_NormSpace_of_BoundedFunctions (X,Y) is ComplexBanachSpace

for seq1, seq2 being Complex_Sequence st seq1 is bounded & seq2 is bounded holds
seq1 + seq2 is bounded by Lm3;

for c being Complex
for seq being Complex_Sequence st seq is bounded holds
c (#) seq is bounded by Lm4;

for seq being Complex_Sequence holds
( seq is bounded iff |.seq.| is bounded ) by Lm9, Lm10;

for seq1, seq2, seq3 being Complex_Sequence holds
( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) by Lm12;