:: Banach Algebra of Complex-Valued Continuous Functionals and Space of Complex-valued Continuous Functionals with Bounded Support
:: by Katuhiko Kanazashi , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received May 30, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users


definition
let X be TopStruct ;
let f be Function of the carrier of X,COMPLEX;
attr f is continuous means :: CC0SP2:def 1
for Y being Subset of COMPLEX st Y is closed holds
f " Y is closed ;
end;

:: deftheorem defines continuous CC0SP2:def 1 :
for X being TopStruct
for f being Function of the carrier of X,COMPLEX holds
( f is continuous iff for Y being Subset of COMPLEX st Y is closed holds
f " Y is closed );

definition
let X be 1-sorted ;
let y be Complex;
func X --> y -> Function of the carrier of X,COMPLEX equals :: CC0SP2:def 2
the carrier of X --> y;
coherence
the carrier of X --> y is Function of the carrier of X,COMPLEX
proof end;
end;

:: deftheorem defines --> CC0SP2:def 2 :
for X being 1-sorted
for y being Complex holds X --> y = the carrier of X --> y;

theorem Th1: :: CC0SP2:1
for X being non empty TopSpace
for y being Complex
for f being Function of the carrier of X,COMPLEX st f = X --> y holds
f is continuous
proof end;

registration
let X be non empty TopSpace;
let y be Complex;
cluster X --> y -> continuous ;
coherence
X --> y is continuous
by Th1;
end;

registration
let X be non empty TopSpace;
cluster Relation-like the carrier of X -defined COMPLEX -valued non empty Function-like total quasi_total V172() continuous for Element of bool [: the carrier of X,COMPLEX:];
existence
ex b1 being Function of the carrier of X,COMPLEX st b1 is continuous
proof end;
end;

theorem Th2: :: CC0SP2:2
for X being non empty TopSpace
for f being Function of the carrier of X,COMPLEX holds
( f is continuous iff for Y being Subset of COMPLEX st Y is open holds
f " Y is open )
proof end;

theorem Th3: :: CC0SP2:3
for X being non empty TopSpace
for f being Function of the carrier of X,COMPLEX holds
( f is continuous iff for x being Point of X
for V being Subset of COMPLEX st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V ) )
proof end;

theorem Th4: :: CC0SP2:4
for X being non empty TopSpace
for f, g being continuous Function of the carrier of X,COMPLEX holds f + g is continuous Function of the carrier of X,COMPLEX
proof end;

theorem Th5: :: CC0SP2:5
for X being non empty TopSpace
for a being Complex
for f being continuous Function of the carrier of X,COMPLEX holds a (#) f is continuous Function of the carrier of X,COMPLEX
proof end;

theorem :: CC0SP2:6
for X being non empty TopSpace
for f, g being continuous Function of the carrier of X,COMPLEX holds f - g is continuous Function of the carrier of X,COMPLEX
proof end;

theorem Th7: :: CC0SP2:7
for X being non empty TopSpace
for f, g being continuous Function of the carrier of X,COMPLEX holds f (#) g is continuous Function of the carrier of X,COMPLEX
proof end;

theorem Th8: :: CC0SP2:8
for X being non empty TopSpace
for f being continuous Function of the carrier of X,COMPLEX holds
( |.f.| is Function of the carrier of X,REAL & |.f.| is continuous )
proof end;

definition
let X be non empty TopSpace;
func CContinuousFunctions X -> Subset of (CAlgebra the carrier of X) equals :: CC0SP2:def 3
{ f where f is continuous Function of the carrier of X,COMPLEX : verum } ;
correctness
coherence
{ f where f is continuous Function of the carrier of X,COMPLEX : verum } is Subset of (CAlgebra the carrier of X)
;
proof end;
end;

:: deftheorem defines CContinuousFunctions CC0SP2:def 3 :
for X being non empty TopSpace holds CContinuousFunctions X = { f where f is continuous Function of the carrier of X,COMPLEX : verum } ;

registration
let X be non empty TopSpace;
cluster CContinuousFunctions X -> non empty ;
coherence
not CContinuousFunctions X is empty
proof end;
end;

registration
let X be non empty TopSpace;
cluster CContinuousFunctions X -> multiplicatively-closed Cadditively-linearly-closed ;
coherence
( CContinuousFunctions X is Cadditively-linearly-closed & CContinuousFunctions X is multiplicatively-closed )
proof end;
end;

definition
let X be non empty TopSpace;
func C_Algebra_of_ContinuousFunctions X -> ComplexAlgebra equals :: CC0SP2:def 4
ComplexAlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) #);
coherence
ComplexAlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) #) is ComplexAlgebra
by CC0SP1:2;
end;

:: deftheorem defines C_Algebra_of_ContinuousFunctions CC0SP2:def 4 :
for X being non empty TopSpace holds C_Algebra_of_ContinuousFunctions X = ComplexAlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) #);

