begin
:: deftheorem defines --> C0SP2:def 1 :
theorem LMcont:
LmAlgebra:
for V being non empty right_complementable Abelian add-associative right_zeroed Algebra-like AlgebraStr st ( for v being VECTOR of holds 1 * v = v ) holds
V is RealLinearSpace
:: deftheorem defines ContinuousFunctions C0SP2:def 2 :
theorem
for
X being non
empty TopSpace holds
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
Subalgebra of
RAlgebra the
carrier of
X by C0SP1:6;
definition
let X be non
empty TopSpace;
func R_Algebra_of_ContinuousFunctions X -> AlgebraStr equals
AlgebraStr(#
(ContinuousFunctions X),
(mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(Add_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(One_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(Zero_ (ContinuousFunctions X),(RAlgebra the carrier of X)) #);
coherence
AlgebraStr(# (ContinuousFunctions X),(mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Add_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(One_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Zero_ (ContinuousFunctions X),(RAlgebra the carrier of X)) #) is AlgebraStr
;
end;
:: deftheorem defines R_Algebra_of_ContinuousFunctions C0SP2:def 3 :
for
X being non
empty TopSpace holds
R_Algebra_of_ContinuousFunctions X = AlgebraStr(#
(ContinuousFunctions X),
(mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(Add_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(One_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(Zero_ (ContinuousFunctions X),(RAlgebra the carrier of X)) #);
theorem ThB10:
theorem ThB11:
theorem ThB12:
theorem ThB12Zero:
theorem ThB12One:
theorem subalgebra:
LMX01:
for X being non empty compact TopSpace
for x being set st x in ContinuousFunctions X holds
x in BoundedFunctions the carrier of X
theorem
:: deftheorem defines ContinuousFunctionsNorm C0SP2:def 4 :
definition
let X be non
empty compact TopSpace;
func R_Normed_Algebra_of_ContinuousFunctions X -> Normed_AlgebraStr equals
Normed_AlgebraStr(#
(ContinuousFunctions X),
(mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(Add_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(One_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(Zero_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(ContinuousFunctionsNorm X) #);
correctness
coherence
Normed_AlgebraStr(# (ContinuousFunctions X),(mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Add_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(One_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(Zero_ (ContinuousFunctions X),(RAlgebra the carrier of X)),(ContinuousFunctionsNorm X) #) is Normed_AlgebraStr ;
;
end;
:: deftheorem defines R_Normed_Algebra_of_ContinuousFunctions C0SP2:def 5 :
for
X being non
empty compact TopSpace holds
R_Normed_Algebra_of_ContinuousFunctions X = Normed_AlgebraStr(#
(ContinuousFunctions X),
(mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(Add_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(One_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(Zero_ (ContinuousFunctions X),(RAlgebra the carrier of X)),
(ContinuousFunctionsNorm X) #);
UNITAL:
now
let X be non
empty compact TopSpace;
for x, e being Element of 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 ;
( 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)
;
( 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 ThB12One
;
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:106;
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:72;
hence
x * e = x
by FUNCSDOM:49;
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:72;
hence
e * x = x
by FUNCSDOM:49;
verum
end;
theorem RSSPACE34:
LMX02:
for X being non empty compact TopSpace
for x being Point of
for y being Point of st x = y holds
||.x.|| = ||.y.||
LMX03:
for X being non empty compact TopSpace
for x1, x2 being Point of
for y1, y2 being Point of st x1 = y1 & x2 = y2 holds
x1 + x2 = y1 + y2
LMX04:
for X being non empty compact TopSpace
for a being Real
for x being Point of
for y being Point of st x = y holds
a * x = a * y
LMX05:
for X being non empty compact TopSpace
for x1, x2 being Point of
for y1, y2 being Point of st x1 = y1 & x2 = y2 holds
x1 * x2 = y1 * y2
theorem FUNCSDOM23:
theorem ThB18:
LMX06:
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)
LMX07:
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)
theorem
theorem
theorem ThB22:
theorem
theorem
theorem ThB24:
LMX03a:
for X being non empty compact TopSpace
for x1, x2 being Point of
for y1, y2 being Point of st x1 = y1 & x2 = y2 holds
x1 - x2 = y1 - y2
theorem
theorem SUBSP1:
theorem SUBSP2:
theorem ThB28: