:: by Katuhiko Kanazashi , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received May 30, 2011

:: Copyright (c) 2011-2019 Association of Mizar Users

definition

let X be TopStruct ;

let f be Function of the carrier of X,COMPLEX;

end;
let f be Function of the carrier of X,COMPLEX;

attr f is continuous means :: CC0SP2:def 1

for Y being Subset of COMPLEX st Y is closed holds

f " Y is closed ;

for Y being Subset of COMPLEX st Y is closed holds

f " Y is closed ;

:: deftheorem defines continuous CC0SP2:def 1 :

for X being TopStruct

for f being Function of the carrier of X,COMPLEX holds

( f is continuous iff for Y being Subset of COMPLEX st Y is closed holds

f " Y is closed );

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;

coherence

the carrier of X --> y is Function of the carrier of X,COMPLEX

end;
let y be Complex;

coherence

the carrier of X --> y is Function of the carrier of X,COMPLEX

proof end;

:: deftheorem defines --> CC0SP2:def 2 :

for X being 1-sorted

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

for X being 1-sorted

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

theorem Th1: :: CC0SP2:1

for X being non empty TopSpace

for y being Complex

for f being Function of the carrier of X,COMPLEX st f = X --> y holds

f is continuous

for y being Complex

for f being Function of the carrier of X,COMPLEX st f = X --> y holds

f is continuous

proof end;

registration
end;

registration

let X be non empty TopSpace;

ex b_{1} being Function of the carrier of X,COMPLEX st b_{1} is continuous

end;
cluster Relation-like the carrier of X -defined COMPLEX -valued non empty Function-like total quasi_total V172() continuous for Element of bool [: the carrier of X,COMPLEX:];

existence ex b

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

for f being Function of the carrier of X,COMPLEX holds

( f is continuous iff for Y being Subset of COMPLEX st Y is open holds

f " Y is open )

proof end;

theorem Th3: :: CC0SP2:3

for X being non empty TopSpace

for f being Function of the carrier of X,COMPLEX holds

( f is continuous iff for x being Point of X

for V being Subset of COMPLEX st f . x in V & V is open holds

ex W being Subset of X st

( x in W & W is open & f .: W c= V ) )

for f being Function of the carrier of X,COMPLEX holds

( f is continuous iff for x being Point of X

for V being Subset of COMPLEX st f . x in V & V is open holds

ex W being Subset of X st

( x in W & W is open & f .: W c= V ) )

proof end;

theorem Th4: :: CC0SP2:4

for X being non empty TopSpace

for f, g being continuous Function of the carrier of X,COMPLEX holds f + g is continuous Function of the carrier of X,COMPLEX

for f, g being continuous Function of the carrier of X,COMPLEX holds f + g is continuous Function of the carrier of X,COMPLEX

proof end;

theorem Th5: :: CC0SP2:5

for X being non empty TopSpace

for a being Complex

for f being continuous Function of the carrier of X,COMPLEX holds a (#) f is continuous Function of the carrier of X,COMPLEX

for a being Complex

for f being continuous Function of the carrier of X,COMPLEX holds a (#) f is continuous Function of the carrier of X,COMPLEX

proof end;

theorem :: CC0SP2:6

for X being non empty TopSpace

for f, g being continuous Function of the carrier of X,COMPLEX holds f - g is continuous Function of the carrier of X,COMPLEX

for f, g being continuous Function of the carrier of X,COMPLEX holds f - g is continuous Function of the carrier of X,COMPLEX

proof end;

theorem Th7: :: CC0SP2:7

for X being non empty TopSpace

for f, g being continuous Function of the carrier of X,COMPLEX holds f (#) g is continuous Function of the carrier of X,COMPLEX

for f, g being continuous Function of the carrier of X,COMPLEX holds f (#) g is continuous Function of the carrier of X,COMPLEX

proof end;

theorem Th8: :: CC0SP2:8

for X being non empty TopSpace

for f being continuous Function of the carrier of X,COMPLEX holds

( |.f.| is Function of the carrier of X,REAL & |.f.| is continuous )

for f being continuous Function of the carrier of X,COMPLEX holds

( |.f.| is Function of the carrier of X,REAL & |.f.| is continuous )

proof end;

definition

let X be non empty TopSpace;

coherence

{ f where f is continuous Function of the carrier of X,COMPLEX : verum } is Subset of (CAlgebra the carrier of X);

end;
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 { f where f is continuous Function of the carrier of X,COMPLEX : verum } ;

coherence

{ f where f is continuous Function of the carrier of X,COMPLEX : verum } is Subset of (CAlgebra the carrier of X);

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

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

registration
end;

registration

let X be non empty TopSpace;

coherence

( CContinuousFunctions X is Cadditively-linearly-closed & CContinuousFunctions X is multiplicatively-closed )

end;
coherence

( CContinuousFunctions X is Cadditively-linearly-closed & CContinuousFunctions X is multiplicatively-closed )

proof end;

definition

let X be non empty TopSpace;

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

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;

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

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;

coherence

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

end;
coherence

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

registration

let X be non empty TopSpace;

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 )

end;
coherence

( C_Algebra_of_ContinuousFunctions X is Abelian & C_Algebra_of_ContinuousFunctions X is add-associative & C_Algebra_of_ContinuousFunctions X is right_zeroed & C_Algebra_of_ContinuousFunctions X is right_complementable & C_Algebra_of_ContinuousFunctions X is vector-distributive & C_Algebra_of_ContinuousFunctions X is scalar-distributive & C_Algebra_of_ContinuousFunctions X is scalar-associative & C_Algebra_of_ContinuousFunctions X is scalar-unital & C_Algebra_of_ContinuousFunctions X is commutative & C_Algebra_of_ContinuousFunctions X is associative & C_Algebra_of_ContinuousFunctions X is right_unital & C_Algebra_of_ContinuousFunctions X is right-distributive & C_Algebra_of_ContinuousFunctions X is vector-distributive & C_Algebra_of_ContinuousFunctions X is scalar-distributive & C_Algebra_of_ContinuousFunctions X is scalar-associative & C_Algebra_of_ContinuousFunctions X is vector-associative )

proof end;

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

for F, G, H being VECTOR of (C_Algebra_of_ContinuousFunctions X)

for f, g, h being Function of the carrier of X,COMPLEX st f = F & g = G & h = H holds

( H = F + G iff for x being Element of the carrier of X holds h . x = (f . x) + (g . x) )

proof end;

theorem Th11: :: CC0SP2:11

for X being non empty TopSpace

for F, G being VECTOR of (C_Algebra_of_ContinuousFunctions X)

for f, g being Function of the carrier of X,COMPLEX

for a being Complex st f = F & g = G holds

( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

for F, G being VECTOR of (C_Algebra_of_ContinuousFunctions X)

for f, g being Function of the carrier of X,COMPLEX

for a being Complex st f = F & g = G holds

( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

proof end;

theorem Th12: :: CC0SP2:12

for X being non empty TopSpace

for F, G, H being VECTOR of (C_Algebra_of_ContinuousFunctions X)

for f, g, h being Function of the carrier of X,COMPLEX st f = F & g = G & h = H holds

( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) )

for F, G, H being VECTOR of (C_Algebra_of_ContinuousFunctions X)

for f, g, h being Function of the carrier of X,COMPLEX st f = F & g = G & h = H holds

( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) )

proof end;

theorem 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

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

A1 is ComplexSubAlgebra of A2

proof end;

Lm1: for X being non empty compact TopSpace

for x being set st x in CContinuousFunctions X holds

x in ComplexBoundedFunctions the carrier of X

proof end;

theorem :: CC0SP2:16

for X being non empty compact TopSpace holds C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of C_Algebra_of_BoundedFunctions the carrier of X

proof end;

definition

let X be non empty compact TopSpace;

coherence

(ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X) is Function of (CContinuousFunctions X),REAL;

end;
func CContinuousFunctionsNorm X -> Function of (CContinuousFunctions X),REAL equals :: CC0SP2:def 5

(ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X);

correctness (ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X);

coherence

(ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X) is Function of (CContinuousFunctions X),REAL;

proof end;

:: deftheorem defines CContinuousFunctionsNorm CC0SP2:def 5 :

for X being non empty compact TopSpace holds CContinuousFunctionsNorm X = (ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X);

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;

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

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 ;

;

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

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;

correctness

coherence

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

;

end;
correctness

coherence

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

;

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 )

for x, e being Element of (C_Normed_Algebra_of_ContinuousFunctions X) st e = One_ ((CContinuousFunctions X),(CAlgebra the carrier of X)) holds

( x * e = x & e * x = x )

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

( x * e = x & e * x = x )

set F = C_Normed_Algebra_of_ContinuousFunctions X;

let x, e be Element of (C_Normed_Algebra_of_ContinuousFunctions X); :: thesis: ( e = One_ ((CContinuousFunctions X),(CAlgebra the carrier of X)) implies ( x * e = x & e * x = x ) )

assume A1: e = One_ ((CContinuousFunctions X),(CAlgebra the carrier of X)) ; :: thesis: ( x * e = x & e * x = x )

set X1 = CContinuousFunctions X;

reconsider f = x as Element of CContinuousFunctions X ;

1_ (CAlgebra the carrier of X) = X --> 1

.= 1_ (C_Algebra_of_ContinuousFunctions X) by Th14 ;

then A2: ( [f,(1_ (CAlgebra the carrier of X))] in [:(CContinuousFunctions X),(CContinuousFunctions X):] & [(1_ (CAlgebra the carrier of X)),f] in [:(CContinuousFunctions X),(CContinuousFunctions X):] ) by ZFMISC_1:87;

x * e = (mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (f,(1_ (CAlgebra the carrier of X))) by A1, C0SP1:def 8;

then x * e = ( the multF of (CAlgebra the carrier of X) || (CContinuousFunctions X)) . (f,(1_ (CAlgebra the carrier of X))) by C0SP1:def 6;

then x * e = f * (1_ (CAlgebra the carrier of X)) by A2, FUNCT_1:49;

hence x * e = x ; :: thesis: e * x = x

e * x = (mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . ((1_ (CAlgebra the carrier of X)),f) by A1, C0SP1:def 8;

then e * x = ( the multF of (CAlgebra the carrier of X) || (CContinuousFunctions X)) . ((1_ (CAlgebra the carrier of X)),f) by C0SP1:def 6;

then e * x = (1_ (CAlgebra the carrier of X)) * f by A2, FUNCT_1:49;

hence e * x = x ; :: thesis: verum

end;
( x * e = x & e * x = x )

set F = C_Normed_Algebra_of_ContinuousFunctions X;

let x, e be Element of (C_Normed_Algebra_of_ContinuousFunctions X); :: thesis: ( e = One_ ((CContinuousFunctions X),(CAlgebra the carrier of X)) implies ( x * e = x & e * x = x ) )

assume A1: e = One_ ((CContinuousFunctions X),(CAlgebra the carrier of X)) ; :: thesis: ( x * e = x & e * x = x )

set X1 = CContinuousFunctions X;

reconsider f = x as Element of CContinuousFunctions X ;

1_ (CAlgebra the carrier of X) = X --> 1

.= 1_ (C_Algebra_of_ContinuousFunctions X) by Th14 ;

then A2: ( [f,(1_ (CAlgebra the carrier of X))] in [:(CContinuousFunctions X),(CContinuousFunctions X):] & [(1_ (CAlgebra the carrier of X)),f] in [:(CContinuousFunctions X),(CContinuousFunctions X):] ) by ZFMISC_1:87;

x * e = (mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (f,(1_ (CAlgebra the carrier of X))) by A1, C0SP1:def 8;

then x * e = ( the multF of (CAlgebra the carrier of X) || (CContinuousFunctions X)) . (f,(1_ (CAlgebra the carrier of X))) by C0SP1:def 6;

then x * e = f * (1_ (CAlgebra the carrier of X)) by A2, FUNCT_1:49;

hence x * e = x ; :: thesis: e * x = x

e * x = (mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . ((1_ (CAlgebra the carrier of X)),f) by A1, C0SP1:def 8;

then e * x = ( the multF of (CAlgebra the carrier of X) || (CContinuousFunctions X)) . ((1_ (CAlgebra the carrier of X)),f) by C0SP1:def 6;

then e * x = (1_ (CAlgebra the carrier of X)) * f by A2, FUNCT_1:49;

hence e * x = x ; :: thesis: verum

registration

let X be non empty compact TopSpace;

correctness

coherence

C_Normed_Algebra_of_ContinuousFunctions X is unital ;

end;
correctness

coherence

C_Normed_Algebra_of_ContinuousFunctions X is unital ;

proof end;

Lm3: for X being non empty compact TopSpace

for x being Point of (C_Normed_Algebra_of_ContinuousFunctions X)

for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds

||.x.|| = ||.y.||

by FUNCT_1:49;

Lm4: for X being non empty compact TopSpace

for x1, x2 being Point of (C_Normed_Algebra_of_ContinuousFunctions X)

for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds

x1 + x2 = y1 + y2

proof end;

Lm5: for X being non empty compact TopSpace

for a being Complex

for x being Point of (C_Normed_Algebra_of_ContinuousFunctions X)

for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds

a * x = a * y

proof end;

Lm6: for X being non empty compact TopSpace

for x1, x2 being Point of (C_Normed_Algebra_of_ContinuousFunctions X)

for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds

x1 * x2 = y1 * y2

proof end;

theorem Th17: :: CC0SP2:17

for X being non empty compact TopSpace holds C_Normed_Algebra_of_ContinuousFunctions X is ComplexAlgebra

proof end;

registration

let X be non empty compact TopSpace;

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

coherence ( C_Normed_Algebra_of_ContinuousFunctions X is right_complementable & C_Normed_Algebra_of_ContinuousFunctions X is Abelian & C_Normed_Algebra_of_ContinuousFunctions X is add-associative & C_Normed_Algebra_of_ContinuousFunctions X is right_zeroed & C_Normed_Algebra_of_ContinuousFunctions X is vector-distributive & C_Normed_Algebra_of_ContinuousFunctions X is scalar-distributive & C_Normed_Algebra_of_ContinuousFunctions X is scalar-associative & C_Normed_Algebra_of_ContinuousFunctions X is associative & C_Normed_Algebra_of_ContinuousFunctions X is commutative & C_Normed_Algebra_of_ContinuousFunctions X is right-distributive & C_Normed_Algebra_of_ContinuousFunctions X is right_unital & C_Normed_Algebra_of_ContinuousFunctions X is vector-associative ) by Th17;

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

for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds (Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (1r,F) = F

proof end;

registration

let X be non empty compact TopSpace;

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

end;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence ( C_Normed_Algebra_of_ContinuousFunctions X is vector-distributive & C_Normed_Algebra_of_ContinuousFunctions X is scalar-distributive & C_Normed_Algebra_of_ContinuousFunctions X is scalar-associative & C_Normed_Algebra_of_ContinuousFunctions X is scalar-unital )

proof end;

theorem :: CC0SP2:19

for X being non empty compact TopSpace holds C_Normed_Algebra_of_ContinuousFunctions X is ComplexLinearSpace ;

theorem Th20: :: CC0SP2:20

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

proof end;

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

proof end;

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

proof end;

theorem :: CC0SP2:21

for X being non empty compact TopSpace

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

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

proof end;

theorem Th22: :: CC0SP2:22

for X being non empty compact TopSpace

for f, g, h being Function of the carrier of X,COMPLEX

for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds

( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )

for f, g, h being Function of the carrier of X,COMPLEX

for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds

( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) )

proof end;

theorem :: CC0SP2:23

for a being Complex

for X being non empty compact TopSpace

for f, g being Function of the carrier of X,COMPLEX

for F, G being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G holds

( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

for X being non empty compact TopSpace

for f, g being Function of the carrier of X,COMPLEX

for F, G being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G holds

( G = a * F iff for x being Element of X holds g . x = a * (f . x) )

proof end;

theorem :: CC0SP2:24

for X being non empty compact TopSpace

for f, g, h being Function of the carrier of X,COMPLEX

for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds

( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )

for f, g, h being Function of the carrier of X,COMPLEX

for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds

( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )

proof end;

theorem Th25: :: CC0SP2:25

for X being non empty compact TopSpace holds ||.(0. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = 0

proof end;

theorem Th26: :: CC0SP2:26

for X being non empty compact TopSpace

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

F = 0. (C_Normed_Algebra_of_ContinuousFunctions X)

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

F = 0. (C_Normed_Algebra_of_ContinuousFunctions X)

proof end;

theorem Th27: :: CC0SP2:27

for a being Complex

for X being non empty compact TopSpace

for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(a * F).|| = |.a.| * ||.F.||

for X being non empty compact TopSpace

for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(a * F).|| = |.a.| * ||.F.||

proof end;

theorem Th28: :: CC0SP2:28

for X being non empty compact TopSpace

for F, G being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(F + G).|| <= ||.F.|| + ||.G.||

for F, G being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(F + G).|| <= ||.F.|| + ||.G.||

proof end;

registration

let X be non empty compact TopSpace;

coherence

( C_Normed_Algebra_of_ContinuousFunctions X is discerning & C_Normed_Algebra_of_ContinuousFunctions X is reflexive & C_Normed_Algebra_of_ContinuousFunctions X is ComplexNormSpace-like ) by Th25, Th26, Th27, Th28;

end;
coherence

( C_Normed_Algebra_of_ContinuousFunctions X is discerning & C_Normed_Algebra_of_ContinuousFunctions X is reflexive & C_Normed_Algebra_of_ContinuousFunctions X is ComplexNormSpace-like ) by Th25, Th26, Th27, Th28;

Lm9: for X being non empty compact TopSpace

for x1, x2 being Point of (C_Normed_Algebra_of_ContinuousFunctions X)

for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds

x1 - x2 = y1 - y2

proof end;

theorem :: CC0SP2:29

for X being non empty compact TopSpace

for f, g, h being Function of the carrier of X,COMPLEX

for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds

( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )

for f, g, h being Function of the carrier of X,COMPLEX

for F, G, H being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st f = F & g = G & h = H holds

( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )

proof end;

theorem Th30: :: CC0SP2:30

for X being ComplexBanachSpace

for Y being Subset of X

for seq being sequence of X st Y is closed & rng seq c= Y & seq is CCauchy holds

( seq is convergent & lim seq in Y ) by CLOPBAN1:def 13, NCFCONT1:def 3;

for Y being Subset of X

for seq being sequence of X st Y is closed & rng seq c= Y & seq is CCauchy holds

( seq is convergent & lim seq in Y ) by CLOPBAN1:def 13, NCFCONT1:def 3;

theorem Th31: :: CC0SP2:31

for X being non empty compact TopSpace

for Y being Subset of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st Y = CContinuousFunctions X holds

Y is closed

for Y being Subset of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st Y = CContinuousFunctions X holds

Y is closed

proof end;

theorem Th32: :: CC0SP2:32

for X being non empty compact TopSpace

for seq being sequence of (C_Normed_Algebra_of_ContinuousFunctions X) st seq is CCauchy holds

seq is convergent

for seq being sequence of (C_Normed_Algebra_of_ContinuousFunctions X) st seq is CCauchy holds

seq is convergent

proof end;

registration

let X be non empty compact TopSpace;

coherence

C_Normed_Algebra_of_ContinuousFunctions X is complete

end;
coherence

C_Normed_Algebra_of_ContinuousFunctions X is complete

proof end;

registration

let X be non empty compact TopSpace;

coherence

C_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like

end;
coherence

C_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like

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

for f, g being Function of the carrier of X,COMPLEX holds support (f + g) c= (support f) \/ (support g)

proof end;

theorem Th34: :: CC0SP2:34

for X being non empty TopSpace

for a being Complex

for f being Function of the carrier of X,COMPLEX holds support (a (#) f) c= support f

for a being Complex

for f being Function of the carrier of X,COMPLEX holds support (a (#) f) c= support f

proof end;

theorem :: CC0SP2:35

for X being non empty TopSpace

for f, g being Function of the carrier of X,COMPLEX holds support (f (#) g) c= (support f) \/ (support g)

for f, g being Function of the carrier of X,COMPLEX holds support (f (#) g) c= (support f) \/ (support g)

proof end;

:: Space of Complex-Valued Continuous Functionals with bounded support

definition

let X be non empty TopSpace;

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

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

coherence

{ f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st

( Y is compact & ( for A being Subset of X st A = support f holds

Cl A is Subset of Y ) ) ) } is non empty Subset of (ComplexVectSpace the carrier of X);

proof end;

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

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

Lm10: for X being non empty TopSpace

for v, u being Element of (CAlgebra the carrier of X) st v in CC_0_Functions X & u in CC_0_Functions X holds

v + u in CC_0_Functions X

proof end;

Lm11: for X being non empty TopSpace

for a being Complex

for u being Element of (CAlgebra the carrier of X) st u in CC_0_Functions X holds

a * u in CC_0_Functions X

proof end;

Lm12: for X being non empty TopSpace

for u being Element of (CAlgebra the carrier of X) st u in CC_0_Functions X holds

- u in CC_0_Functions X

proof end;

theorem :: CC0SP2:37

for X being non empty TopSpace

for W being non empty Subset of (CAlgebra the carrier of X) st W = CC_0_Functions X holds

W is Cadditively-linearly-closed

for W being non empty Subset of (CAlgebra the carrier of X) st W = CC_0_Functions X holds

W is Cadditively-linearly-closed

proof end;

registration

let X be non empty TopSpace;

correctness

coherence

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

by Th39;

end;
correctness

coherence

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

by Th39;

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

for V1 being Subset of V st V1 is linearly-closed & not V1 is empty holds

CLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V

proof end;

theorem Th41: :: CC0SP2:41

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

definition

let X be non empty TopSpace;

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

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;

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

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

for x being set st x in CC_0_Functions X holds

x in ComplexBoundedFunctions the carrier of X

proof end;

definition

let X be non empty TopSpace;

coherence

(ComplexBoundedFunctionsNorm the carrier of X) | (CC_0_Functions X) is Function of (CC_0_Functions X),REAL;

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

coherence

(ComplexBoundedFunctionsNorm the carrier of X) | (CC_0_Functions X) is Function of (CC_0_Functions X),REAL;

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

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;

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

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 ;

;

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

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;

correctness

coherence

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

;

end;
correctness

coherence

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

;

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

for x being set st x in CC_0_Functions X holds

x in CContinuousFunctions X

proof end;

Lm13: for X being non empty TopSpace

for x1, x2 being Point of (C_Normed_Space_of_C_0_Functions X)

for y1, y2 being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x1 = y1 & x2 = y2 holds

x1 + x2 = y1 + y2

proof end;

Lm14: for X being non empty TopSpace

for a being Complex

for x being Point of (C_Normed_Space_of_C_0_Functions X)

for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds

a * x = a * y

proof end;

theorem Th46: :: CC0SP2:46

for a being Complex

for X being non empty TopSpace

for F, G being Point of (C_Normed_Space_of_C_0_Functions X) holds

( ( ||.F.|| = 0 implies F = 0. (C_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (C_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

for X being non empty TopSpace

for F, G being Point of (C_Normed_Space_of_C_0_Functions X) holds

( ( ||.F.|| = 0 implies F = 0. (C_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (C_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

proof end;

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

by Th46;

registration

let X be non empty TopSpace;

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

end;
cluster C_Normed_Space_of_C_0_Functions X -> right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;

coherence ( C_Normed_Space_of_C_0_Functions X is reflexive & C_Normed_Space_of_C_0_Functions X is discerning & C_Normed_Space_of_C_0_Functions X is ComplexNormSpace-like & C_Normed_Space_of_C_0_Functions X is vector-distributive & C_Normed_Space_of_C_0_Functions X is scalar-distributive & C_Normed_Space_of_C_0_Functions X is scalar-associative & C_Normed_Space_of_C_0_Functions X is scalar-unital & C_Normed_Space_of_C_0_Functions X is Abelian & C_Normed_Space_of_C_0_Functions X is add-associative & C_Normed_Space_of_C_0_Functions X is right_zeroed & C_Normed_Space_of_C_0_Functions X is right_complementable )

proof end;

theorem :: CC0SP2:47