theorem :: CC0SP2:9
for X being non empty TopSpace holds C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2;

registration
let X be non empty TopSpace;
cluster C_Algebra_of_ContinuousFunctions X -> strict ;
coherence
( C_Algebra_of_ContinuousFunctions X is strict & not C_Algebra_of_ContinuousFunctions X is empty )
;
end;

registration
let X be non empty TopSpace;
cluster C_Algebra_of_ContinuousFunctions X -> scalar-unital ;
coherence
( C_Algebra_of_ContinuousFunctions X is Abelian & C_Algebra_of_ContinuousFunctions X is add-associative & C_Algebra_of_ContinuousFunctions X is right_zeroed & C_Algebra_of_ContinuousFunctions X is right_complementable & C_Algebra_of_ContinuousFunctions X is vector-distributive & C_Algebra_of_ContinuousFunctions X is scalar-distributive & C_Algebra_of_ContinuousFunctions X is scalar-associative & C_Algebra_of_ContinuousFunctions X is scalar-unital & C_Algebra_of_ContinuousFunctions X is commutative & C_Algebra_of_ContinuousFunctions X is associative & C_Algebra_of_ContinuousFunctions X is right_unital & C_Algebra_of_ContinuousFunctions X is right-distributive & C_Algebra_of_ContinuousFunctions X is vector-distributive & C_Algebra_of_ContinuousFunctions X is scalar-distributive & C_Algebra_of_ContinuousFunctions X is scalar-associative & C_Algebra_of_ContinuousFunctions X is vector-associative )
proof end;
end;

theorem Th10: :: CC0SP2:10
for X being non empty TopSpace
for F, G, H being VECTOR of (C_Algebra_of_ContinuousFunctions X)
for f, g, h being Function of the carrier of X,COMPLEX st f = F & g = G & h = H holds
( H = F + G iff for x being Element of the carrier of X holds h . x = (f . x) + (g . x) )
proof end;

theorem Th11: :: CC0SP2:11
for X being non empty TopSpace
for F, G being VECTOR of (C_Algebra_of_ContinuousFunctions X)
for f, g being Function of the carrier of X,COMPLEX
for a being Complex st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
proof end;

theorem Th12: :: CC0SP2:12
for X being non empty TopSpace
for F, G, H being VECTOR of (C_Algebra_of_ContinuousFunctions X)
for f, g, h being Function of the carrier of X,COMPLEX st f = F & g = G & h = H holds
( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) )
proof end;

theorem Th13: :: CC0SP2:13
for X being non empty TopSpace holds 0. (C_Algebra_of_ContinuousFunctions X) = X --> 0c
proof end;

theorem Th14: :: CC0SP2:14
for X being non empty TopSpace holds 1_ (C_Algebra_of_ContinuousFunctions X) = X --> 1r
proof end;

theorem Th15: :: CC0SP2:15
for A being ComplexAlgebra
for A1, A2 being ComplexSubAlgebra of A st the carrier of A1 c= the carrier of A2 holds
A1 is ComplexSubAlgebra of A2
proof end;

Lm1: for X being non empty compact TopSpace
for x being set st x in CContinuousFunctions X holds
x in ComplexBoundedFunctions the carrier of X

proof end;

theorem :: CC0SP2:16
for X being non empty compact TopSpace holds C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of C_Algebra_of_BoundedFunctions the carrier of X
proof end;

definition
let X be non empty compact TopSpace;
func CContinuousFunctionsNorm X -> Function of (CContinuousFunctions X),REAL equals :: CC0SP2:def 5
(ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X);
correctness
coherence
(ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X) is Function of (CContinuousFunctions X),REAL
;
proof end;
end;

