:: by Katuhiko Kanazashi, Noboru Endou and Yasunari Shidama

::

:: Received October 20, 2009

:: Copyright (c) 2009-2016 Association of Mizar Users

definition
end;

:: deftheorem defines --> C0SP2:def 1 :

for X being 1-sorted

for y being Real holds X --> y = the carrier of X --> y;

for X being 1-sorted

for y being Real holds X --> y = the carrier of X --> y;

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 ) )

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 ) )

proof end;

definition

let X be non empty TopSpace;

coherence

{ f where f is continuous RealMap of X : verum } is Subset of (RAlgebra the carrier of X);

end;
func ContinuousFunctions X -> Subset of (RAlgebra the carrier of X) equals :: C0SP2:def 2

{ f where f is continuous RealMap of X : verum } ;

correctness { f where f is continuous RealMap of X : verum } ;

coherence

{ f where f is continuous RealMap of X : verum } is Subset of (RAlgebra the carrier of X);

proof 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 } ;

for X being non empty TopSpace holds ContinuousFunctions X = { f where f is continuous RealMap of X : verum } ;

registration
end;

registration

let X be non empty TopSpace;

coherence

( ContinuousFunctions X is additively-linearly-closed & ContinuousFunctions X is multiplicatively-closed )

end;
coherence

( ContinuousFunctions X is additively-linearly-closed & ContinuousFunctions X is multiplicatively-closed )

proof end;

definition

let X be non empty TopSpace;

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;
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))) #);

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 ;

:: 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))) #);

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;

coherence

( R_Algebra_of_ContinuousFunctions X is strict & not R_Algebra_of_ContinuousFunctions X is empty ) ;

end;
coherence

( R_Algebra_of_ContinuousFunctions X is strict & not R_Algebra_of_ContinuousFunctions X is empty ) ;

registration

let X be non empty TopSpace;

( 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 )

end;
cluster R_Algebra_of_ContinuousFunctions X -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital right-distributive right_unital associative commutative 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 )

proof 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) )

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) )

proof end;

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) )

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) )

proof end;

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) )

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) )

proof end;

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

for A1, A2 being Subalgebra of A st the carrier of A1 c= the carrier of A2 holds

A1 is Subalgebra of A2

proof end;

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

proof end;

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

proof end;

definition

let X be non empty compact TopSpace;

coherence

(BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X) is Function of (ContinuousFunctions X),REAL;

end;
func ContinuousFunctionsNorm X -> Function of (ContinuousFunctions X),REAL equals :: C0SP2:def 4

(BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X);

correctness (BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X);

coherence

(BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X) is Function of (ContinuousFunctions X),REAL;

proof end;

:: deftheorem defines ContinuousFunctionsNorm C0SP2:def 4 :

for X being non empty compact TopSpace holds ContinuousFunctionsNorm X = (BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X);

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;

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;
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 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) #);

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 ;

;

:: 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) #);

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;

correctness

coherence

( R_Normed_Algebra_of_ContinuousFunctions X is strict & not R_Normed_Algebra_of_ContinuousFunctions X is empty );

;

end;
correctness

coherence

( R_Normed_Algebra_of_ContinuousFunctions X is strict & not R_Normed_Algebra_of_ContinuousFunctions X is empty );

;

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 )

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;
( 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

registration

let X be non empty compact TopSpace;

correctness

coherence

R_Normed_Algebra_of_ContinuousFunctions X is unital ;

end;
correctness

coherence

R_Normed_Algebra_of_ContinuousFunctions X is unital ;

proof 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

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

proof end;

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

proof end;

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

proof end;

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

proof end;

registration

let X be non empty compact TopSpace;

( 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 )

end;
cluster R_Normed_Algebra_of_ContinuousFunctions X -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative right-distributive right_unital associative commutative 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 )

proof end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

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

for F being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds (Mult_ ((ContinuousFunctions X),(RAlgebra the carrier of X))) . (1,F) = F

