begin
:: deftheorem Def1 defines continuous CC0SP2:def 1 :
for X being TopStruct
for f being Function of the carrier of X,COMPLEX holds
( f is continuous iff for Y being Subset of COMPLEX st Y is closed holds
f " Y is closed );
:: deftheorem defines --> CC0SP2:def 2 :
for X being 1-sorted
for y being complex number holds X --> y = the carrier of X --> y;
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem Th8:
:: 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 } ;
definition
let X be non
empty TopSpace;
func C_Algebra_of_ContinuousFunctions X -> ComplexAlgebra equals
ComplexAlgebraStr(#
(CContinuousFunctions X),
(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),
(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),
(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),
(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),
(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) #);
coherence
ComplexAlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) #) is ComplexAlgebra
by CC0SP1:2;
end;
:: deftheorem defines C_Algebra_of_ContinuousFunctions CC0SP2:def 4 :
for X being non empty TopSpace holds C_Algebra_of_ContinuousFunctions X = ComplexAlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) #);
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
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
theorem
:: deftheorem defines CContinuousFunctionsNorm CC0SP2:def 5 :
for X being non empty compact TopSpace holds CContinuousFunctionsNorm X = (ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X);
definition
let X be non
empty compact TopSpace;
func C_Normed_Algebra_of_ContinuousFunctions X -> Normed_Complex_AlgebraStr equals
Normed_Complex_AlgebraStr(#
(CContinuousFunctions X),
(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),
(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),
(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),
(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),
(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),
(CContinuousFunctionsNorm X) #);
correctness
coherence
Normed_Complex_AlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(CContinuousFunctionsNorm X) #) is Normed_Complex_AlgebraStr ;
;
end;
:: deftheorem defines C_Normed_Algebra_of_ContinuousFunctions CC0SP2:def 6 :
for X being non empty compact TopSpace holds C_Normed_Algebra_of_ContinuousFunctions X = Normed_Complex_AlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(CContinuousFunctionsNorm X) #);
UNITAL:
now
let X be 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 )set F =
C_Normed_Algebra_of_ContinuousFunctions X;
let x,
e be
Element of
(C_Normed_Algebra_of_ContinuousFunctions X);
( 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))
;
( x * e = x & e * x = x )set X1 =
CContinuousFunctions X;
reconsider f =
x as
Element of
CContinuousFunctions X ;
1_ (CAlgebra the carrier of X) =
X --> 1
.=
1_ (C_Algebra_of_ContinuousFunctions X)
by Th14
;
then A2:
(
[f,(1_ (CAlgebra the carrier of X))] in [:(CContinuousFunctions X),(CContinuousFunctions X):] &
[(1_ (CAlgebra the carrier of X)),f] in [:(CContinuousFunctions X),(CContinuousFunctions X):] )
by ZFMISC_1:87;
x * e = (mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (
f,
(1_ (CAlgebra the carrier of X)))
by A1, C0SP1:def 8;
then
x * e = ( the multF of (CAlgebra the carrier of X) || (CContinuousFunctions X)) . (
f,
(1_ (CAlgebra the carrier of X)))
by C0SP1:def 6;
then
x * e = f * (1_ (CAlgebra the carrier of X))
by A2, FUNCT_1:49;
hence
x * e = x
by VECTSP_1:def 4;
e * x = x
e * x = (mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (
(1_ (CAlgebra the carrier of X)),
f)
by A1, C0SP1:def 8;
then
e * x = ( the multF of (CAlgebra the carrier of X) || (CContinuousFunctions X)) . (
(1_ (CAlgebra the carrier of X)),
f)
by C0SP1:def 6;
then
e * x = (1_ (CAlgebra the carrier of X)) * f
by A2, FUNCT_1:49;
hence
e * x = x
by VECTSP_1:def 4;
verum
end;
Lm2:
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;
Lm3:
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
Lm4:
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
Lm5:
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
theorem Th18:
theorem
theorem
theorem Th21:
Lm6:
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)
Lm7:
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)
theorem
theorem Th24:
theorem
theorem
theorem Th27a:
theorem Th27b:
theorem Th27c:
theorem Th27d:
Lm8:
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
theorem
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem
:: deftheorem defines CC_0_Functions CC0SP2:def 7 :
for X being non empty TopSpace holds CC_0_Functions X = { f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) ) } ;
theorem
Lm9:
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
Lm10:
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
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
theorem
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
definition
let X be non
empty TopSpace;
func C_VectorSpace_of_C_0_Functions X -> ComplexLinearSpace equals
CLSStruct(#
(CC_0_Functions X),
(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),
(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),
(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))) #);
correctness
coherence
CLSStruct(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))) #) is ComplexLinearSpace;
by Th40;
end;
:: deftheorem defines C_VectorSpace_of_C_0_Functions CC0SP2:def 8 :
for X being non empty TopSpace holds C_VectorSpace_of_C_0_Functions X = CLSStruct(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))) #);
theorem Th41:
:: deftheorem defines CC_0_FunctionsNorm CC0SP2:def 9 :
for X being non empty TopSpace holds CC_0_FunctionsNorm X = (ComplexBoundedFunctionsNorm the carrier of X) | (CC_0_Functions X);
definition
let X be non
empty TopSpace;
func C_Normed_Space_of_C_0_Functions X -> CNORMSTR equals
CNORMSTR(#
(CC_0_Functions X),
(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),
(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),
(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),
(CC_0_FunctionsNorm X) #);
correctness
coherence
CNORMSTR(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(CC_0_FunctionsNorm X) #) is CNORMSTR ;
;
end;
:: deftheorem defines C_Normed_Space_of_C_0_Functions CC0SP2:def 10 :
for X being non empty TopSpace holds C_Normed_Space_of_C_0_Functions X = CNORMSTR(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(CC_0_FunctionsNorm X) #);
theorem
theorem Th43:
theorem Th44:
Lm14:
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
Lm15:
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
theorem Th45:
Th46:
for X being non empty TopSpace holds C_Normed_Space_of_C_0_Functions X is ComplexNormSpace-like
theorem