:: deftheorem defines CContinuousFunctionsNorm CC0SP2:def 5 :
for X being non empty compact TopSpace holds CContinuousFunctionsNorm X = (ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X);

definition
let X be non empty compact TopSpace;
func C_Normed_Algebra_of_ContinuousFunctions X -> Normed_Complex_AlgebraStr equals :: CC0SP2:def 6
Normed_Complex_AlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(CContinuousFunctionsNorm X) #);
correctness
coherence
Normed_Complex_AlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(CContinuousFunctionsNorm X) #) is Normed_Complex_AlgebraStr
;
;
end;

:: deftheorem defines C_Normed_Algebra_of_ContinuousFunctions CC0SP2:def 6 :
for X being non empty compact TopSpace holds C_Normed_Algebra_of_ContinuousFunctions X = Normed_Complex_AlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(CContinuousFunctionsNorm X) #);

registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> non empty strict ;
correctness
coherence
( not C_Normed_Algebra_of_ContinuousFunctions X is empty & C_Normed_Algebra_of_ContinuousFunctions X is strict )
;
;
end;

Lm2: now :: thesis: for X being non empty compact TopSpace
for x, e being Element of (C_Normed_Algebra_of_ContinuousFunctions X) st e = One_ ((CContinuousFunctions X),(CAlgebra the carrier of X)) holds
( x * e = x & e * x = x )
let X be non empty compact TopSpace; :: thesis: for x, e being Element of (C_Normed_Algebra_of_ContinuousFunctions X) st e = One_ ((CContinuousFunctions X),(CAlgebra the carrier of X)) holds
( x * e = x & e * x = x )