proof end;

registration

let X be non empty compact TopSpace;

( 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 ) by Th11;

end;
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 ) by Th11;

theorem Th12: :: C0SP2:12

for X being non empty compact TopSpace holds X --> 0 = 0. (R_Normed_Algebra_of_ContinuousFunctions X)

proof end;

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)

proof end;

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)

proof end;

theorem :: C0SP2:13

for X being non empty compact TopSpace

for F being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds 0 <= ||.F.||

for F being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds 0 <= ||.F.||

proof end;

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.||

for F being Point of (R_Normed_Algebra_of_ContinuousFunctions X) st F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) holds

0 = ||.F.||

proof end;

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) )

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) )

proof end;

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) )

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) )

proof end;

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) )

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) )

proof end;

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).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

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).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

proof end;

registration

let X be non empty compact TopSpace;

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 )

end;
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 )

proof 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

proof end;

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) )

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) )

proof end;

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 ) by LOPBAN_1:def 15, NFCONT_1:def 3;

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 ) by LOPBAN_1:def 15, NFCONT_1:def 3;

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

for Y being Subset of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st Y = ContinuousFunctions X holds

Y is closed

proof end;

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

for seq being sequence of (R_Normed_Algebra_of_ContinuousFunctions X) st seq is Cauchy_sequence_by_Norm holds

seq is convergent

proof end;

registration

let X be non empty compact TopSpace;

coherence

R_Normed_Algebra_of_ContinuousFunctions X is complete

end;
coherence

R_Normed_Algebra_of_ContinuousFunctions X is complete

proof end;

registration

let X be non empty compact TopSpace;

coherence

R_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like

end;
coherence

R_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like

proof end;

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)

for f, g being RealMap of X holds support (f + g) c= (support f) \/ (support g)

proof end;

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

for a being Real

for f being RealMap of X holds support (a (#) f) c= support f

proof end;

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)

for f, g being RealMap of X holds support (f (#) g) c= (support f) \/ (support g)

proof end;

definition

let X be non empty TopSpace;

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);

end;
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 { 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 ) ) ) } ;

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);

proof 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 ) ) ) } ;

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

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

proof end;

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

proof end;

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

proof end;

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

for W being non empty Subset of (RAlgebra the carrier of X) st W = C_0_Functions X holds

W is additively-linearly-closed

proof end;

registration

let X be non empty TopSpace;

correctness

coherence

( not C_0_Functions X is empty & C_0_Functions X is linearly-closed );

by Th28;

end;
correctness

coherence

( not C_0_Functions X is empty & C_0_Functions X is linearly-closed );

by Th28;

definition

let X be non empty TopSpace;

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;
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 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))) #);

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;

:: 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))) #);

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

for x being set st x in C_0_Functions X holds

x in BoundedFunctions the carrier of X

proof end;

definition

let X be non empty TopSpace;

coherence

(BoundedFunctionsNorm the carrier of X) | (C_0_Functions X) is Function of (C_0_Functions X),REAL;

end;
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 (BoundedFunctionsNorm the carrier of X) | (C_0_Functions X);

coherence

(BoundedFunctionsNorm the carrier of X) | (C_0_Functions X) is Function of (C_0_Functions X),REAL;

proof 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);

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;

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;
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 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) #);

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 ;

;

:: 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) #);

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;

correctness

coherence

( R_Normed_Space_of_C_0_Functions X is strict & not R_Normed_Space_of_C_0_Functions X is empty );

;

end;
correctness

coherence

( R_Normed_Space_of_C_0_Functions X is strict & not R_Normed_Space_of_C_0_Functions X is empty );

;

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

for x being set st x in C_0_Functions X holds

x in ContinuousFunctions X

proof end;

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

proof end;

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

proof end;

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).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

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).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

proof end;

registration

let X be non empty TopSpace;

( 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 )

end;
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 )

proof end;

theorem :: C0SP2:36