:: Banach Algebra of Continuous Functionals and Space of Real-valued Continuous Functionals with Bounded Support :: by Katuhiko Kanazashi, Noboru Endou and Yasunari Shidama :: :: Received October 20, 2009 :: Copyright (c) 2009-2012 Association of Mizar Users begin definition let X be 1-sorted ; let y be real number ; funcX --> y -> RealMap of X equals :: C0SP2:def 1 the carrier of X --> y; coherence the carrier of X --> y is RealMap of X proofend; end; :: deftheorem defines --> C0SP2:def_1_:_ for X being 1-sorted for y being real number holds X --> y = the carrier of X --> y; registration let X be TopSpace; let y be real number ; clusterX --> y -> continuous ; coherence X --> y is continuous proofend; end; theorem Th1: :: C0SP2:1 for X being non empty TopSpace for f being RealMap of X holds ( f is continuous iff for x being Point of X for V being Subset of REAL 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; definition let X be non empty TopSpace; func ContinuousFunctions X -> Subset of (RAlgebra the carrier of X) equals :: C0SP2:def 2 { f where f is continuous RealMap of X : verum } ; correctness coherence { f where f is continuous RealMap of X : verum } is Subset of (RAlgebra the carrier of X); proofend; end; :: deftheorem defines ContinuousFunctions C0SP2:def_2_:_ for X being non empty TopSpace holds ContinuousFunctions X = { f where f is continuous RealMap of X : verum } ; registration let X be non empty TopSpace; cluster ContinuousFunctions X -> non empty ; coherence not ContinuousFunctions X is empty proofend; end; registration let X be non empty TopSpace; cluster ContinuousFunctions X -> multiplicatively-closed additively-linearly-closed ; coherence ( ContinuousFunctions X is additively-linearly-closed & ContinuousFunctions X is multiplicatively-closed ) proofend; end; definition let X be non empty TopSpace; func R_Algebra_of_ContinuousFunctions X -> AlgebraStr equals :: C0SP2:def 3 AlgebraStr(# (ContinuousFunctions X),(mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Add_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(One_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Zero_ ((ContinuousFunctions X),(RAlgebra the carrier of X))) #); coherence AlgebraStr(# (ContinuousFunctions X),(mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Add_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(One_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Zero_ ((ContinuousFunctions X),(RAlgebra the carrier of X))) #) is AlgebraStr ; end; :: deftheorem defines R_Algebra_of_ContinuousFunctions C0SP2:def_3_:_ for X being non empty TopSpace holds R_Algebra_of_ContinuousFunctions X = AlgebraStr(# (ContinuousFunctions X),(mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Add_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(One_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Zero_ ((ContinuousFunctions X),(RAlgebra the carrier of X))) #); theorem :: C0SP2:2 for X being non empty TopSpace holds R_Algebra_of_ContinuousFunctions X is Subalgebra of RAlgebra the carrier of X by C0SP1:6; registration let X be non empty TopSpace; cluster R_Algebra_of_ContinuousFunctions X -> non empty strict ; coherence ( R_Algebra_of_ContinuousFunctions X is strict & not R_Algebra_of_ContinuousFunctions X is empty ) ; end; registration let X be non empty TopSpace; cluster R_Algebra_of_ContinuousFunctions X -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital associative commutative right-distributive right_unital vector-associative ; coherence ( R_Algebra_of_ContinuousFunctions X is Abelian & R_Algebra_of_ContinuousFunctions X is add-associative & R_Algebra_of_ContinuousFunctions X is right_zeroed & R_Algebra_of_ContinuousFunctions X is right_complementable & R_Algebra_of_ContinuousFunctions X is vector-distributive & R_Algebra_of_ContinuousFunctions X is scalar-distributive & R_Algebra_of_ContinuousFunctions X is scalar-associative & R_Algebra_of_ContinuousFunctions X is scalar-unital & R_Algebra_of_ContinuousFunctions X is commutative & R_Algebra_of_ContinuousFunctions X is associative & R_Algebra_of_ContinuousFunctions X is right_unital & R_Algebra_of_ContinuousFunctions X is right-distributive & R_Algebra_of_ContinuousFunctions X is vector-distributive & R_Algebra_of_ContinuousFunctions X is scalar-distributive & R_Algebra_of_ContinuousFunctions X is scalar-associative & R_Algebra_of_ContinuousFunctions X is vector-associative ) proofend; end; theorem Th3: :: C0SP2:3 for X being non empty TopSpace for F, G, H being VECTOR of (R_Algebra_of_ContinuousFunctions X) for f, g, h being RealMap of X 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 Th4: :: C0SP2:4 for X being non empty TopSpace for F, G, H being VECTOR of (R_Algebra_of_ContinuousFunctions X) for f, g, h being RealMap of X for a being Real st f = F & g = G holds ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) proofend; theorem Th5: :: C0SP2:5 for X being non empty TopSpace for F, G, H being VECTOR of (R_Algebra_of_ContinuousFunctions X) for f, g, h being RealMap of X 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 Th6: :: C0SP2:6 for X being non empty TopSpace holds 0. (R_Algebra_of_ContinuousFunctions X) = X --> 0 proofend; theorem Th7: :: C0SP2:7 for X being non empty TopSpace holds 1_ (R_Algebra_of_ContinuousFunctions X) = X --> 1 proofend; theorem Th8: :: C0SP2:8 for A being Algebra for A1, A2 being Subalgebra of A st the carrier of A1 c= the carrier of A2 holds A1 is Subalgebra of A2 proofend; Lm1: for X being non empty compact TopSpace for x being set st x in ContinuousFunctions X holds x in BoundedFunctions the carrier of X proofend; theorem :: C0SP2:9 for X being non empty compact TopSpace holds R_Algebra_of_ContinuousFunctions X is Subalgebra of R_Algebra_of_BoundedFunctions the carrier of X proofend; definition let X be non empty compact TopSpace; func ContinuousFunctionsNorm X -> Function of (ContinuousFunctions X),REAL equals :: C0SP2:def 4 (BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X); correctness coherence (BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X) is Function of (ContinuousFunctions X),REAL; proofend; end; :: deftheorem defines ContinuousFunctionsNorm C0SP2:def_4_:_ for X being non empty compact TopSpace holds ContinuousFunctionsNorm X = (BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X); definition let X be non empty compact TopSpace; func R_Normed_Algebra_of_ContinuousFunctions X -> Normed_AlgebraStr equals :: C0SP2:def 5 Normed_AlgebraStr(# (ContinuousFunctions X),(mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Add_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(One_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Zero_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(ContinuousFunctionsNorm X) #); correctness coherence Normed_AlgebraStr(# (ContinuousFunctions X),(mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Add_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(One_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Zero_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(ContinuousFunctionsNorm X) #) is Normed_AlgebraStr ; ; end; :: deftheorem defines R_Normed_Algebra_of_ContinuousFunctions C0SP2:def_5_:_ for X being non empty compact TopSpace holds R_Normed_Algebra_of_ContinuousFunctions X = Normed_AlgebraStr(# (ContinuousFunctions X),(mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Add_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(One_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(Zero_ ((ContinuousFunctions X),(RAlgebra the carrier of X))),(ContinuousFunctionsNorm X) #); registration let X be non empty compact TopSpace; cluster R_Normed_Algebra_of_ContinuousFunctions X -> non empty strict ; correctness coherence ( R_Normed_Algebra_of_ContinuousFunctions X is strict & not R_Normed_Algebra_of_ContinuousFunctions X is empty ); ; end; Lm2: now__::_thesis:_for_X_being_non_empty_compact_TopSpace for_x,_e_being_Element_of_(R_Normed_Algebra_of_ContinuousFunctions_X)_st_e_=_One__((ContinuousFunctions_X),(RAlgebra_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 (R_Normed_Algebra_of_ContinuousFunctions X) st e = One_ ((ContinuousFunctions X),(RAlgebra the carrier of X)) holds ( x * e = x & e * x = x ) set F = R_Normed_Algebra_of_ContinuousFunctions X; let x, e be Element of (R_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( e = One_ ((ContinuousFunctions X),(RAlgebra the carrier of X)) implies ( x * e = x & e * x = x ) ) assume A1: e = One_ ((ContinuousFunctions X),(RAlgebra the carrier of X)) ; ::_thesis: ( x * e = x & e * x = x ) set X1 = ContinuousFunctions X; reconsider f = x as Element of ContinuousFunctions X ; 1_ (RAlgebra the carrier of X) = X --> 1 .= 1_ (R_Algebra_of_ContinuousFunctions X) by Th7 ; then A2: ( [f,(1_ (RAlgebra the carrier of X))] in [:(ContinuousFunctions X),(ContinuousFunctions X):] & [(1_ (RAlgebra the carrier of X)),f] in [:(ContinuousFunctions X),(ContinuousFunctions X):] ) by ZFMISC_1:87; x * e = (mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))) . (f,(1_ (RAlgebra the carrier of X))) by A1, C0SP1:def_8; then x * e = ( the multF of (RAlgebra the carrier of X) || (ContinuousFunctions X)) . (f,(1_ (RAlgebra the carrier of X))) by C0SP1:def_6; then x * e = f * (1_ (RAlgebra 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_ ((ContinuousFunctions X),(RAlgebra the carrier of X))) . ((1_ (RAlgebra the carrier of X)),f) by A1, C0SP1:def_8; then e * x = ( the multF of (RAlgebra the carrier of X) || (ContinuousFunctions X)) . ((1_ (RAlgebra the carrier of X)),f) by C0SP1:def_6; then e * x = (1_ (RAlgebra 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 R_Normed_Algebra_of_ContinuousFunctions X -> unital ; correctness coherence R_Normed_Algebra_of_ContinuousFunctions X is unital ; proofend; end; theorem Th10: :: C0SP2:10 for W being Normed_AlgebraStr for V being Algebra st AlgebraStr(# the carrier of W, the multF of W, the addF of W, the Mult of W, the OneF of W, the ZeroF of W #) = V holds W is Algebra proofend; Lm3: for X being non empty compact TopSpace for x being Point of (R_Normed_Algebra_of_ContinuousFunctions X) for y being Point of (R_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 (R_Normed_Algebra_of_ContinuousFunctions X) for y1, y2 being Point of (R_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 Real for x being Point of (R_Normed_Algebra_of_ContinuousFunctions X) for y being Point of (R_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 (R_Normed_Algebra_of_ContinuousFunctions X) for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds x1 * x2 = y1 * y2 proofend; registration let X be non empty compact TopSpace; cluster R_Normed_Algebra_of_ContinuousFunctions X -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative commutative right-distributive right_unital vector-associative ; coherence ( R_Normed_Algebra_of_ContinuousFunctions X is Abelian & R_Normed_Algebra_of_ContinuousFunctions X is add-associative & R_Normed_Algebra_of_ContinuousFunctions X is right_zeroed & R_Normed_Algebra_of_ContinuousFunctions X is right_complementable & R_Normed_Algebra_of_ContinuousFunctions X is commutative & R_Normed_Algebra_of_ContinuousFunctions X is associative & R_Normed_Algebra_of_ContinuousFunctions X is right_unital & R_Normed_Algebra_of_ContinuousFunctions X is right-distributive & R_Normed_Algebra_of_ContinuousFunctions X is vector-distributive & R_Normed_Algebra_of_ContinuousFunctions X is scalar-distributive & R_Normed_Algebra_of_ContinuousFunctions X is scalar-associative & R_Normed_Algebra_of_ContinuousFunctions X is vector-associative ) proofend; end; theorem Th11: :: C0SP2:11 for X being non empty compact TopSpace for F being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds (Mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))) . (1,F) = F proofend; registration let X be non empty compact TopSpace; cluster R_Normed_Algebra_of_ContinuousFunctions X -> vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( R_Normed_Algebra_of_ContinuousFunctions X is vector-distributive & R_Normed_Algebra_of_ContinuousFunctions X is scalar-distributive & R_Normed_Algebra_of_ContinuousFunctions X is scalar-associative & R_Normed_Algebra_of_ContinuousFunctions X is scalar-unital ) proofend; end; theorem Th12: :: C0SP2:12 for X being non empty compact TopSpace holds X --> 0 = 0. (R_Normed_Algebra_of_ContinuousFunctions X) proofend; Lm7: for X being non empty compact TopSpace holds 0. (R_Normed_Algebra_of_ContinuousFunctions X) = 0. (R_Normed_Algebra_of_BoundedFunctions the carrier of X) proofend; Lm8: for X being non empty compact TopSpace holds 1. (R_Normed_Algebra_of_ContinuousFunctions X) = 1. (R_Normed_Algebra_of_BoundedFunctions the carrier of X) proofend; theorem :: C0SP2:13 for X being non empty compact TopSpace for F being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds 0 <= ||.F.|| proofend; theorem :: C0SP2:14 for X being non empty compact TopSpace for F being Point of (R_Normed_Algebra_of_ContinuousFunctions X) st F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) holds 0 = ||.F.|| proofend; theorem Th15: :: C0SP2:15 for X being non empty compact TopSpace for F, G, H being Point of (R_Normed_Algebra_of_ContinuousFunctions X) for f, g, h being RealMap of 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 :: C0SP2:16 for a being Real for X being non empty compact TopSpace for F, G being Point of (R_Normed_Algebra_of_ContinuousFunctions X) for f, g being RealMap of 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 :: C0SP2:17 for X being non empty compact TopSpace for F, G, H being Point of (R_Normed_Algebra_of_ContinuousFunctions X) for f, g, h being RealMap of 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 Th18: :: C0SP2:18 for a being Real for X being non empty compact TopSpace for F, G being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds ( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) proofend; registration let X be non empty compact TopSpace; cluster R_Normed_Algebra_of_ContinuousFunctions X -> discerning reflexive RealNormSpace-like ; coherence ( R_Normed_Algebra_of_ContinuousFunctions X is reflexive & R_Normed_Algebra_of_ContinuousFunctions X is discerning & R_Normed_Algebra_of_ContinuousFunctions X is RealNormSpace-like ) proofend; end; Lm9: for X being non empty compact TopSpace for x1, x2 being Point of (R_Normed_Algebra_of_ContinuousFunctions X) for y1, y2 being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds x1 - x2 = y1 - y2 proofend; theorem :: C0SP2:19 for X being non empty compact TopSpace for F, G, H being Point of (R_Normed_Algebra_of_ContinuousFunctions X) for f, g, h being RealMap of 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 Th20: :: C0SP2:20 for X being RealBanachSpace for Y being Subset of X for seq being sequence of X st Y is closed & rng seq c= Y & seq is Cauchy_sequence_by_Norm holds ( seq is convergent & lim seq in Y ) proofend; theorem Th21: :: C0SP2:21 for X being non empty compact TopSpace for Y being Subset of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st Y = ContinuousFunctions X holds Y is closed proofend; theorem Th22: :: C0SP2:22 for X being non empty compact TopSpace for seq being sequence of (R_Normed_Algebra_of_ContinuousFunctions X) st seq is Cauchy_sequence_by_Norm holds seq is convergent proofend; registration let X be non empty compact TopSpace; cluster R_Normed_Algebra_of_ContinuousFunctions X -> complete ; coherence R_Normed_Algebra_of_ContinuousFunctions X is complete proofend; end; registration let X be non empty compact TopSpace; cluster R_Normed_Algebra_of_ContinuousFunctions X -> Banach_Algebra-like ; coherence R_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like proofend; end; begin theorem Th23: :: C0SP2:23 for X being non empty TopSpace for f, g being RealMap of X holds support (f + g) c= (support f) \/ (support g) proofend; theorem Th24: :: C0SP2:24 for X being non empty TopSpace for a being Real for f being RealMap of X holds support (a (#) f) c= support f proofend; theorem :: C0SP2:25 for X being non empty TopSpace for f, g being RealMap of X holds support (f (#) g) c= (support f) \/ (support g) proofend; begin definition let X be non empty TopSpace; func C_0_Functions X -> non empty Subset of (RealVectSpace the carrier of X) equals :: C0SP2:def 6 { f where f is RealMap of X : ( 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 RealMap of X : ( 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 (RealVectSpace the carrier of X); proofend; end; :: deftheorem defines C_0_Functions C0SP2:def_6_:_ for X being non empty TopSpace holds C_0_Functions X = { f where f is RealMap of X : ( 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 :: C0SP2:26 for X being non empty TopSpace holds C_0_Functions X is non empty Subset of (RAlgebra the carrier of X) ; Lm10: for X being non empty TopSpace for v, u being Element of (RAlgebra the carrier of X) st v in C_0_Functions X & u in C_0_Functions X holds v + u in C_0_Functions X proofend; Lm11: for X being non empty TopSpace for a being Real for u being Element of (RAlgebra the carrier of X) st u in C_0_Functions X holds a * u in C_0_Functions X proofend; Lm12: for X being non empty TopSpace for u being Element of (RAlgebra the carrier of X) st u in C_0_Functions X holds - u in C_0_Functions X proofend; theorem :: C0SP2:27 for X being non empty TopSpace for W being non empty Subset of (RAlgebra the carrier of X) st W = C_0_Functions X holds W is additively-linearly-closed proofend; theorem Th28: :: C0SP2:28 for X being non empty TopSpace holds C_0_Functions X is linearly-closed proofend; registration let X be non empty TopSpace; cluster C_0_Functions X -> non empty linearly-closed ; correctness coherence ( not C_0_Functions X is empty & C_0_Functions X is linearly-closed ); by Th28; end; definition let X be non empty TopSpace; func R_VectorSpace_of_C_0_Functions X -> RealLinearSpace equals :: C0SP2:def 7 RLSStruct(# (C_0_Functions X),(Zero_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Add_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Mult_ ((C_0_Functions X),(RealVectSpace the carrier of X))) #); correctness coherence RLSStruct(# (C_0_Functions X),(Zero_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Add_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Mult_ ((C_0_Functions X),(RealVectSpace the carrier of X))) #) is RealLinearSpace; by RSSPACE:11; end; :: deftheorem defines R_VectorSpace_of_C_0_Functions C0SP2:def_7_:_ for X being non empty TopSpace holds R_VectorSpace_of_C_0_Functions X = RLSStruct(# (C_0_Functions X),(Zero_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Add_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Mult_ ((C_0_Functions X),(RealVectSpace the carrier of X))) #); theorem :: C0SP2:29 for X being non empty TopSpace holds R_VectorSpace_of_C_0_Functions X is Subspace of RealVectSpace the carrier of X by RSSPACE:11; theorem Th30: :: C0SP2:30 for X being non empty TopSpace for x being set st x in C_0_Functions X holds x in BoundedFunctions the carrier of X proofend; definition let X be non empty TopSpace; func C_0_FunctionsNorm X -> Function of (C_0_Functions X),REAL equals :: C0SP2:def 8 (BoundedFunctionsNorm the carrier of X) | (C_0_Functions X); correctness coherence (BoundedFunctionsNorm the carrier of X) | (C_0_Functions X) is Function of (C_0_Functions X),REAL; proofend; end; :: deftheorem defines C_0_FunctionsNorm C0SP2:def_8_:_ for X being non empty TopSpace holds C_0_FunctionsNorm X = (BoundedFunctionsNorm the carrier of X) | (C_0_Functions X); definition let X be non empty TopSpace; func R_Normed_Space_of_C_0_Functions X -> non empty NORMSTR equals :: C0SP2:def 9 NORMSTR(# (C_0_Functions X),(Zero_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Add_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Mult_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(C_0_FunctionsNorm X) #); correctness coherence NORMSTR(# (C_0_Functions X),(Zero_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Add_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Mult_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(C_0_FunctionsNorm X) #) is non empty NORMSTR ; ; end; :: deftheorem defines R_Normed_Space_of_C_0_Functions C0SP2:def_9_:_ for X being non empty TopSpace holds R_Normed_Space_of_C_0_Functions X = NORMSTR(# (C_0_Functions X),(Zero_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Add_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(Mult_ ((C_0_Functions X),(RealVectSpace the carrier of X))),(C_0_FunctionsNorm X) #); registration let X be non empty TopSpace; cluster R_Normed_Space_of_C_0_Functions X -> non empty strict ; correctness coherence ( R_Normed_Space_of_C_0_Functions X is strict & not R_Normed_Space_of_C_0_Functions X is empty ); ; end; theorem :: C0SP2:31 for X being non empty TopSpace for x being set st x in C_0_Functions X holds x in ContinuousFunctions X proofend; theorem Th32: :: C0SP2:32 for X being non empty TopSpace holds 0. (R_VectorSpace_of_C_0_Functions X) = X --> 0 proofend; theorem Th33: :: C0SP2:33 for X being non empty TopSpace holds 0. (R_Normed_Space_of_C_0_Functions X) = X --> 0 proofend; Lm13: for X being non empty TopSpace for x1, x2 being Point of (R_Normed_Space_of_C_0_Functions X) for y1, y2 being Point of (R_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 Real for x being Point of (R_Normed_Space_of_C_0_Functions X) for y being Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds a * x = a * y proofend; theorem Th34: :: C0SP2:34 for a being Real for X being non empty TopSpace for F, G being Point of (R_Normed_Space_of_C_0_Functions X) holds ( ( ||.F.|| = 0 implies F = 0. (R_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (R_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) proofend; theorem Th35: :: C0SP2:35 for X being non empty TopSpace holds R_Normed_Space_of_C_0_Functions X is RealNormSpace-like proofend; registration let X be non empty TopSpace; cluster R_Normed_Space_of_C_0_Functions X -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ; coherence ( R_Normed_Space_of_C_0_Functions X is reflexive & R_Normed_Space_of_C_0_Functions X is discerning & R_Normed_Space_of_C_0_Functions X is RealNormSpace-like & R_Normed_Space_of_C_0_Functions X is vector-distributive & R_Normed_Space_of_C_0_Functions X is scalar-distributive & R_Normed_Space_of_C_0_Functions X is scalar-associative & R_Normed_Space_of_C_0_Functions X is scalar-unital & R_Normed_Space_of_C_0_Functions X is Abelian & R_Normed_Space_of_C_0_Functions X is add-associative & R_Normed_Space_of_C_0_Functions X is right_zeroed & R_Normed_Space_of_C_0_Functions X is right_complementable ) proofend; end; theorem :: C0SP2:36 for X being non empty TopSpace holds R_Normed_Space_of_C_0_Functions X is RealNormSpace ;