set F = C_Normed_Algebra_of_ContinuousFunctions X;
let x, e be Element of (C_Normed_Algebra_of_ContinuousFunctions X); :: thesis: ( e = One_ ((CContinuousFunctions X),(CAlgebra the carrier of X)) implies ( x * e = x & e * x = x ) )
assume A1: e = One_ ((CContinuousFunctions X),(CAlgebra the carrier of X)) ; :: thesis: ( x * e = x & e * x = x )
set X1 = CContinuousFunctions X;
reconsider f = x as Element of CContinuousFunctions X ;
1_ (CAlgebra the carrier of X) = X --> 1
.= 1_ (C_Algebra_of_ContinuousFunctions X) by Th14 ;
then A2: ( [f,(1_ (CAlgebra the carrier of X))] in [:(CContinuousFunctions X),(CContinuousFunctions X):] & [(1_ (CAlgebra the carrier of X)),f] in [:(CContinuousFunctions X),(CContinuousFunctions X):] ) by ZFMISC_1:87;
x * e = (mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (f,(1_ (CAlgebra the carrier of X))) by A1, C0SP1:def 8;
then x * e = ( the multF of (CAlgebra the carrier of X) || (CContinuousFunctions X)) . (f,(1_ (CAlgebra the carrier of X))) by C0SP1:def 6;
then x * e = f * (1_ (CAlgebra the carrier of X)) by A2, FUNCT_1:49;
hence x * e = x ; :: thesis: e * x = x
e * x = (mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . ((1_ (CAlgebra the carrier of X)),f) by A1, C0SP1:def 8;
then e * x = ( the multF of (CAlgebra the carrier of X) || (CContinuousFunctions X)) . ((1_ (CAlgebra the carrier of X)),f) by C0SP1:def 6;
then e * x = (1_ (CAlgebra the carrier of X)) * f by A2, FUNCT_1:49;
hence e * x = x ; :: thesis: verum
end;

registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> unital ;
correctness
coherence
C_Normed_Algebra_of_ContinuousFunctions X is unital
;
proof end;
end;

Lm3: for X being non empty compact TopSpace
for x being Point of (C_Normed_Algebra_of_ContinuousFunctions X)
for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
||.x.|| = ||.y.||

by FUNCT_1:49;

Lm4: for X being non empty compact TopSpace
for x1, x2 being Point of (C_Normed_Algebra_of_ContinuousFunctions X)
for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2

proof end;

Lm5: for X being non empty compact TopSpace
for a being Complex
for x being Point of (C_Normed_Algebra_of_ContinuousFunctions X)
for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y

proof end;

Lm6: for X being non empty compact TopSpace
for x1, x2 being Point of (C_Normed_Algebra_of_ContinuousFunctions X)
for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 * x2 = y1 * y2

proof end;

theorem Th17: :: CC0SP2:17
for X being non empty compact TopSpace holds C_Normed_Algebra_of_ContinuousFunctions X is ComplexAlgebra
proof end;

registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> right_complementable Abelian add-associative right_zeroed right-distributive right_unital associative commutative vector-distributive scalar-distributive scalar-associative vector-associative ;
coherence
( C_Normed_Algebra_of_ContinuousFunctions X is right_complementable & C_Normed_Algebra_of_ContinuousFunctions X is Abelian & C_Normed_Algebra_of_ContinuousFunctions X is add-associative & C_Normed_Algebra_of_ContinuousFunctions X is right_zeroed & C_Normed_Algebra_of_ContinuousFunctions X is vector-distributive & C_Normed_Algebra_of_ContinuousFunctions X is scalar-distributive & C_Normed_Algebra_of_ContinuousFunctions X is scalar-associative & C_Normed_Algebra_of_ContinuousFunctions X is associative & C_Normed_Algebra_of_ContinuousFunctions X is commutative & C_Normed_Algebra_of_ContinuousFunctions X is right-distributive & C_Normed_Algebra_of_ContinuousFunctions X is right_unital & C_Normed_Algebra_of_ContinuousFunctions X is vector-associative )
by Th17;
end;

theorem :: CC0SP2:18
for X being non empty compact TopSpace
for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds (Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (1r,F) = F
proof end;

registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( C_Normed_Algebra_of_ContinuousFunctions X is vector-distributive & C_Normed_Algebra_of_ContinuousFunctions X is scalar-distributive & C_Normed_Algebra_of_ContinuousFunctions X is scalar-associative & C_Normed_Algebra_of_ContinuousFunctions X is scalar-unital )
proof end;
end;

theorem :: CC0SP2:19
for X being non empty compact TopSpace holds C_Normed_Algebra_of_ContinuousFunctions X is ComplexLinearSpace ;

theorem Th20: :: CC0SP2:20
for X being non empty compact TopSpace holds X --> 0 = 0. (C_Normed_Algebra_of_ContinuousFunctions X)
proof end;

Lm7: for X being non empty compact TopSpace holds 0. (C_Normed_Algebra_of_ContinuousFunctions X) = 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X)
proof end;

Lm8: for X being non empty compact TopSpace holds 1. (C_Normed_Algebra_of_ContinuousFunctions X) = 1. (C_Normed_Algebra_of_BoundedFunctions the carrier of X)
proof end;

theorem :: CC0SP2:21
for X being non empty compact TopSpace
for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds 0 <= ||.F.||
proof end;

theorem Th22: :: CC0SP2:22
for X being non empty compact TopSpace
for f, g, h being Function of the carrier of X,COMPLEX
for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds
( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )
proof end;

theorem :: CC0SP2:23
for a being Complex
for X being non empty compact TopSpace
for f, g being Function of the carrier of X,COMPLEX
for F, G being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G holds
( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
proof end;

theorem :: CC0SP2:24
for X being non empty compact TopSpace
for f, g, h being Function of the carrier of X,COMPLEX
for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )
proof end;

theorem Th25: :: CC0SP2:25
for X being non empty compact TopSpace holds ||.(0. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = 0
proof end;

theorem Th26: :: CC0SP2:26
for X being non empty compact TopSpace
for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st ||.F.|| = 0 holds
F = 0. (C_Normed_Algebra_of_ContinuousFunctions X)
proof end;

theorem Th27: :: CC0SP2:27
for a being Complex
for X being non empty compact TopSpace
for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(a * F).|| = |.a.| * ||.F.||
proof end;

theorem Th28: :: CC0SP2:28
for X being non empty compact TopSpace
for F, G being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(F + G).|| <= ||.F.|| + ||.G.||
proof end;

registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> discerning reflexive ComplexNormSpace-like ;
coherence
( C_Normed_Algebra_of_ContinuousFunctions X is discerning & C_Normed_Algebra_of_ContinuousFunctions X is reflexive & C_Normed_Algebra_of_ContinuousFunctions X is ComplexNormSpace-like )
by Th25, Th26, Th27, Th28;
end;

Lm9: for X being non empty compact TopSpace
for x1, x2 being Point of (C_Normed_Algebra_of_ContinuousFunctions X)
for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 - x2 = y1 - y2

proof end;

theorem :: CC0SP2:29
for X being non empty compact TopSpace
for f, g, h being Function of the carrier of X,COMPLEX
for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds
( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )
proof end;

theorem Th30: :: CC0SP2:30
for X being ComplexBanachSpace
for Y being Subset of X
for seq being sequence of X st Y is closed & rng seq c= Y & seq is CCauchy holds
( seq is convergent & lim seq in Y ) by CLOPBAN1:def 13, NCFCONT1:def 3;

theorem Th31: :: CC0SP2:31
for X being non empty compact TopSpace
for Y being Subset of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st Y = CContinuousFunctions X holds
Y is closed
proof end;

theorem Th32: :: CC0SP2:32
for X being non empty compact TopSpace
for seq being sequence of (C_Normed_Algebra_of_ContinuousFunctions X) st seq is CCauchy holds
seq is convergent
proof end;

registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> complete ;
coherence
C_Normed_Algebra_of_ContinuousFunctions X is complete
proof end;
end;

registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> Banach_Algebra-like ;
coherence
C_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like
proof end;
end;

:: Some properties of support
theorem Th33: :: CC0SP2:33
for X being non empty TopSpace
for f, g being Function of the carrier of X,COMPLEX holds support (f + g) c= (support f) \/ (support g)
proof end;

theorem Th34: :: CC0SP2:34
for X being non empty TopSpace
for a being Complex
for f being Function of the carrier of X,COMPLEX holds support (a (#) f) c= support f
proof end;

theorem :: CC0SP2:35
for X being non empty TopSpace
for f, g being Function of the carrier of X,COMPLEX holds support (f (#) g) c= (support f) \/ (support g)
proof end;

:: Space of Complex-Valued Continuous Functionals with bounded support
definition
let X be non empty TopSpace;
func CC_0_Functions X -> non empty Subset of (ComplexVectSpace the carrier of X) equals :: CC0SP2:def 7
{ f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) )
}
;
correctness
coherence
{ f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) )
}
is non empty Subset of (ComplexVectSpace the carrier of X)
;
proof end;
end;

:: deftheorem defines CC_0_Functions CC0SP2:def 7 :
for X being non empty TopSpace holds CC_0_Functions X = { f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) )
}
;

theorem :: CC0SP2:36
for X being non empty TopSpace holds CC_0_Functions X is non empty Subset of (CAlgebra the carrier of X) ;

Lm10: for X being non empty TopSpace
for v, u being Element of (CAlgebra the carrier of X) st v in CC_0_Functions X & u in CC_0_Functions X holds
v + u in CC_0_Functions X

proof end;

Lm11: for X being non empty TopSpace
for a being Complex
for u being Element of (CAlgebra the carrier of X) st u in CC_0_Functions X holds
a * u in CC_0_Functions X

proof end;

Lm12: for X being non empty TopSpace
for u being Element of (CAlgebra the carrier of X) st u in CC_0_Functions X holds
- u in CC_0_Functions X

proof end;

theorem :: CC0SP2:37
for X being non empty TopSpace
for W being non empty Subset of (CAlgebra the carrier of X) st W = CC_0_Functions X holds
W is Cadditively-linearly-closed
proof end;

theorem Th38: :: CC0SP2:38
for X being non empty TopSpace holds CC_0_Functions X is add-closed
proof end;

theorem Th39: :: CC0SP2:39
for X being non empty TopSpace holds CC_0_Functions X is linearly-closed
proof end;

registration
let X be non empty TopSpace;
cluster CC_0_Functions X -> non empty linearly-closed ;
correctness
coherence
( not CC_0_Functions X is empty & CC_0_Functions X is linearly-closed )
;
by Th39;
end;

theorem Th40: :: CC0SP2:40
for V being ComplexLinearSpace
for V1 being Subset of V st V1 is linearly-closed & not V1 is empty holds
CLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V
proof end;

theorem Th41: :: CC0SP2:41
for X being non empty TopSpace holds CLSStruct(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))) #) is Subspace of ComplexVectSpace the carrier of X by Th40;

