:: 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-2012 Association of Mizar Users begin definition let X be TopStruct ; let f be Function of the carrier of X,COMPLEX; attrf is continuous means :Def1: :: CC0SP2:def 1 for Y being Subset of COMPLEX st Y is closed holds f " Y is closed ; end; :: deftheorem Def1 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 number ; funcX --> 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 proofend; end; :: deftheorem defines --> CC0SP2:def_2_:_ for X being 1-sorted for y being complex number holds X --> y = the carrier of X --> y; theorem Th1: :: CC0SP2:1 for X being non empty TopSpace for y being complex number for f being Function of the carrier of X,COMPLEX st f = X --> y holds f is continuous proofend; registration let X be non empty TopSpace; let y be complex number ; clusterX --> y -> continuous ; coherence X --> y is continuous by Th1; end; registration let X be non empty TopSpace; cluster non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() 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 proofend; 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 ) proofend; 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 ) ) proofend; 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 proofend; theorem Th5: :: CC0SP2:5 for X being non empty TopSpace for a being complex number for f being continuous Function of the carrier of X,COMPLEX holds a (#) f is continuous Function of the carrier of X,COMPLEX proofend; 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 proofend; 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 proofend; 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 ) proofend; 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); proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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) ) proofend; 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) ) proofend; 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) ) proofend; theorem Th13: :: CC0SP2:13 for X being non empty TopSpace holds 0. (C_Algebra_of_ContinuousFunctions X) = X --> 0c proofend; theorem Th14: :: CC0SP2:14 for X being non empty TopSpace holds 1_ (C_Algebra_of_ContinuousFunctions X) = X --> 1r proofend; 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 proofend; 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 proofend; 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 proofend; 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; proofend; 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 by VECTSP_1:def_4; ::_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 by VECTSP_1:def_4; ::_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 ; proofend; 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 proofend; 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 proofend; 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 proofend; theorem Th17: :: CC0SP2:17 for X being non empty compact TopSpace holds C_Normed_Algebra_of_ContinuousFunctions X is ComplexAlgebra proofend; registration let X be non empty compact TopSpace; cluster C_Normed_Algebra_of_ContinuousFunctions X -> right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital 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 proofend; 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 ) proofend; 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) proofend; 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) proofend; 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) proofend; theorem :: CC0SP2:21 for X being non empty compact TopSpace for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds 0 <= ||.F.|| proofend; 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) ) proofend; 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) ) proofend; 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) ) proofend; theorem Th25: :: CC0SP2:25 for X being non empty compact TopSpace holds ||.(0. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = 0 proofend; 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) proofend; 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).|| = (abs a) * ||.F.|| proofend; 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.|| proofend; 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 ) proofend; 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 proofend; 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) ) proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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) proofend; 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 proofend; 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) proofend; :: 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); proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; theorem Th38: :: CC0SP2:38 for X being non empty TopSpace holds CC_0_Functions X is add-closed proofend; theorem Th39: :: CC0SP2:39 for X being non empty TopSpace holds CC_0_Functions X is linearly-closed proofend; 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 proofend; 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 proofend; 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; proofend; 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 proofend; theorem Th44: :: CC0SP2:44 for X being non empty TopSpace holds 0. (C_VectorSpace_of_C_0_Functions X) = X --> 0 proofend; theorem Th45: :: CC0SP2:45 for X being non empty TopSpace holds 0. (C_Normed_Space_of_C_0_Functions X) = X --> 0 proofend; 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 proofend; 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 proofend; 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).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) proofend; Lm15: for X being non empty TopSpace holds C_Normed_Space_of_C_0_Functions X is ComplexNormSpace-like proofend; 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 ) proofend; end; theorem :: CC0SP2:47 for X being non empty TopSpace holds C_Normed_Space_of_C_0_Functions X is ComplexNormSpace ;