definition
let X be non empty TopSpace;
func C_VectorSpace_of_C_0_Functions X -> ComplexLinearSpace equals :: CC0SP2:def 8
CLSStruct(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))) #);
correctness
coherence
CLSStruct(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))) #) is ComplexLinearSpace
;
by Th41;
end;

:: deftheorem defines C_VectorSpace_of_C_0_Functions CC0SP2:def 8 :
for X being non empty TopSpace holds C_VectorSpace_of_C_0_Functions X = CLSStruct(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))) #);

theorem Th42: :: CC0SP2:42
for X being non empty TopSpace
for x being set st x in CC_0_Functions X holds
x in ComplexBoundedFunctions the carrier of X
proof end;

definition
let X be non empty TopSpace;
func CC_0_FunctionsNorm X -> Function of (CC_0_Functions X),REAL equals :: CC0SP2:def 9
(ComplexBoundedFunctionsNorm the carrier of X) | (CC_0_Functions X);
correctness
coherence
(ComplexBoundedFunctionsNorm the carrier of X) | (CC_0_Functions X) is Function of (CC_0_Functions X),REAL
;
proof end;
end;

:: deftheorem defines CC_0_FunctionsNorm CC0SP2:def 9 :
for X being non empty TopSpace holds CC_0_FunctionsNorm X = (ComplexBoundedFunctionsNorm the carrier of X) | (CC_0_Functions X);

definition
let X be non empty TopSpace;
func C_Normed_Space_of_C_0_Functions X -> CNORMSTR equals :: CC0SP2:def 10
CNORMSTR(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(CC_0_FunctionsNorm X) #);
correctness
coherence
CNORMSTR(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(CC_0_FunctionsNorm X) #) is CNORMSTR
;
;
end;

:: deftheorem defines C_Normed_Space_of_C_0_Functions CC0SP2:def 10 :
for X being non empty TopSpace holds C_Normed_Space_of_C_0_Functions X = CNORMSTR(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(CC_0_FunctionsNorm X) #);

registration
let X be non empty TopSpace;
cluster C_Normed_Space_of_C_0_Functions X -> non empty strict ;
correctness
coherence
( C_Normed_Space_of_C_0_Functions X is strict & not C_Normed_Space_of_C_0_Functions X is empty )
;
;
end;

theorem :: CC0SP2:43
for X being non empty TopSpace
for x being set st x in CC_0_Functions X holds
x in CContinuousFunctions X
proof end;

theorem Th44: :: CC0SP2:44
for X being non empty TopSpace holds 0. (C_VectorSpace_of_C_0_Functions X) = X --> 0
proof end;

theorem Th45: :: CC0SP2:45
for X being non empty TopSpace holds 0. (C_Normed_Space_of_C_0_Functions X) = X --> 0
proof end;

Lm13: for X being non empty TopSpace
for x1, x2 being Point of (C_Normed_Space_of_C_0_Functions X)
for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2

proof end;

Lm14: for X being non empty TopSpace
for a being Complex
for x being Point of (C_Normed_Space_of_C_0_Functions X)
for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y

proof end;

theorem Th46: :: CC0SP2:46
for a being Complex
for X being non empty TopSpace
for F, G being Point of (C_Normed_Space_of_C_0_Functions X) holds
( ( ||.F.|| = 0 implies F = 0. (C_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (C_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
proof end;

Lm15: for X being non empty TopSpace holds C_Normed_Space_of_C_0_Functions X is ComplexNormSpace-like
by Th46;

registration
let X be non empty TopSpace;
cluster C_Normed_Space_of_C_0_Functions X -> right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;
coherence
( C_Normed_Space_of_C_0_Functions X is reflexive & C_Normed_Space_of_C_0_Functions X is discerning & C_Normed_Space_of_C_0_Functions X is ComplexNormSpace-like & C_Normed_Space_of_C_0_Functions X is vector-distributive & C_Normed_Space_of_C_0_Functions X is scalar-distributive & C_Normed_Space_of_C_0_Functions X is scalar-associative & C_Normed_Space_of_C_0_Functions X is scalar-unital & C_Normed_Space_of_C_0_Functions X is Abelian & C_Normed_Space_of_C_0_Functions X is add-associative & C_Normed_Space_of_C_0_Functions X is right_zeroed & C_Normed_Space_of_C_0_Functions X is right_complementable )
proof end;
end;

theorem :: CC0SP2:47
for X being non empty TopSpace holds C_Normed_Space_of_C_0_Functions X is ComplexNormSpace ;