:: CC0SP2 semantic presentation
begin
definition
let X be TopStruct ;
let f be Function of the carrier of X,COMPLEX;
attrf is continuous means :Def1: :: CC0SP2:def 1
for Y being Subset of COMPLEX st Y is closed holds
f " Y is closed ;
end;
:: 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 );
definition
let X be 1-sorted ;
let y be complex number ;
funcX --> y -> Function of the carrier of X,COMPLEX equals :: CC0SP2:def 2
the carrier of X --> y;
coherence
the carrier of X --> y is Function of the carrier of X,COMPLEX
proof
y in COMPLEX by XCMPLX_0:def_2;
hence the carrier of X --> y is Function of the carrier of X,COMPLEX by FUNCOP_1:45; ::_thesis: verum
end;
end;
:: 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: :: CC0SP2:1
for X being non empty TopSpace
for y being complex number
for f being Function of the carrier of X,COMPLEX st f = X --> y holds
f is continuous
proof
let X be non empty TopSpace; ::_thesis: for y being complex number
for f being Function of the carrier of X,COMPLEX st f = X --> y holds
f is continuous
let y be complex number ; ::_thesis: for f being Function of the carrier of X,COMPLEX st f = X --> y holds
f is continuous
let f be Function of the carrier of X,COMPLEX; ::_thesis: ( f = X --> y implies f is continuous )
assume A1: f = X --> y ; ::_thesis: f is continuous
set H = the carrier of X;
set HX = [#] X;
let P1 be Subset of COMPLEX; :: according to CC0SP2:def_1 ::_thesis: ( P1 is closed implies f " P1 is closed )
assume P1 is closed ; ::_thesis: f " P1 is closed
percases ( y in P1 or not y in P1 ) ;
suppose y in P1 ; ::_thesis: f " P1 is closed
then f " P1 = [#] X by A1, FUNCOP_1:14;
hence f " P1 is closed ; ::_thesis: verum
end;
suppose not y in P1 ; ::_thesis: f " P1 is closed
then f " P1 = {} X by A1, FUNCOP_1:16;
hence f " P1 is closed ; ::_thesis: verum
end;
end;
end;
registration
let X be non empty TopSpace;
let y be complex number ;
clusterX --> y -> continuous ;
coherence
X --> y is continuous by Th1;
end;
registration
let X be non empty TopSpace;
cluster non empty Relation-like the carrier of X -defined COMPLEX -valued Function-like total quasi_total V139() continuous for Element of bool [: the carrier of X,COMPLEX:];
existence
ex b1 being Function of the carrier of X,COMPLEX st b1 is continuous
proof
take f = X --> 0c; ::_thesis: f is continuous
thus f is continuous ; ::_thesis: verum
end;
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 )
proof
let X be non empty TopSpace; ::_thesis: 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 )
let f be Function of the carrier of X,COMPLEX; ::_thesis: ( f is continuous iff for Y being Subset of COMPLEX st Y is open holds
f " Y is open )
hereby ::_thesis: ( ( for Y being Subset of COMPLEX st Y is open holds
f " Y is open ) implies f is continuous )
assume A1: f is continuous ; ::_thesis: for Y being Subset of COMPLEX st Y is open holds
f " Y is open
let Y be Subset of COMPLEX; ::_thesis: ( Y is open implies f " Y is open )
assume Y is open ; ::_thesis: f " Y is open
then Y ` is closed by CFDIFF_1:def_11;
then A2: f " (Y `) is closed by A1, Def1;
f " (Y `) = (f " COMPLEX) \ (f " Y) by FUNCT_1:69
.= ([#] X) \ (f " Y) by FUNCT_2:40 ;
then ([#] X) \ (([#] X) \ (f " Y)) is open by A2, PRE_TOPC:def_3;
hence f " Y is open by PRE_TOPC:3; ::_thesis: verum
end;
assume A3: for Y being Subset of COMPLEX st Y is open holds
f " Y is open ; ::_thesis: f is continuous
let Y be Subset of COMPLEX; :: according to CC0SP2:def_1 ::_thesis: ( Y is closed implies f " Y is closed )
assume A4: Y is closed ; ::_thesis: f " Y is closed
Y = (Y `) ` ;
then Y ` is open by A4, CFDIFF_1:def_11;
then A5: f " (Y `) is open by A3;
f " (Y `) = (f " COMPLEX) \ (f " Y) by FUNCT_1:69
.= ([#] X) \ (f " Y) by FUNCT_2:40 ;
hence f " Y is closed by A5, PRE_TOPC:def_3; ::_thesis: verum
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 ) )
proof
let X be non empty TopSpace; ::_thesis: 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 ) )
let f be Function of the carrier of X,COMPLEX; ::_thesis: ( 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 ) )
hereby ::_thesis: ( ( 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 ) ) implies f is continuous )
assume A1: f is continuous ; ::_thesis: 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 )
now__::_thesis:_for_x_being_Point_of_X
for_V_being_Subset_of_COMPLEX_st_f_._x_in_V_&_V_is_open_holds_
ex_W_being_Element_of_bool_the_carrier_of_X_st_
(_x_in_W_&_W_is_open_&_f_.:_W_c=_V_)
let x be Point of X; ::_thesis: for V being Subset of COMPLEX st f . x in V & V is open holds
ex W being Element of bool the carrier of X st
( x in W & W is open & f .: W c= V )
let V be Subset of COMPLEX; ::_thesis: ( f . x in V & V is open implies ex W being Element of bool the carrier of X st
( x in W & W is open & f .: W c= V ) )
set z = f . x;
reconsider z0 = f . x as Complex ;
assume ( f . x in V & V is open ) ; ::_thesis: ex W being Element of bool the carrier of X st
( x in W & W is open & f .: W c= V )
then consider N being Neighbourhood of z0 such that
A2: N c= V by CFDIFF_1:9;
consider g being Real such that
A3: ( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= N ) by CFDIFF_1:def_5;
set S = { y where y is Complex : |.(y - z0).| < g } ;
{ y where y is Complex : |.(y - z0).| < g } c= COMPLEX
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z0).| < g } or z in COMPLEX )
assume z in { y where y is Complex : |.(y - z0).| < g } ; ::_thesis: z in COMPLEX
then ex y being Complex st
( z = y & |.(y - z0).| < g ) ;
hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
end;
then reconsider S1 = { y where y is Complex : |.(y - z0).| < g } as Subset of COMPLEX ;
take W = f " { y where y is Complex : |.(y - z0).| < g } ; ::_thesis: ( x in W & W is open & f .: W c= V )
A4: S1 is open by CFDIFF_1:13;
{ y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0 by A3, CFDIFF_1:6;
then f . x in { y where y is Complex : |.(y - z0).| < g } by CFDIFF_1:7;
hence x in W by FUNCT_2:38; ::_thesis: ( W is open & f .: W c= V )
thus W is open by A1, A4, Th2; ::_thesis: f .: W c= V
f .: (f " { y where y is Complex : |.(y - z0).| < g } ) c= { y where y is Complex : |.(y - z0).| < g } by FUNCT_1:75;
then f .: W c= N by A3, XBOOLE_1:1;
hence f .: W c= V by A2, XBOOLE_1:1; ::_thesis: verum
end;
hence 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 ) ; ::_thesis: verum
end;
assume A5: 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 ) ; ::_thesis: f is continuous
now__::_thesis:_for_Y_being_Subset_of_COMPLEX_st_Y_is_closed_holds_
f_"_Y_is_closed
let Y be Subset of COMPLEX; ::_thesis: ( Y is closed implies f " Y is closed )
assume Y is closed ; ::_thesis: f " Y is closed
then (Y `) ` is closed ;
then A6: Y ` is open by CFDIFF_1:def_11;
for x being Point of X st x in (f " Y) ` holds
ex W being Subset of X st
( W is a_neighborhood of x & W c= (f " Y) ` )
proof
let x be Point of X; ::_thesis: ( x in (f " Y) ` implies ex W being Subset of X st
( W is a_neighborhood of x & W c= (f " Y) ` ) )
assume x in (f " Y) ` ; ::_thesis: ex W being Subset of X st
( W is a_neighborhood of x & W c= (f " Y) ` )
then x in f " (Y `) by FUNCT_2:100;
then f . x in Y ` by FUNCT_2:38;
then consider V being Subset of COMPLEX such that
A7: ( f . x in V & V is open & V c= Y ` ) by A6;
consider W being Subset of X such that
A8: ( x in W & W is open & f .: W c= V ) by A5, A7;
take W ; ::_thesis: ( W is a_neighborhood of x & W c= (f " Y) ` )
thus W is a_neighborhood of x by A8, CONNSP_2:3; ::_thesis: W c= (f " Y) `
f .: W c= Y ` by A7, A8, XBOOLE_1:1;
then A9: f " (f .: W) c= f " (Y `) by RELAT_1:143;
W c= f " (f .: W) by FUNCT_2:42;
then W c= f " (Y `) by A9, XBOOLE_1:1;
hence W c= (f " Y) ` by FUNCT_2:100; ::_thesis: verum
end;
then (f " Y) ` is open by CONNSP_2:7;
then ((f " Y) `) ` is closed by TOPS_1:4;
hence f " Y is closed ; ::_thesis: verum
end;
hence f is continuous by Def1; ::_thesis: verum
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
proof
let X be non empty TopSpace; ::_thesis: for f, g being continuous Function of the carrier of X,COMPLEX holds f + g is continuous Function of the carrier of X,COMPLEX
let f, g be continuous Function of the carrier of X,COMPLEX; ::_thesis: f + g is continuous Function of the carrier of X,COMPLEX
set h = f + g;
A1: rng (f + g) c= COMPLEX by MEMBERED:1;
dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1
.= the carrier of X /\ (dom g) by PARTFUN1:def_2
.= the carrier of X /\ the carrier of X by PARTFUN1:def_2 ;
then reconsider h = f + g as Function of the carrier of X,COMPLEX by A1, FUNCT_2:2;
A2: for x being Point of X holds h . x = (f . x) + (g . x) by VALUED_1:1;
for p being Point of X
for V being Subset of COMPLEX st h . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & h .: W c= V )
proof
let p be Point of X; ::_thesis: for V being Subset of COMPLEX st h . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & h .: W c= V )
let V be Subset of COMPLEX; ::_thesis: ( h . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & h .: W c= V ) )
assume A3: ( h . p in V & V is open ) ; ::_thesis: ex W being Subset of X st
( p in W & W is open & h .: W c= V )
reconsider z0 = h . p as Complex ;
consider N being Neighbourhood of z0 such that
A4: N c= V by A3, CFDIFF_1:9;
consider r being Real such that
A5: ( 0 < r & { y where y is Complex : |.(y - z0).| < r } c= N ) by CFDIFF_1:def_5;
set S = { y where y is Complex : |.(y - z0).| < r } ;
A6: r / 2 is Real by XREAL_0:def_1;
reconsider z1 = f . p as Complex ;
set S1 = { y where y is Complex : |.(y - z1).| < r / 2 } ;
{ y where y is Complex : |.(y - z1).| < r / 2 } c= COMPLEX
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z1).| < r / 2 } or z in COMPLEX )
assume z in { y where y is Complex : |.(y - z1).| < r / 2 } ; ::_thesis: z in COMPLEX
then ex y being Complex st
( z = y & |.(y - z1).| < r / 2 ) ;
hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
end;
then reconsider T1 = { y where y is Complex : |.(y - z1).| < r / 2 } as Subset of COMPLEX ;
A7: T1 is open by A6, CFDIFF_1:13;
|.(z1 - z1).| = 0 ;
then z1 in { y where y is Complex : |.(y - z1).| < r / 2 } by A5;
then consider W1 being Subset of X such that
A8: ( p in W1 & W1 is open & f .: W1 c= { y where y is Complex : |.(y - z1).| < r / 2 } ) by A7, Th3;
reconsider z2 = g . p as Complex ;
set S2 = { y where y is Complex : |.(y - z2).| < r / 2 } ;
{ y where y is Complex : |.(y - z2).| < r / 2 } c= COMPLEX
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z2).| < r / 2 } or z in COMPLEX )
assume z in { y where y is Complex : |.(y - z2).| < r / 2 } ; ::_thesis: z in COMPLEX
then ex y being Complex st
( z = y & |.(y - z2).| < r / 2 ) ;
hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
end;
then reconsider T2 = { y where y is Complex : |.(y - z2).| < r / 2 } as Subset of COMPLEX ;
A9: T2 is open by A6, CFDIFF_1:13;
|.(z2 - z2).| = 0 ;
then z2 in { y where y is Complex : |.(y - z2).| < r / 2 } by A5;
then consider W2 being Subset of X such that
A10: ( p in W2 & W2 is open & g .: W2 c= { y where y is Complex : |.(y - z2).| < r / 2 } ) by A9, Th3;
set W = W1 /\ W2;
A11: W1 /\ W2 is open by A8, A10, TOPS_1:11;
A12: p in W1 /\ W2 by A8, A10, XBOOLE_0:def_4;
h .: (W1 /\ W2) c= { y where y is Complex : |.(y - z0).| < r }
proof
let z3 be set ; :: according to TARSKI:def_3 ::_thesis: ( not z3 in h .: (W1 /\ W2) or z3 in { y where y is Complex : |.(y - z0).| < r } )
assume z3 in h .: (W1 /\ W2) ; ::_thesis: z3 in { y where y is Complex : |.(y - z0).| < r }
then consider x3 being set such that
A13: ( x3 in dom h & x3 in W1 /\ W2 & h . x3 = z3 ) by FUNCT_1:def_6;
A14: x3 in W1 by A13, XBOOLE_0:def_4;
reconsider px = x3 as Point of X by A13;
A15: px in the carrier of X ;
then px in dom f by FUNCT_2:def_1;
then f . px in f .: W1 by A14, FUNCT_1:def_6;
then A16: f . px in { y where y is Complex : |.(y - z1).| < r / 2 } by A8;
reconsider a1 = f . px as Complex ;
A17: ex aa1 being Complex st
( f . px = aa1 & |.(aa1 - z1).| < r / 2 ) by A16;
A18: x3 in W2 by A13, XBOOLE_0:def_4;
px in dom g by A15, FUNCT_2:def_1;
then g . px in g .: W2 by A18, FUNCT_1:def_6;
then A19: g . px in { y where y is Complex : |.(y - z2).| < r / 2 } by A10;
reconsider a2 = g . px as Complex ;
ex aa2 being Complex st
( g . px = aa2 & |.(aa2 - z2).| < r / 2 ) by A19;
then A20: |.(a2 - z2).| < r / 2 ;
|.((h . x3) - z0).| = |.(((f . px) + (g . px)) - z0).| by A2
.= |.(((f . px) + (g . px)) - ((f . p) + (g . p))).| by A2
.= |.((a1 - z1) + (a2 - z2)).| ;
then A21: |.((h . px) - z0).| <= |.(a1 - z1).| + |.(a2 - z2).| by COMPLEX1:56;
A22: |.(a1 - z1).| + |.(a2 - z2).| < (r / 2) + |.(a2 - z2).| by A17, XREAL_1:8;
(r / 2) + |.(a2 - z2).| < (r / 2) + (r / 2) by A20, XREAL_1:8;
then |.(a1 - z1).| + |.(a2 - z2).| < r by A22, XXREAL_0:2;
then |.((h . px) - z0).| < r by A21, XXREAL_0:2;
hence z3 in { y where y is Complex : |.(y - z0).| < r } by A13; ::_thesis: verum
end;
then h .: (W1 /\ W2) c= N by A5, XBOOLE_1:1;
hence ex W being Subset of X st
( p in W & W is open & h .: W c= V ) by A11, A12, A4, XBOOLE_1:1; ::_thesis: verum
end;
hence f + g is continuous Function of the carrier of X,COMPLEX by Th3; ::_thesis: verum
end;
theorem Th5: :: CC0SP2:5
for X being non empty TopSpace
for a being complex number
for f being continuous Function of the carrier of X,COMPLEX holds a (#) f is continuous Function of the carrier of X,COMPLEX
proof
let X be non empty TopSpace; ::_thesis: for a being complex number
for f being continuous Function of the carrier of X,COMPLEX holds a (#) f is continuous Function of the carrier of X,COMPLEX
let a be complex number ; ::_thesis: for f being continuous Function of the carrier of X,COMPLEX holds a (#) f is continuous Function of the carrier of X,COMPLEX
let f be continuous Function of the carrier of X,COMPLEX; ::_thesis: a (#) f is continuous Function of the carrier of X,COMPLEX
set h = a (#) f;
A1: for x being Point of X holds (a (#) f) . x = a * (f . x) by VALUED_1:6;
now__::_thesis:_a_(#)_f_is_continuous
percases ( a <> 0 or a = 0 ) ;
supposeA2: a <> 0 ; ::_thesis: a (#) f is continuous
for p being Point of X
for V being Subset of COMPLEX st (a (#) f) . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & (a (#) f) .: W c= V )
proof
let p be Point of X; ::_thesis: for V being Subset of COMPLEX st (a (#) f) . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & (a (#) f) .: W c= V )
let V be Subset of COMPLEX; ::_thesis: ( (a (#) f) . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & (a (#) f) .: W c= V ) )
assume A3: ( (a (#) f) . p in V & V is open ) ; ::_thesis: ex W being Subset of X st
( p in W & W is open & (a (#) f) .: W c= V )
reconsider z0 = (a (#) f) . p as Complex ;
consider N being Neighbourhood of z0 such that
A4: N c= V by A3, CFDIFF_1:9;
consider r being Real such that
A5: ( 0 < r & { y where y is Complex : |.(y - z0).| < r } c= N ) by CFDIFF_1:def_5;
set S = { y where y is Complex : |.(y - z0).| < r } ;
A6: |.a.| > 0 by A2;
A7: r / |.a.| is Real by XREAL_0:def_1;
A8: r / |.a.| > 0 by A2, A5;
reconsider z1 = f . p as Complex ;
set S1 = { y where y is Complex : |.(y - z1).| < r / |.a.| } ;
{ y where y is Complex : |.(y - z1).| < r / |.a.| } c= COMPLEX
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z1).| < r / |.a.| } or z in COMPLEX )
assume z in { y where y is Complex : |.(y - z1).| < r / |.a.| } ; ::_thesis: z in COMPLEX
then ex y being Complex st
( z = y & |.(y - z1).| < r / |.a.| ) ;
hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
end;
then reconsider T1 = { y where y is Complex : |.(y - z1).| < r / |.a.| } as Subset of COMPLEX ;
A9: T1 is open by A7, CFDIFF_1:13;
|.(z1 - z1).| = 0 ;
then z1 in { y where y is Complex : |.(y - z1).| < r / |.a.| } by A8;
then consider W1 being Subset of X such that
A10: ( p in W1 & W1 is open & f .: W1 c= { y where y is Complex : |.(y - z1).| < r / |.a.| } ) by A9, Th3;
set W = W1;
A11: W1 is open by A10;
A12: p in W1 by A10;
(a (#) f) .: W1 c= { y where y is Complex : |.(y - z0).| < r }
proof
let z3 be set ; :: according to TARSKI:def_3 ::_thesis: ( not z3 in (a (#) f) .: W1 or z3 in { y where y is Complex : |.(y - z0).| < r } )
assume z3 in (a (#) f) .: W1 ; ::_thesis: z3 in { y where y is Complex : |.(y - z0).| < r }
then consider x3 being set such that
A13: ( x3 in dom (a (#) f) & x3 in W1 & (a (#) f) . x3 = z3 ) by FUNCT_1:def_6;
reconsider px = x3 as Point of X by A13;
px in the carrier of X ;
then px in dom f by FUNCT_2:def_1;
then f . px in f .: W1 by A13, FUNCT_1:def_6;
then A14: f . px in { y where y is Complex : |.(y - z1).| < r / |.a.| } by A10;
reconsider a1 = f . px as Complex ;
ex aa1 being Complex st
( f . px = aa1 & |.(aa1 - z1).| < r / |.a.| ) by A14;
then A15: |.(a1 - z1).| < r / |.a.| ;
A16: |.(((a (#) f) . x3) - z0).| = |.((a * (f . px)) - z0).| by A1
.= |.((a * (f . px)) - (a * (f . p))).| by A1
.= |.(a * ((f . px) - (f . p))).|
.= |.a.| * |.(a1 - z1).| by COMPLEX1:65 ;
A17: |.a.| * |.(a1 - z1).| < |.a.| * (r / |.a.|) by A6, A15, XREAL_1:68;
|.a.| * (r / |.a.|) = r * (|.a.| / |.a.|)
.= r * 1 by A6, XCMPLX_1:60
.= r ;
then |.(((a (#) f) . px) - z0).| < r by A16, A17;
hence z3 in { y where y is Complex : |.(y - z0).| < r } by A13; ::_thesis: verum
end;
then (a (#) f) .: W1 c= N by A5, XBOOLE_1:1;
hence ex W being Subset of X st
( p in W & W is open & (a (#) f) .: W c= V ) by A11, A12, A4, XBOOLE_1:1; ::_thesis: verum
end;
hence a (#) f is continuous by Th3; ::_thesis: verum
end;
supposeA18: a = 0 ; ::_thesis: a (#) f is continuous
set g = X --> 0c;
set CX = the carrier of X;
A19: dom (X --> 0c) = the carrier of X by FUNCOP_1:13;
dom (a (#) f) = the carrier of X by FUNCT_2:def_1;
then A20: dom (X --> 0c) = dom (a (#) f) by A19;
for z being set st z in dom (a (#) f) holds
(X --> 0c) . z = (a (#) f) . z
proof
let z be set ; ::_thesis: ( z in dom (a (#) f) implies (X --> 0c) . z = (a (#) f) . z )
assume A21: z in dom (a (#) f) ; ::_thesis: (X --> 0c) . z = (a (#) f) . z
(a (#) f) . z = 0 * (f . z) by A18, VALUED_1:6
.= 0 ;
hence (X --> 0c) . z = (a (#) f) . z by A21, FUNCOP_1:7; ::_thesis: verum
end;
hence a (#) f is continuous by A20, FUNCT_1:def_11; ::_thesis: verum
end;
end;
end;
hence a (#) f is continuous Function of the carrier of X,COMPLEX ; ::_thesis: verum
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
proof
let X be non empty TopSpace; ::_thesis: for f, g being continuous Function of the carrier of X,COMPLEX holds f - g is continuous Function of the carrier of X,COMPLEX
let f, g be continuous Function of the carrier of X,COMPLEX; ::_thesis: f - g is continuous Function of the carrier of X,COMPLEX
(- 1) (#) g is continuous by Th5;
hence f - g is continuous Function of the carrier of X,COMPLEX by Th4; ::_thesis: verum
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
proof
let X be non empty TopSpace; ::_thesis: for f, g being continuous Function of the carrier of X,COMPLEX holds f (#) g is continuous Function of the carrier of X,COMPLEX
let f, g be continuous Function of the carrier of X,COMPLEX; ::_thesis: f (#) g is continuous Function of the carrier of X,COMPLEX
set h = f (#) g;
A1: for x being Point of X holds (f (#) g) . x = (f . x) * (g . x) by VALUED_1:5;
for p being Point of X
for V being Subset of COMPLEX st (f (#) g) . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & (f (#) g) .: W c= V )
proof
let p be Point of X; ::_thesis: for V being Subset of COMPLEX st (f (#) g) . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & (f (#) g) .: W c= V )
let V be Subset of COMPLEX; ::_thesis: ( (f (#) g) . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & (f (#) g) .: W c= V ) )
assume A2: ( (f (#) g) . p in V & V is open ) ; ::_thesis: ex W being Subset of X st
( p in W & W is open & (f (#) g) .: W c= V )
reconsider z0 = (f (#) g) . p as Complex ;
consider N being Neighbourhood of z0 such that
A3: N c= V by A2, CFDIFF_1:9;
consider r being Real such that
A4: ( 0 < r & { y where y is Complex : |.(y - z0).| < r } c= N ) by CFDIFF_1:def_5;
set S = { y where y is Complex : |.(y - z0).| < r } ;
reconsider z1 = f . p as Complex ;
reconsider z2 = g . p as Complex ;
set a = (|.z1.| + |.z2.|) + 1;
A5: r / ((|.z1.| + |.z2.|) + 1) is Real by XREAL_0:def_1;
set S1 = { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } ;
{ y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } c= COMPLEX
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } or z in COMPLEX )
assume z in { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } ; ::_thesis: z in COMPLEX
then ex y being Complex st
( z = y & |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) ) ;
hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
end;
then reconsider T1 = { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } as Subset of COMPLEX ;
A6: T1 is open by A5, CFDIFF_1:13;
|.(z1 - z1).| = 0 ;
then z1 in { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } by A4;
then consider W1 being Subset of X such that
A7: ( p in W1 & W1 is open & f .: W1 c= { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } ) by A6, Th3;
set S2 = { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } ;
{ y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } c= COMPLEX
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } or z in COMPLEX )
assume z in { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } ; ::_thesis: z in COMPLEX
then ex y being Complex st
( z = y & |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) ) ;
hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
end;
then reconsider T2 = { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } as Subset of COMPLEX ;
A8: T2 is open by A5, CFDIFF_1:13;
|.(z2 - z2).| = 0 ;
then z2 in { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } by A4;
then consider W2 being Subset of X such that
A9: ( p in W2 & W2 is open & g .: W2 c= { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } ) by A8, Th3;
set S3 = { y where y is Complex : |.(y - z1).| < 1 } ;
{ y where y is Complex : |.(y - z1).| < 1 } c= COMPLEX
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z1).| < 1 } or z in COMPLEX )
assume z in { y where y is Complex : |.(y - z1).| < 1 } ; ::_thesis: z in COMPLEX
then ex y being Complex st
( z = y & |.(y - z1).| < 1 ) ;
hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
end;
then reconsider T3 = { y where y is Complex : |.(y - z1).| < 1 } as Subset of COMPLEX ;
A10: T3 is open by CFDIFF_1:13;
|.(z1 - z1).| = 0 ;
then z1 in { y where y is Complex : |.(y - z1).| < 1 } ;
then consider W3 being Subset of X such that
A11: ( p in W3 & W3 is open & f .: W3 c= { y where y is Complex : |.(y - z1).| < 1 } ) by A10, Th3;
set W = (W1 /\ W2) /\ W3;
W1 /\ W2 is open by A7, A9, TOPS_1:11;
then A12: (W1 /\ W2) /\ W3 is open by A11, TOPS_1:11;
p in W1 /\ W2 by A7, A9, XBOOLE_0:def_4;
then A13: p in (W1 /\ W2) /\ W3 by A11, XBOOLE_0:def_4;
(f (#) g) .: ((W1 /\ W2) /\ W3) c= { y where y is Complex : |.(y - z0).| < r }
proof
let z3 be set ; :: according to TARSKI:def_3 ::_thesis: ( not z3 in (f (#) g) .: ((W1 /\ W2) /\ W3) or z3 in { y where y is Complex : |.(y - z0).| < r } )
assume z3 in (f (#) g) .: ((W1 /\ W2) /\ W3) ; ::_thesis: z3 in { y where y is Complex : |.(y - z0).| < r }
then consider x3 being set such that
A14: ( x3 in dom (f (#) g) & x3 in (W1 /\ W2) /\ W3 & (f (#) g) . x3 = z3 ) by FUNCT_1:def_6;
A15: x3 in W1 /\ W2 by A14, XBOOLE_0:def_4;
then A16: x3 in W1 by XBOOLE_0:def_4;
reconsider px = x3 as Point of X by A14;
A17: px in the carrier of X ;
then px in dom f by FUNCT_2:def_1;
then f . px in f .: W1 by A16, FUNCT_1:def_6;
then A18: f . px in { y where y is Complex : |.(y - z1).| < r / ((|.z1.| + |.z2.|) + 1) } by A7;
reconsider a1 = f . px as Complex ;
ex aa1 being Complex st
( f . px = aa1 & |.(aa1 - z1).| < r / ((|.z1.| + |.z2.|) + 1) ) by A18;
then A19: |.(a1 - z1).| < r / ((|.z1.| + |.z2.|) + 1) ;
A20: x3 in W2 by A15, XBOOLE_0:def_4;
px in dom g by A17, FUNCT_2:def_1;
then g . px in g .: W2 by A20, FUNCT_1:def_6;
then A21: g . px in { y where y is Complex : |.(y - z2).| < r / ((|.z1.| + |.z2.|) + 1) } by A9;
reconsider a2 = g . px as Complex ;
ex aa2 being Complex st
( g . px = aa2 & |.(aa2 - z2).| < r / ((|.z1.| + |.z2.|) + 1) ) by A21;
then A22: |.(a2 - z2).| < r / ((|.z1.| + |.z2.|) + 1) ;
A23: x3 in W3 by A14, XBOOLE_0:def_4;
px in dom f by A17, FUNCT_2:def_1;
then f . px in f .: W3 by A23, FUNCT_1:def_6;
then A24: f . px in { y where y is Complex : |.(y - z1).| < 1 } by A11;
reconsider a3 = f . px as Complex ;
ex aa3 being Complex st
( f . px = aa3 & |.(aa3 - z1).| < 1 ) by A24;
then A25: |.(a3 - z1).| < 1 ;
|.((a1 - z1) + z1).| <= |.(a1 - z1).| + |.z1.| by COMPLEX1:56;
then |.a1.| - |.z1.| <= (|.(a1 - z1).| + |.z1.|) - |.z1.| by XREAL_1:9;
then |.a1.| - |.z1.| < 1 by A25, XXREAL_0:2;
then (|.a1.| - |.z1.|) + |.z1.| < 1 + |.z1.| by XREAL_1:8;
then A26: |.a1.| < 1 + |.z1.| ;
A27: |.(((f (#) g) . x3) - z0).| = |.(((f . px) * (g . px)) - z0).| by A1
.= |.((a1 * a2) - (z1 * z2)).| by A1
.= |.(((a1 * a2) - (a1 * z2)) + ((a1 * z2) - (z1 * z2))).| ;
A28: |.(((f (#) g) . x3) - z0).| <= |.((a1 * a2) - (a1 * z2)).| + |.((a1 * z2) - (z1 * z2)).| by A27, COMPLEX1:56;
|.((a1 * a2) - (a1 * z2)).| + |.((a1 * z2) - (z1 * z2)).| = |.(a1 * (a2 - z2)).| + |.(z2 * (a1 - z1)).|
.= (|.a1.| * |.(a2 - z2).|) + |.(z2 * (a1 - z1)).| by COMPLEX1:65
.= (|.a1.| * |.(a2 - z2).|) + (|.z2.| * |.(a1 - z1).|) by COMPLEX1:65 ;
then A29: |.(((f (#) g) . x3) - z0).| <= (|.a1.| * |.(a2 - z2).|) + (|.z2.| * |.(a1 - z1).|) by A28;
A30: |.a1.| * |.(a2 - z2).| <= |.a1.| * (r / ((|.z1.| + |.z2.|) + 1)) by A22, XREAL_1:66;
|.a1.| * (r / ((|.z1.| + |.z2.|) + 1)) < (1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1)) by A26, A4, XREAL_1:68;
then A31: |.a1.| * |.(a2 - z2).| < (1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1)) by A30, XXREAL_0:2;
A32: |.z2.| * |.(a1 - z1).| <= |.z2.| * (r / ((|.z1.| + |.z2.|) + 1)) by A19, XREAL_1:66;
A33: (|.a1.| * |.(a2 - z2).|) + (|.z2.| * |.(a1 - z1).|) < ((1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))) + (|.z2.| * |.(a1 - z1).|) by A31, XREAL_1:8;
((1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))) + (|.z2.| * |.(a1 - z1).|) <= ((1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))) + (|.z2.| * (r / ((|.z1.| + |.z2.|) + 1))) by A32, XREAL_1:6;
then (|.a1.| * |.(a2 - z2).|) + (|.z2.| * |.(a1 - z1).|) < ((1 + |.z1.|) * (r / ((|.z1.| + |.z2.|) + 1))) + (|.z2.| * (r / ((|.z1.| + |.z2.|) + 1))) by A33, XXREAL_0:2;
then A34: |.(((f (#) g) . x3) - z0).| < r * (((|.z1.| + |.z2.|) + 1) / ((|.z1.| + |.z2.|) + 1)) by A29, XXREAL_0:2;
((|.z1.| + |.z2.|) + 1) / ((|.z1.| + |.z2.|) + 1) = 1 by XCMPLX_0:def_7;
then |.(((f (#) g) . px) - z0).| < r by A34;
hence z3 in { y where y is Complex : |.(y - z0).| < r } by A14; ::_thesis: verum
end;
then (f (#) g) .: ((W1 /\ W2) /\ W3) c= N by A4, XBOOLE_1:1;
hence ex W being Subset of X st
( p in W & W is open & (f (#) g) .: W c= V ) by A12, A13, A3, XBOOLE_1:1; ::_thesis: verum
end;
hence f (#) g is continuous Function of the carrier of X,COMPLEX by Th3; ::_thesis: verum
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 )
proof
let X be non empty TopSpace; ::_thesis: for f being continuous Function of the carrier of X,COMPLEX holds
( |.f.| is Function of the carrier of X,REAL & |.f.| is continuous )
let f be continuous Function of the carrier of X,COMPLEX; ::_thesis: ( |.f.| is Function of the carrier of X,REAL & |.f.| is continuous )
reconsider h = |.f.| as Function of the carrier of X,REAL ;
for p being Point of X
for V being Subset of REAL st h . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & h .: W c= V )
proof
let p be Point of X; ::_thesis: for V being Subset of REAL st h . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & h .: W c= V )
let V be Subset of REAL; ::_thesis: ( h . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & h .: W c= V ) )
assume A1: ( h . p in V & V is open ) ; ::_thesis: ex W being Subset of X st
( p in W & W is open & h .: W c= V )
reconsider r0 = h . p as Real ;
consider r being real number such that
A2: ( 0 < r & ].(r0 - r),(r0 + r).[ c= V ) by A1, RCOMP_1:19;
set S = ].(r0 - r),(r0 + r).[;
reconsider z1 = f . p as Complex ;
set S1 = { y where y is Complex : |.(y - z1).| < r } ;
{ y where y is Complex : |.(y - z1).| < r } c= COMPLEX
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z1).| < r } or z in COMPLEX )
assume z in { y where y is Complex : |.(y - z1).| < r } ; ::_thesis: z in COMPLEX
then ex y being Complex st
( z = y & |.(y - z1).| < r ) ;
hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
end;
then reconsider T1 = { y where y is Complex : |.(y - z1).| < r } as Subset of COMPLEX ;
r is Real by XREAL_0:def_1;
then A3: T1 is open by CFDIFF_1:13;
|.(z1 - z1).| = 0 ;
then z1 in { y where y is Complex : |.(y - z1).| < r } by A2;
then consider W1 being Subset of X such that
A4: ( p in W1 & W1 is open & f .: W1 c= { y where y is Complex : |.(y - z1).| < r } ) by A3, Th3;
set W = W1;
A5: W1 is open by A4;
A6: p in W1 by A4;
h .: W1 c= ].(r0 - r),(r0 + r).[
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in h .: W1 or x in ].(r0 - r),(r0 + r).[ )
assume x in h .: W1 ; ::_thesis: x in ].(r0 - r),(r0 + r).[
then consider z being set such that
A7: ( z in dom h & z in W1 & h . z = x ) by FUNCT_1:def_6;
A8: z in W1 by A7;
reconsider pz = z as Point of X by A7;
pz in the carrier of X ;
then pz in dom f by FUNCT_2:def_1;
then f . pz in f .: W1 by A8, FUNCT_1:def_6;
then A9: f . pz in { y where y is Complex : |.(y - z1).| < r } by A4;
reconsider a1 = f . pz as Complex ;
ex aa1 being Complex st
( f . pz = aa1 & |.(aa1 - z1).| < r ) by A9;
then A10: |.(a1 - z1).| < r ;
A11: |.((h . z) - r0).| = |.(|.(f . pz).| - (|.f.| . p)).| by VALUED_1:18
.= |.(|.(f . pz).| - |.(f . p).|).| by VALUED_1:18 ;
|.(|.(f . pz).| - |.(f . p).|).| <= |.((f . pz) - (f . p)).| by COMPLEX1:64;
then |.(|.(f . pz).| - |.(f . p).|).| < r by A10, XXREAL_0:2;
hence x in ].(r0 - r),(r0 + r).[ by A7, A11, RCOMP_1:1; ::_thesis: verum
end;
hence ex W being Subset of X st
( p in W & W is open & h .: W c= V ) by A5, A6, A2, XBOOLE_1:1; ::_thesis: verum
end;
hence ( |.f.| is Function of the carrier of X,REAL & |.f.| is continuous ) by C0SP2:1; ::_thesis: verum
end;
definition
let X be non empty TopSpace;
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
coherence
{ f where f is continuous Function of the carrier of X,COMPLEX : verum } is Subset of (CAlgebra the carrier of X);
proof
set A = { f where f is continuous Function of the carrier of X,COMPLEX : verum } ;
{ f where f is continuous Function of the carrier of X,COMPLEX : verum } c= Funcs ( the carrier of X,COMPLEX)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { f where f is continuous Function of the carrier of X,COMPLEX : verum } or x in Funcs ( the carrier of X,COMPLEX) )
assume x in { f where f is continuous Function of the carrier of X,COMPLEX : verum } ; ::_thesis: x in Funcs ( the carrier of X,COMPLEX)
then ex f being continuous Function of the carrier of X,COMPLEX st x = f ;
hence x in Funcs ( the carrier of X,COMPLEX) by FUNCT_2:8; ::_thesis: verum
end;
hence { f where f is continuous Function of the carrier of X,COMPLEX : verum } is Subset of (CAlgebra the carrier of X) ; ::_thesis: verum
end;
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 } ;
registration
let X be non empty TopSpace;
cluster CContinuousFunctions X -> non empty ;
coherence
not CContinuousFunctions X is empty
proof
X --> 0c in { f where f is continuous Function of the carrier of X,COMPLEX : verum } ;
hence not CContinuousFunctions X is empty ; ::_thesis: verum
end;
end;
registration
let X be non empty TopSpace;
cluster CContinuousFunctions X -> multiplicatively-closed Cadditively-linearly-closed ;
coherence
( CContinuousFunctions X is Cadditively-linearly-closed & CContinuousFunctions X is multiplicatively-closed )
proof
set W = CContinuousFunctions X;
set V = CAlgebra the carrier of X;
for v, u being Element of (CAlgebra the carrier of X) st v in CContinuousFunctions X & u in CContinuousFunctions X holds
v + u in CContinuousFunctions X
proof
let v, u be Element of (CAlgebra the carrier of X); ::_thesis: ( v in CContinuousFunctions X & u in CContinuousFunctions X implies v + u in CContinuousFunctions X )
assume A1: ( v in CContinuousFunctions X & u in CContinuousFunctions X ) ; ::_thesis: v + u in CContinuousFunctions X
consider v1 being continuous Function of the carrier of X,COMPLEX such that
A2: v1 = v by A1;
consider u1 being continuous Function of the carrier of X,COMPLEX such that
A3: u1 = u by A1;
reconsider h = v + u as Element of Funcs ( the carrier of X,COMPLEX) ;
A4: ex f being Function st
( h = f & dom f = the carrier of X & rng f c= COMPLEX ) by FUNCT_2:def_2;
(dom v1) /\ (dom u1) = the carrier of X /\ (dom u1) by FUNCT_2:def_1;
then A5: (dom v1) /\ (dom u1) = the carrier of X /\ the carrier of X by FUNCT_2:def_1;
for x being set st x in dom h holds
h . x = (v1 . x) + (u1 . x) by A2, A3, CFUNCDOM:1;
then A6: v + u = v1 + u1 by A5, A4, VALUED_1:def_1;
v1 + u1 is continuous Function of the carrier of X,COMPLEX by Th4;
hence v + u in CContinuousFunctions X by A6; ::_thesis: verum
end;
then A7: CContinuousFunctions X is add-closed by IDEAL_1:def_1;
for v being Element of (CAlgebra the carrier of X) st v in CContinuousFunctions X holds
- v in CContinuousFunctions X
proof
let v be Element of (CAlgebra the carrier of X); ::_thesis: ( v in CContinuousFunctions X implies - v in CContinuousFunctions X )
assume A8: v in CContinuousFunctions X ; ::_thesis: - v in CContinuousFunctions X
consider v1 being continuous Function of the carrier of X,COMPLEX such that
A9: v1 = v by A8;
reconsider h = - v, v2 = v as Element of Funcs ( the carrier of X,COMPLEX) ;
reconsider e = - 1r as Complex ;
A10: h = e * v by CLVECT_1:3;
A11: ex f being Function st
( h = f & dom f = the carrier of X & rng f c= COMPLEX ) by FUNCT_2:def_2;
A12: dom v1 = the carrier of X by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_h_holds_
h_._x_=_-_(v1_._x)
let x be set ; ::_thesis: ( x in dom h implies h . x = - (v1 . x) )
assume x in dom h ; ::_thesis: h . x = - (v1 . x)
then reconsider y = x as Element of the carrier of X ;
h . x = (- 1) * (v2 . y) by A10, CFUNCDOM:4;
hence h . x = - (v1 . x) by A9; ::_thesis: verum
end;
then A13: - v = - v1 by A12, A11, VALUED_1:9;
e (#) v1 is continuous Function of the carrier of X,COMPLEX by Th5;
hence - v in CContinuousFunctions X by A13; ::_thesis: verum
end;
then A14: CContinuousFunctions X is having-inverse by C0SP1:def_1;
for a being Complex
for u being Element of (CAlgebra the carrier of X) st u in CContinuousFunctions X holds
a * u in CContinuousFunctions X
proof
let a be Complex; ::_thesis: for u being Element of (CAlgebra the carrier of X) st u in CContinuousFunctions X holds
a * u in CContinuousFunctions X
let u be Element of (CAlgebra the carrier of X); ::_thesis: ( u in CContinuousFunctions X implies a * u in CContinuousFunctions X )
assume A15: u in CContinuousFunctions X ; ::_thesis: a * u in CContinuousFunctions X
consider u1 being continuous Function of the carrier of X,COMPLEX such that
A16: u1 = u by A15;
reconsider h = a * u as Element of Funcs ( the carrier of X,COMPLEX) ;
A17: ex f being Function st
( h = f & dom f = the carrier of X & rng f c= COMPLEX ) by FUNCT_2:def_2;
A18: dom u1 = the carrier of X by FUNCT_2:def_1;
a in COMPLEX by XCMPLX_0:def_2;
then for x being set st x in dom h holds
h . x = a * (u1 . x) by A16, CFUNCDOM:4;
then A19: a * u = a (#) u1 by A18, A17, VALUED_1:def_5;
a (#) u1 is continuous Function of the carrier of X,COMPLEX by Th5;
hence a * u in CContinuousFunctions X by A19; ::_thesis: verum
end;
hence CContinuousFunctions X is Cadditively-linearly-closed by A7, A14, CC0SP1:def_2; ::_thesis: CContinuousFunctions X is multiplicatively-closed
A20: for v, u being Element of (CAlgebra the carrier of X) st v in CContinuousFunctions X & u in CContinuousFunctions X holds
v * u in CContinuousFunctions X
proof
let v, u be Element of (CAlgebra the carrier of X); ::_thesis: ( v in CContinuousFunctions X & u in CContinuousFunctions X implies v * u in CContinuousFunctions X )
assume A21: ( v in CContinuousFunctions X & u in CContinuousFunctions X ) ; ::_thesis: v * u in CContinuousFunctions X
consider v1 being continuous Function of the carrier of X,COMPLEX such that
A22: v1 = v by A21;
consider u1 being continuous Function of the carrier of X,COMPLEX such that
A23: u1 = u by A21;
reconsider h = v * u as Element of Funcs ( the carrier of X,COMPLEX) ;
A24: ex f being Function st
( h = f & dom f = the carrier of X & rng f c= COMPLEX ) by FUNCT_2:def_2;
(dom v1) /\ (dom u1) = the carrier of X /\ (dom u1) by FUNCT_2:def_1;
then A25: (dom v1) /\ (dom u1) = the carrier of X /\ the carrier of X by FUNCT_2:def_1;
for x being set st x in dom h holds
h . x = (v1 . x) * (u1 . x) by A22, A23, CFUNCDOM:2;
then A26: v * u = v1 (#) u1 by A25, A24, VALUED_1:def_4;
v1 (#) u1 is continuous Function of the carrier of X,COMPLEX by Th7;
hence v * u in CContinuousFunctions X by A26; ::_thesis: verum
end;
reconsider g = ComplexFuncUnit the carrier of X as Function of the carrier of X,COMPLEX ;
g = X --> 1r ;
then 1. (CAlgebra the carrier of X) in CContinuousFunctions X ;
hence CContinuousFunctions X is multiplicatively-closed by A20, C0SP1:def_4; ::_thesis: verum
end;
end;
definition
let X be non empty TopSpace;
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))) #) 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 :: 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;
cluster C_Algebra_of_ContinuousFunctions X -> strict ;
coherence
( C_Algebra_of_ContinuousFunctions X is strict & not C_Algebra_of_ContinuousFunctions X is empty ) ;
end;
registration
let X be non empty TopSpace;
cluster C_Algebra_of_ContinuousFunctions X -> scalar-unital ;
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
now__::_thesis:_for_v_being_VECTOR_of_(C_Algebra_of_ContinuousFunctions_X)_holds_1r_*_v_=_v
let v be VECTOR of (C_Algebra_of_ContinuousFunctions X); ::_thesis: 1r * v = v
reconsider v1 = v as VECTOR of (CAlgebra the carrier of X) by TARSKI:def_3;
C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2;
then 1r * v = 1r * v1 by CC0SP1:3;
hence 1r * v = v by CFUNCDOM:12; ::_thesis: verum
end;
hence ( 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 ) by CLVECT_1:def_5; ::_thesis: verum
end;
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) )
proof
let X be non empty TopSpace; ::_thesis: 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) )
let F, G, H be VECTOR of (C_Algebra_of_ContinuousFunctions X); ::_thesis: 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) )
let f, g, h be Function of the carrier of X,COMPLEX; ::_thesis: ( f = F & g = G & h = H implies ( H = F + G iff for x being Element of the carrier of X holds h . x = (f . x) + (g . x) ) )
assume A1: ( f = F & g = G & h = H ) ; ::_thesis: ( H = F + G iff for x being Element of the carrier of X holds h . x = (f . x) + (g . x) )
A2: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2;
reconsider f1 = F, g1 = G, h1 = H as VECTOR of (CAlgebra the carrier of X) by TARSKI:def_3;
hereby ::_thesis: ( ( for x being Element of the carrier of X holds h . x = (f . x) + (g . x) ) implies H = F + G )
assume A3: H = F + G ; ::_thesis: for x being Element of the carrier of X holds h . x = (f . x) + (g . x)
let x be Element of the carrier of X; ::_thesis: h . x = (f . x) + (g . x)
h1 = f1 + g1 by A2, A3, CC0SP1:3;
hence h . x = (f . x) + (g . x) by A1, CFUNCDOM:1; ::_thesis: verum
end;
assume for x being Element of X holds h . x = (f . x) + (g . x) ; ::_thesis: H = F + G
then h1 = f1 + g1 by A1, CFUNCDOM:1;
hence H = F + G by A2, CC0SP1:3; ::_thesis: verum
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) )
proof
let X be non empty TopSpace; ::_thesis: 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) )
let F, G be VECTOR of (C_Algebra_of_ContinuousFunctions X); ::_thesis: 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) )
let f, g be Function of the carrier of X,COMPLEX; ::_thesis: 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) )
let a be Complex; ::_thesis: ( f = F & g = G implies ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) )
assume A1: ( f = F & g = G ) ; ::_thesis: ( G = a * F iff for x being Element of X holds g . x = a * (f . x) )
A2: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2;
reconsider f1 = F, g1 = G as VECTOR of (CAlgebra the carrier of X) by TARSKI:def_3;
A3: a in COMPLEX by XCMPLX_0:def_2;
hereby ::_thesis: ( ( for x being Element of X holds g . x = a * (f . x) ) implies G = a * F )
assume A4: G = a * F ; ::_thesis: for x being Element of the carrier of X holds g . x = a * (f . x)
let x be Element of the carrier of X; ::_thesis: g . x = a * (f . x)
g1 = a * f1 by A2, A4, CC0SP1:3;
hence g . x = a * (f . x) by A1, A3, CFUNCDOM:4; ::_thesis: verum
end;
assume for x being Element of the carrier of X holds g . x = a * (f . x) ; ::_thesis: G = a * F
then g1 = a * f1 by A1, A3, CFUNCDOM:4;
hence G = a * F by A2, CC0SP1:3; ::_thesis: verum
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) )
proof
let X be non empty TopSpace; ::_thesis: 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) )
let F, G, H be VECTOR of (C_Algebra_of_ContinuousFunctions X); ::_thesis: 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) )
let f, g, h be Function of the carrier of X,COMPLEX; ::_thesis: ( f = F & g = G & h = H implies ( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) ) )
assume A1: ( f = F & g = G & h = H ) ; ::_thesis: ( H = F * G iff for x being Element of the carrier of X holds h . x = (f . x) * (g . x) )
A2: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2;
reconsider f1 = F, g1 = G, h1 = H as VECTOR of (CAlgebra the carrier of X) by TARSKI:def_3;
hereby ::_thesis: ( ( for x being Element of the carrier of X holds h . x = (f . x) * (g . x) ) implies H = F * G )
assume A3: H = F * G ; ::_thesis: for x being Element of the carrier of X holds h . x = (f . x) * (g . x)
let x be Element of the carrier of X; ::_thesis: h . x = (f . x) * (g . x)
h1 = f1 * g1 by A2, A3, CC0SP1:3;
hence h . x = (f . x) * (g . x) by A1, CFUNCDOM:2; ::_thesis: verum
end;
assume for x being Element of X holds h . x = (f . x) * (g . x) ; ::_thesis: H = F * G
then h1 = f1 * g1 by A1, CFUNCDOM:2;
hence H = F * G by A2, CC0SP1:3; ::_thesis: verum
end;
theorem Th13: :: CC0SP2:13
for X being non empty TopSpace holds 0. (C_Algebra_of_ContinuousFunctions X) = X --> 0c
proof
let X be non empty TopSpace; ::_thesis: 0. (C_Algebra_of_ContinuousFunctions X) = X --> 0c
A1: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2;
0. (CAlgebra the carrier of X) = X --> 0c ;
hence 0. (C_Algebra_of_ContinuousFunctions X) = X --> 0 by A1, CC0SP1:3; ::_thesis: verum
end;
theorem Th14: :: CC0SP2:14
for X being non empty TopSpace holds 1_ (C_Algebra_of_ContinuousFunctions X) = X --> 1r
proof
let X be non empty TopSpace; ::_thesis: 1_ (C_Algebra_of_ContinuousFunctions X) = X --> 1r
A1: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2;
1_ (CAlgebra the carrier of X) = X --> 1r ;
hence 1_ (C_Algebra_of_ContinuousFunctions X) = X --> 1r by A1, CC0SP1:3; ::_thesis: verum
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
proof
let A be ComplexAlgebra; ::_thesis: for A1, A2 being ComplexSubAlgebra of A st the carrier of A1 c= the carrier of A2 holds
A1 is ComplexSubAlgebra of A2
let A1, A2 be ComplexSubAlgebra of A; ::_thesis: ( the carrier of A1 c= the carrier of A2 implies A1 is ComplexSubAlgebra of A2 )
assume A1: the carrier of A1 c= the carrier of A2 ; ::_thesis: A1 is ComplexSubAlgebra of A2
set CA1 = the carrier of A1;
set CA2 = the carrier of A2;
set AA = the addF of A;
set mA = the multF of A;
set MA = the Mult of A;
A2: ( 0. A1 = 0. A & 0. A2 = 0. A & 1. A1 = 1. A & 1. A2 = 1. A ) by CC0SP1:def_1;
A3: the addF of A1 = the addF of A2 || the carrier of A1
proof
( the addF of A1 = the addF of A || the carrier of A1 & the addF of A2 = the addF of A || the carrier of A2 & [: the carrier of A1, the carrier of A1:] c= [: the carrier of A2, the carrier of A2:] ) by A1, CC0SP1:def_1, ZFMISC_1:96;
hence the addF of A1 = the addF of A2 || the carrier of A1 by FUNCT_1:51; ::_thesis: verum
end;
A4: the multF of A1 = the multF of A2 || the carrier of A1
proof
( the multF of A1 = the multF of A || the carrier of A1 & the multF of A2 = the multF of A || the carrier of A2 & [: the carrier of A1, the carrier of A1:] c= [: the carrier of A2, the carrier of A2:] ) by A1, CC0SP1:def_1, ZFMISC_1:96;
hence the multF of A1 = the multF of A2 || the carrier of A1 by FUNCT_1:51; ::_thesis: verum
end;
the Mult of A1 = the Mult of A2 | [:COMPLEX, the carrier of A1:]
proof
( the Mult of A1 = the Mult of A | [:COMPLEX, the carrier of A1:] & the Mult of A2 = the Mult of A | [:COMPLEX, the carrier of A2:] & [:COMPLEX, the carrier of A1:] c= [:COMPLEX, the carrier of A2:] ) by A1, CC0SP1:def_1, ZFMISC_1:96;
hence the Mult of A1 = the Mult of A2 | [:COMPLEX, the carrier of A1:] by FUNCT_1:51; ::_thesis: verum
end;
hence A1 is ComplexSubAlgebra of A2 by A1, A2, A3, A4, CC0SP1:def_1; ::_thesis: verum
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
let X be non empty compact TopSpace; ::_thesis: for x being set st x in CContinuousFunctions X holds
x in ComplexBoundedFunctions the carrier of X
let x be set ; ::_thesis: ( x in CContinuousFunctions X implies x in ComplexBoundedFunctions the carrier of X )
assume x in CContinuousFunctions X ; ::_thesis: x in ComplexBoundedFunctions the carrier of X
then consider h being continuous Function of the carrier of X,COMPLEX such that
A1: x = h ;
( |.h.| is Function of the carrier of X,REAL & |.h.| is continuous ) by Th8;
then consider h1 being Function of the carrier of X,REAL such that
A2: ( h1 = |.h.| & h1 is continuous ) ;
( h1 is bounded_above & h1 is bounded_below ) by A2, SEQ_2:def_8;
then consider r1 being real number such that
A3: for y being set st y in dom h1 holds
h1 . y < r1 by SEQ_2:def_1;
A4: for y being set st y in dom h holds
abs (h . y) < r1
proof
let y be set ; ::_thesis: ( y in dom h implies abs (h . y) < r1 )
assume A5: y in dom h ; ::_thesis: abs (h . y) < r1
A6: dom h1 = dom h by A2, VALUED_1:def_11;
h1 . y = |.(h . y).| by A2, VALUED_1:18
.= abs (h . y) ;
hence abs (h . y) < r1 by A3, A5, A6; ::_thesis: verum
end;
h is bounded by A4, COMSEQ_2:def_3;
then h | the carrier of X is bounded by FUNCT_2:33;
hence x in ComplexBoundedFunctions the carrier of X by A1; ::_thesis: verum
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
let X be non empty compact TopSpace; ::_thesis: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of C_Algebra_of_BoundedFunctions the carrier of X
A1: the carrier of (C_Algebra_of_ContinuousFunctions X) c= the carrier of (C_Algebra_of_BoundedFunctions the carrier of X)
proof
for x being set st x in CContinuousFunctions X holds
x in ComplexBoundedFunctions the carrier of X by Lm1;
hence the carrier of (C_Algebra_of_ContinuousFunctions X) c= the carrier of (C_Algebra_of_BoundedFunctions the carrier of X) by TARSKI:def_3; ::_thesis: verum
end;
A2: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2;
C_Algebra_of_BoundedFunctions the carrier of X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:4;
hence C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of C_Algebra_of_BoundedFunctions the carrier of X by A1, A2, Th15; ::_thesis: verum
end;
definition
let X be non empty compact TopSpace;
func CContinuousFunctionsNorm X -> Function of (CContinuousFunctions X),REAL equals :: CC0SP2:def 5
(ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X);
correctness
coherence
(ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X) is Function of (CContinuousFunctions X),REAL;
proof
for x being set st x in CContinuousFunctions X holds
x in ComplexBoundedFunctions the carrier of X by Lm1;
then CContinuousFunctions X c= ComplexBoundedFunctions the carrier of X by TARSKI:def_3;
hence (ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X) is Function of (CContinuousFunctions X),REAL by FUNCT_2:32; ::_thesis: verum
end;
end;
:: 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 :: 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
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) #);
registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> non empty strict ;
correctness
coherence
( not C_Normed_Algebra_of_ContinuousFunctions X is empty & C_Normed_Algebra_of_ContinuousFunctions X is strict );
;
end;
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_)
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 by VECTSP_1:def_4; ::_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 by VECTSP_1:def_4; ::_thesis: verum
end;
registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> unital ;
correctness
coherence
C_Normed_Algebra_of_ContinuousFunctions X is unital ;
proof
reconsider e = One_ ((CContinuousFunctions X),(CAlgebra the carrier of X)) as Element of (C_Normed_Algebra_of_ContinuousFunctions X) ;
take e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (C_Normed_Algebra_of_ContinuousFunctions X) holds
( b1 * e = b1 & e * b1 = b1 )
thus for b1 being Element of the carrier of (C_Normed_Algebra_of_ContinuousFunctions X) holds
( b1 * e = b1 & e * b1 = b1 ) by Lm2; ::_thesis: verum
end;
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
let X be non empty compact TopSpace; ::_thesis: 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
let x1, x2 be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: 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
let y1, y2 be Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x1 = y1 & x2 = y2 implies x1 + x2 = y1 + y2 )
assume A1: ( x1 = y1 & x2 = y2 ) ; ::_thesis: x1 + x2 = y1 + y2
A2: CContinuousFunctions X is add-closed by CC0SP1:def_2;
A3: ComplexBoundedFunctions the carrier of X is add-closed by CC0SP1:def_2;
thus x1 + x2 = ( the addF of (CAlgebra the carrier of X) || (CContinuousFunctions X)) . [x1,x2] by A2, C0SP1:def_5
.= the addF of (CAlgebra the carrier of X) . [x1,x2] by FUNCT_1:49
.= ( the addF of (CAlgebra the carrier of X) || (ComplexBoundedFunctions the carrier of X)) . [y1,y2] by A1, FUNCT_1:49
.= y1 + y2 by A3, C0SP1:def_5 ; ::_thesis: verum
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
let X be non empty compact TopSpace; ::_thesis: 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
let a be Complex; ::_thesis: 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
let x be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y
let y be Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x = y implies a * x = a * y )
assume A1: x = y ; ::_thesis: a * x = a * y
reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def_2;
thus a * x = ( the Mult of (CAlgebra the carrier of X) | [:COMPLEX,(CContinuousFunctions X):]) . [a1,x] by CC0SP1:def_3
.= the Mult of (CAlgebra the carrier of X) . [a1,x] by FUNCT_1:49
.= ( the Mult of (CAlgebra the carrier of X) | [:COMPLEX,(ComplexBoundedFunctions the carrier of X):]) . [a1,y] by A1, FUNCT_1:49
.= a * y by CC0SP1:def_3 ; ::_thesis: verum
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
let X be non empty compact TopSpace; ::_thesis: 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
let x1, x2 be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: 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
let y1, y2 be Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x1 = y1 & x2 = y2 implies x1 * x2 = y1 * y2 )
assume A1: ( x1 = y1 & x2 = y2 ) ; ::_thesis: x1 * x2 = y1 * y2
thus x1 * x2 = ( the multF of (CAlgebra the carrier of X) || (CContinuousFunctions X)) . [x1,x2] by C0SP1:def_6
.= the multF of (CAlgebra the carrier of X) . [x1,x2] by FUNCT_1:49
.= ( the multF of (CAlgebra the carrier of X) || (ComplexBoundedFunctions the carrier of X)) . [y1,y2] by A1, FUNCT_1:49
.= y1 * y2 by C0SP1:def_6 ; ::_thesis: verum
end;
theorem Th17: :: CC0SP2:17
for X being non empty compact TopSpace holds C_Normed_Algebra_of_ContinuousFunctions X is ComplexAlgebra
proof
let X be non empty compact TopSpace; ::_thesis: C_Normed_Algebra_of_ContinuousFunctions X is ComplexAlgebra
1. (C_Normed_Algebra_of_ContinuousFunctions X) = 1_ (C_Algebra_of_ContinuousFunctions X) ;
hence C_Normed_Algebra_of_ContinuousFunctions X is ComplexAlgebra by CC0SP1:14; ::_thesis: verum
end;
registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> right_complementable Abelian add-associative right_zeroed associative commutative right-distributive right_unital 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;
end;
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
proof
let X be non empty compact TopSpace; ::_thesis: for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds (Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (1r,F) = F
let F be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: (Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (1r,F) = F
set X1 = CContinuousFunctions X;
reconsider f1 = F as Element of CContinuousFunctions X ;
A1: [1,f1] in [:COMPLEX,(CContinuousFunctions X):] by ZFMISC_1:87;
(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (1,F) = ( the Mult of (CAlgebra the carrier of X) | [:COMPLEX,(CContinuousFunctions X):]) . (1,f1) by CC0SP1:def_3
.= the Mult of (CAlgebra the carrier of X) . (1,f1) by A1, FUNCT_1:49
.= F by CFUNCDOM:12 ;
hence (Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (1r,F) = F ; ::_thesis: verum
end;
registration
let X be non empty compact TopSpace;
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
for v being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds 1r * v = v
proof
let v be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: 1r * v = v
reconsider v1 = v as Element of CContinuousFunctions X ;
A1: 1r * v = ( the Mult of (CAlgebra the carrier of X) | [:COMPLEX,(CContinuousFunctions X):]) . [1r,v1] by CC0SP1:def_3
.= the Mult of (CAlgebra the carrier of X) . (1r,v1) by FUNCT_1:49
.= v1 by CFUNCDOM:12 ;
thus 1r * v = v by A1; ::_thesis: verum
end;
hence ( 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 ) by CLVECT_1:def_5; ::_thesis: verum
end;
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
let X be non empty compact TopSpace; ::_thesis: X --> 0 = 0. (C_Normed_Algebra_of_ContinuousFunctions X)
X --> 0 = 0. (C_Algebra_of_ContinuousFunctions X) by Th13;
hence X --> 0 = 0. (C_Normed_Algebra_of_ContinuousFunctions X) ; ::_thesis: verum
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
let X be non empty compact TopSpace; ::_thesis: 0. (C_Normed_Algebra_of_ContinuousFunctions X) = 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X)
thus 0. (C_Normed_Algebra_of_ContinuousFunctions X) = X --> 0 by Th20
.= 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by CC0SP1:18 ; ::_thesis: verum
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
let X be non empty compact TopSpace; ::_thesis: 1. (C_Normed_Algebra_of_ContinuousFunctions X) = 1. (C_Normed_Algebra_of_BoundedFunctions the carrier of X)
thus 1. (C_Normed_Algebra_of_ContinuousFunctions X) = 1_ (C_Algebra_of_ContinuousFunctions X)
.= X --> 1r by Th14
.= 1_ (C_Algebra_of_BoundedFunctions the carrier of X) by CC0SP1:9
.= 1. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ; ::_thesis: verum
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.||
proof
let X be non empty compact TopSpace; ::_thesis: for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds 0 <= ||.F.||
let F be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: 0 <= ||.F.||
reconsider F1 = F as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
||.F.|| = ||.F1.|| by FUNCT_1:49;
hence 0 <= ||.F.|| by CC0SP1:20; ::_thesis: verum
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) )
proof
let X be non empty compact TopSpace; ::_thesis: 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) )
let f, g, h be Function of the carrier of X,COMPLEX; ::_thesis: 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) )
let F, G, H be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( f = F & g = G & h = H implies ( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) ) )
reconsider f1 = F, g1 = G, h1 = H as VECTOR of (C_Algebra_of_ContinuousFunctions X) ;
( H = F + G iff h1 = f1 + g1 ) ;
hence ( f = F & g = G & h = H implies ( H = F + G iff for x being Element of X holds h . x = (f . x) + (g . x) ) ) by Th10; ::_thesis: verum
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) )
proof
let a be Complex; ::_thesis: 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) )
let X be non empty compact TopSpace; ::_thesis: 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) )
let f, g be Function of the carrier of X,COMPLEX; ::_thesis: 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) )
let F, G be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( f = F & g = G implies ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) )
reconsider f1 = F, g1 = G as VECTOR of (C_Algebra_of_ContinuousFunctions X) ;
( G = a * F iff g1 = a * f1 ) ;
hence ( f = F & g = G implies ( G = a * F iff for x being Element of X holds g . x = a * (f . x) ) ) by Th11; ::_thesis: verum
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) )
proof
let X be non empty compact TopSpace; ::_thesis: 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) )
let f, g, h be Function of the carrier of X,COMPLEX; ::_thesis: 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) )
let F, G, H be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( f = F & g = G & h = H implies ( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) ) )
reconsider f1 = F, g1 = G, h1 = H as VECTOR of (C_Algebra_of_ContinuousFunctions X) ;
( H = F * G iff h1 = f1 * g1 ) ;
hence ( f = F & g = G & h = H implies ( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) ) ) by Th12; ::_thesis: verum
end;
theorem Th25: :: CC0SP2:25
for X being non empty compact TopSpace holds ||.(0. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = 0
proof
let X be non empty compact TopSpace; ::_thesis: ||.(0. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = 0
set F = 0. (C_Normed_Algebra_of_ContinuousFunctions X);
reconsider F1 = 0. (C_Normed_Algebra_of_ContinuousFunctions X) as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
( ||.F1.|| = 0 iff F1 = 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ) by CC0SP1:25;
hence ||.(0. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = 0 by Lm7, FUNCT_1:49; ::_thesis: verum
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)
proof
let X be non empty compact TopSpace; ::_thesis: for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st ||.F.|| = 0 holds
F = 0. (C_Normed_Algebra_of_ContinuousFunctions X)
let F be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_ContinuousFunctions X) )
reconsider F1 = F as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
( ||.F1.|| = 0 iff F1 = 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ) by CC0SP1:25;
hence ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_ContinuousFunctions X) ) by Lm7, FUNCT_1:49; ::_thesis: verum
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).|| = (abs a) * ||.F.||
proof
let a be Complex; ::_thesis: for X being non empty compact TopSpace
for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(a * F).|| = (abs a) * ||.F.||
let X be non empty compact TopSpace; ::_thesis: for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(a * F).|| = (abs a) * ||.F.||
let F be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ||.(a * F).|| = (abs a) * ||.F.||
reconsider F1 = F as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
thus ||.(a * F).|| = ||.(a * F1).|| by Lm5, Lm3
.= (abs a) * ||.F1.|| by CC0SP1:25
.= (abs a) * ||.F.|| by FUNCT_1:49 ; ::_thesis: verum
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.||
proof
let X be non empty compact TopSpace; ::_thesis: for F, G being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(F + G).|| <= ||.F.|| + ||.G.||
let F, G be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ||.(F + G).|| <= ||.F.|| + ||.G.||
reconsider F1 = F, G1 = G as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
A1: ||.F.|| = ||.F1.|| by FUNCT_1:49;
A2: ||.G.|| = ||.G1.|| by FUNCT_1:49;
A3: ||.(F + G).|| = ||.(F1 + G1).|| by Lm4, Lm3;
thus ||.(F + G).|| <= ||.F.|| + ||.G.|| by A1, A2, A3, CC0SP1:25; ::_thesis: verum
end;
registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> discerning reflexive ComplexNormSpace-like ;
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 )
proof
set C = C_Normed_Algebra_of_ContinuousFunctions X;
A1: ||.(0. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = 0 by Th25;
A2: for x, y being Point of (C_Normed_Algebra_of_ContinuousFunctions X)
for a being Complex holds
( ( ||.x.|| = 0 implies x = 0. (C_Normed_Algebra_of_ContinuousFunctions X) ) & ( x = 0. (C_Normed_Algebra_of_ContinuousFunctions X) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th25, Th26, Th27, Th28;
thus ( 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 A1, A2, CLVECT_1:def_13, NORMSP_0:def_5, NORMSP_0:def_6; ::_thesis: verum
end;
end;
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
let X be non empty compact TopSpace; ::_thesis: 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
let x1, x2 be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: 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
let y1, y2 be Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x1 = y1 & x2 = y2 implies x1 - x2 = y1 - y2 )
assume A1: ( x1 = y1 & x2 = y2 ) ; ::_thesis: x1 - x2 = y1 - y2
reconsider z2 = x2 as VECTOR of (C_Normed_Algebra_of_ContinuousFunctions X) ;
reconsider e = - 1r as Complex ;
- x2 = e * x2 by CLVECT_1:3
.= e * y2 by A1, Lm5
.= - y2 by CLVECT_1:3 ;
hence x1 - x2 = y1 - y2 by A1, Lm4; ::_thesis: verum
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) )
proof
let X be non empty compact TopSpace; ::_thesis: 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) )
let f, g, h be Function of the carrier of X,COMPLEX; ::_thesis: 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) )
let F, G, H be Point of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( f = F & g = G & h = H implies ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) ) )
assume A1: ( f = F & g = G & h = H ) ; ::_thesis: ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) )
A2: now__::_thesis:_(_H_=_F_-_G_implies_for_x_being_Element_of_X_holds_h_._x_=_(f_._x)_-_(g_._x)_)
assume H = F - G ; ::_thesis: for x being Element of X holds h . x = (f . x) - (g . x)
then H + G = F - (G - G) by RLVECT_1:29;
then H + G = F - (0. (C_Normed_Algebra_of_ContinuousFunctions X)) by RLVECT_1:15;
then A3: H + G = F by RLVECT_1:13;
now__::_thesis:_for_x_being_Element_of_X_holds_(f_._x)_-_(g_._x)_=_h_._x
let x be Element of X; ::_thesis: (f . x) - (g . x) = h . x
f . x = (h . x) + (g . x) by A1, A3, Th22;
hence (f . x) - (g . x) = h . x ; ::_thesis: verum
end;
hence for x being Element of X holds h . x = (f . x) - (g . x) ; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h_._x_=_(f_._x)_-_(g_._x)_)_implies_F_-_G_=_H_)
assume A4: for x being Element of X holds h . x = (f . x) - (g . x) ; ::_thesis: F - G = H
now__::_thesis:_for_x_being_Element_of_X_holds_(h_._x)_+_(g_._x)_=_f_._x
let x be Element of X; ::_thesis: (h . x) + (g . x) = f . x
h . x = (f . x) - (g . x) by A4;
hence (h . x) + (g . x) = f . x ; ::_thesis: verum
end;
then F = H + G by A1, Th22;
then F - G = H + (G - G) by RLVECT_1:def_3;
then F - G = H + (0. (C_Normed_Algebra_of_ContinuousFunctions X)) by RLVECT_1:15;
hence F - G = H by RLVECT_1:4; ::_thesis: verum
end;
hence ( H = F - G iff for x being Element of X holds h . x = (f . x) - (g . x) ) by A2; ::_thesis: verum
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 )
proof
let X be ComplexBanachSpace; ::_thesis: 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 )
let Y be Subset of X; ::_thesis: 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 )
let seq be sequence of X; ::_thesis: ( Y is closed & rng seq c= Y & seq is CCauchy implies ( seq is convergent & lim seq in Y ) )
assume A1: ( Y is closed & rng seq c= Y & seq is CCauchy ) ; ::_thesis: ( seq is convergent & lim seq in Y )
hence seq is convergent by CLOPBAN1:def_13; ::_thesis: lim seq in Y
hence lim seq in Y by A1, NCFCONT1:def_3; ::_thesis: verum
end;
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
proof
let X be non empty compact TopSpace; ::_thesis: for Y being Subset of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st Y = CContinuousFunctions X holds
Y is closed
let Y be Subset of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( Y = CContinuousFunctions X implies Y is closed )
assume A1: Y = CContinuousFunctions X ; ::_thesis: Y is closed
now__::_thesis:_for_seq_being_sequence_of_(C_Normed_Algebra_of_BoundedFunctions_the_carrier_of_X)_st_rng_seq_c=_Y_&_seq_is_convergent_holds_
lim_seq_in_Y
let seq be sequence of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( rng seq c= Y & seq is convergent implies lim seq in Y )
assume A2: ( rng seq c= Y & seq is convergent ) ; ::_thesis: lim seq in Y
lim seq in ComplexBoundedFunctions the carrier of X ;
then consider f being Function of the carrier of X,COMPLEX such that
A3: ( f = lim seq & f | the carrier of X is bounded ) ;
now__::_thesis:_for_z_being_set_st_z_in_ComplexBoundedFunctions_the_carrier_of_X_holds_
z_in_PFuncs_(_the_carrier_of_X,COMPLEX)
let z be set ; ::_thesis: ( z in ComplexBoundedFunctions the carrier of X implies z in PFuncs ( the carrier of X,COMPLEX) )
assume z in ComplexBoundedFunctions the carrier of X ; ::_thesis: z in PFuncs ( the carrier of X,COMPLEX)
then ex f being Function of the carrier of X,COMPLEX st
( f = z & f | the carrier of X is bounded ) ;
hence z in PFuncs ( the carrier of X,COMPLEX) by PARTFUN1:45; ::_thesis: verum
end;
then ComplexBoundedFunctions the carrier of X c= PFuncs ( the carrier of X,COMPLEX) by TARSKI:def_3;
then reconsider H = seq as Functional_Sequence of the carrier of X,COMPLEX by FUNCT_2:7;
A4: for p being Real st p > 0 holds
ex k being Element of NAT st
for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < p
proof
let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < p )
assume p > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < p
then consider k being Element of NAT such that
A5: for n being Element of NAT st n >= k holds
||.((seq . n) - (lim seq)).|| < p by A2, CLVECT_1:def_16;
take k ; ::_thesis: for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < p
hereby ::_thesis: verum
let n be Element of NAT ; ::_thesis: for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < p
let x be set ; ::_thesis: ( n >= k & x in the carrier of X implies abs (((H . n) . x) - (f . x)) < p )
assume A6: ( n >= k & x in the carrier of X ) ; ::_thesis: abs (((H . n) . x) - (f . x)) < p
then A7: ||.((seq . n) - (lim seq)).|| < p by A5;
(seq . n) - (lim seq) in ComplexBoundedFunctions the carrier of X ;
then consider g being Function of the carrier of X,COMPLEX such that
A8: ( g = (seq . n) - (lim seq) & g | the carrier of X is bounded ) ;
seq . n in ComplexBoundedFunctions the carrier of X ;
then consider s being Function of the carrier of X,COMPLEX such that
A9: ( s = seq . n & s | the carrier of X is bounded ) ;
reconsider x0 = x as Element of the carrier of X by A6;
A10: g . x0 = (s . x0) - (f . x0) by A8, A9, A3, CC0SP1:26;
abs (g . x0) <= ||.((seq . n) - (lim seq)).|| by A8, CC0SP1:19;
hence abs (((H . n) . x) - (f . x)) < p by A10, A9, A7, XXREAL_0:2; ::_thesis: verum
end;
end;
f is continuous
proof
set n = the Element of NAT ;
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
let x be Point of X; ::_thesis: 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 )
let V be Subset of COMPLEX; ::_thesis: ( f . x in V & V is open implies ex W being Subset of X st
( x in W & W is open & f .: W c= V ) )
assume A11: ( f . x in V & V is open ) ; ::_thesis: ex W being Subset of X st
( x in W & W is open & f .: W c= V )
reconsider z0 = f . x as Complex ;
consider N being Neighbourhood of z0 such that
A12: N c= V by A11, CFDIFF_1:9;
consider r being Real such that
A13: ( 0 < r & { p where p is Complex : |.(p - z0).| < r } c= N ) by CFDIFF_1:def_5;
set S = { p where p is Complex : |.(p - z0).| < r } ;
A14: ( r / 3 > 0 & r / 3 is Real ) by A13, XREAL_0:def_1;
consider k being Element of NAT such that
A15: for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < r / 3 by A4, A14;
k in NAT ;
then k in dom seq by NORMSP_1:12;
then H . k in rng seq by FUNCT_1:def_3;
then H . k in Y by A2;
then consider h being continuous Function of the carrier of X,COMPLEX such that
A16: H . k = h by A1;
set z1 = h . x;
set G1 = { p where p is Complex : |.(p - (h . x)).| < r / 3 } ;
{ p where p is Complex : |.(p - (h . x)).| < r / 3 } c= COMPLEX
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { p where p is Complex : |.(p - (h . x)).| < r / 3 } or z in COMPLEX )
assume z in { p where p is Complex : |.(p - (h . x)).| < r / 3 } ; ::_thesis: z in COMPLEX
then ex y being Complex st
( z = y & |.(y - (h . x)).| < r / 3 ) ;
hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
end;
then reconsider T1 = { p where p is Complex : |.(p - (h . x)).| < r / 3 } as Subset of COMPLEX ;
A17: T1 is open by A14, CFDIFF_1:13;
|.((h . x) - (h . x)).| = 0 ;
then h . x in { p where p is Complex : |.(p - (h . x)).| < r / 3 } by A13;
then consider W1 being Subset of X such that
A18: ( x in W1 & W1 is open & h .: W1 c= { p where p is Complex : |.(p - (h . x)).| < r / 3 } ) by A17, Th3;
now__::_thesis:_for_zz0_being_set_st_zz0_in_f_.:_W1_holds_
zz0_in__{__p_where_p_is_Complex_:_|.(p_-_z0).|_<_r__}_
let zz0 be set ; ::_thesis: ( zz0 in f .: W1 implies zz0 in { p where p is Complex : |.(p - z0).| < r } )
assume zz0 in f .: W1 ; ::_thesis: zz0 in { p where p is Complex : |.(p - z0).| < r }
then consider xx0 being set such that
A19: ( xx0 in dom f & xx0 in W1 & f . xx0 = zz0 ) by FUNCT_1:def_6;
h . xx0 in h .: W1 by A19, FUNCT_2:35;
then h . xx0 in { p where p is Complex : |.(p - (h . x)).| < r / 3 } by A18;
then consider hx0 being Complex such that
A20: ( hx0 = h . xx0 & |.(hx0 - (h . x)).| < r / 3 ) ;
|.((h . xx0) - (f . xx0)).| < r / 3 by A19, A15, A16;
then |.(- ((h . xx0) - (f . xx0))).| < r / 3 by COMPLEX1:52;
then A21: |.((f . xx0) - (h . xx0)).| < r / 3 ;
A22: |.((h . x) - (f . x)).| < r / 3 by A15, A16;
|.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).| < (r / 3) + (r / 3) by A20, A21, XREAL_1:8;
then (|.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).|) + |.((h . x) - (f . x)).| < ((r / 3) + (r / 3)) + (r / 3) by A22, XREAL_1:8;
then A23: (|.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).|) + |.((h . x) - (f . x)).| < r ;
|.((f . xx0) - (f . x)).| = |.((((f . xx0) - (h . xx0)) + ((h . xx0) - (h . x))) + ((h . x) - (f . x))).| ;
then A24: |.((f . xx0) - (f . x)).| <= |.(((f . xx0) - (h . xx0)) + ((h . xx0) - (h . x))).| + |.((h . x) - (f . x)).| by COMPLEX1:56;
|.(((f . xx0) - (h . xx0)) + ((h . xx0) - (h . x))).| <= |.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).| by COMPLEX1:56;
then |.(((f . xx0) - (h . xx0)) + ((h . xx0) - (h . x))).| + |.((h . x) - (f . x)).| <= (|.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).|) + |.((h . x) - (f . x)).| by XREAL_1:6;
then |.((f . xx0) - (f . x)).| <= (|.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).|) + |.((h . x) - (f . x)).| by A24, XXREAL_0:2;
then |.((f . xx0) - (f . x)).| < r by A23, XXREAL_0:2;
hence zz0 in { p where p is Complex : |.(p - z0).| < r } by A19; ::_thesis: verum
end;
then f .: W1 c= { p where p is Complex : |.(p - z0).| < r } by TARSKI:def_3;
then f .: W1 c= N by A13, XBOOLE_1:1;
hence ex W being Subset of X st
( x in W & W is open & f .: W c= V ) by A18, A12, XBOOLE_1:1; ::_thesis: verum
end;
hence f is continuous by Th3; ::_thesis: verum
end;
hence lim seq in Y by A3, A1; ::_thesis: verum
end;
hence Y is closed by NCFCONT1:def_3; ::_thesis: verum
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
proof
let X be non empty compact TopSpace; ::_thesis: for seq being sequence of (C_Normed_Algebra_of_ContinuousFunctions X) st seq is CCauchy holds
seq is convergent
let vseq be sequence of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ( vseq is CCauchy implies vseq is convergent )
assume A1: vseq is CCauchy ; ::_thesis: vseq is convergent
A2: for x being set st x in CContinuousFunctions X holds
x in ComplexBoundedFunctions the carrier of X by Lm1;
then CContinuousFunctions X c= ComplexBoundedFunctions the carrier of X by TARSKI:def_3;
then rng vseq c= ComplexBoundedFunctions the carrier of X by XBOOLE_1:1;
then reconsider vseq1 = vseq as sequence of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by FUNCT_2:6;
now__::_thesis:_for_e_being_Real_st_e_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((vseq1_._n)_-_(vseq1_._m)).||_<_e
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e )
assume A3: e > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e
consider k being Element of NAT such that
A4: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A3, CSSPACE3:8;
take k = k; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((vseq1_._n)_-_(vseq1_._m)).||_<_e
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((vseq1 . n) - (vseq1 . m)).|| < e )
assume ( n >= k & m >= k ) ; ::_thesis: ||.((vseq1 . n) - (vseq1 . m)).|| < e
then ||.((vseq . n) - (vseq . m)).|| < e by A4;
hence ||.((vseq1 . n) - (vseq1 . m)).|| < e by Lm9, Lm3; ::_thesis: verum
end;
hence for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e ; ::_thesis: verum
end;
then A5: vseq1 is CCauchy by CSSPACE3:8;
then A6: vseq1 is convergent by CC0SP1:27;
reconsider Y = CContinuousFunctions X as Subset of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by A2, TARSKI:def_3;
A7: rng vseq c= CContinuousFunctions X ;
Y is closed by Th31;
then reconsider tv = lim vseq1 as Point of (C_Normed_Algebra_of_ContinuousFunctions X) by A7, A5, Th30;
for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| < e
proof
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| < e )
assume e > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| < e
then consider k being Element of NAT such that
A8: for n being Element of NAT st n >= k holds
||.((vseq1 . n) - (lim vseq1)).|| < e by A6, CLVECT_1:def_16;
take k ; ::_thesis: for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| < e
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_
||.((vseq_._n)_-_tv).||_<_e
let n be Element of NAT ; ::_thesis: ( n >= k implies ||.((vseq . n) - tv).|| < e )
assume n >= k ; ::_thesis: ||.((vseq . n) - tv).|| < e
then ||.((vseq1 . n) - (lim vseq1)).|| < e by A8;
hence ||.((vseq . n) - tv).|| < e by Lm9, Lm3; ::_thesis: verum
end;
hence for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| < e ; ::_thesis: verum
end;
hence vseq is convergent by CLVECT_1:def_15; ::_thesis: verum
end;
registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> complete ;
coherence
C_Normed_Algebra_of_ContinuousFunctions X is complete
proof
for seq being sequence of (C_Normed_Algebra_of_ContinuousFunctions X) st seq is CCauchy holds
seq is convergent by Th32;
hence C_Normed_Algebra_of_ContinuousFunctions X is complete by CLOPBAN1:def_13; ::_thesis: verum
end;
end;
registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> Banach_Algebra-like ;
coherence
C_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like
proof
set B = C_Normed_Algebra_of_ContinuousFunctions X;
A1: now__::_thesis:_for_f,_g_being_Element_of_(C_Normed_Algebra_of_ContinuousFunctions_X)_holds_||.(f_*_g).||_<=_||.f.||_*_||.g.||
let f, g be Element of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: ||.(f * g).|| <= ||.f.|| * ||.g.||
reconsider f1 = f, g1 = g as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
A2: ( ||.f.|| = ||.f1.|| & ||.g.|| = ||.g1.|| & ||.(f * g).|| = ||.(f1 * g1).|| ) by Lm6, Lm3;
C_Normed_Algebra_of_BoundedFunctions the carrier of X is Banach_Algebra-like_1 by CC0SP1:28;
hence ||.(f * g).|| <= ||.f.|| * ||.g.|| by A2, CLOPBAN2:def_9; ::_thesis: verum
end;
A3: C_Normed_Algebra_of_BoundedFunctions the carrier of X is Banach_Algebra-like_2 by CC0SP1:28;
A4: ||.(1. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = ||.(1. (C_Normed_Algebra_of_BoundedFunctions the carrier of X)).|| by Lm8, Lm3
.= 1 by A3, CLOPBAN2:def_10 ;
A5: now__::_thesis:_for_a_being_Complex
for_f,_g_being_Element_of_(C_Normed_Algebra_of_ContinuousFunctions_X)_holds_a_*_(f_*_g)_=_f_*_(a_*_g)
let a be Complex; ::_thesis: for f, g being Element of (C_Normed_Algebra_of_ContinuousFunctions X) holds a * (f * g) = f * (a * g)
let f, g be Element of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: a * (f * g) = f * (a * g)
reconsider f1 = f, g1 = g as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
A6: a * g1 = a * g by Lm5;
A7: f * g = f1 * g1 by Lm6;
A8: C_Normed_Algebra_of_BoundedFunctions the carrier of X is Banach_Algebra-like_3 by CC0SP1:28;
a * (f * g) = a * (f1 * g1) by A7, Lm5;
then a * (f * g) = f1 * (a * g1) by A8, CLOPBAN2:def_11;
hence a * (f * g) = f * (a * g) by A6, Lm6; ::_thesis: verum
end;
now__::_thesis:_for_f,_g,_h_being_Element_of_(C_Normed_Algebra_of_ContinuousFunctions_X)_holds_(g_+_h)_*_f_=_(g_*_f)_+_(h_*_f)
let f, g, h be Element of (C_Normed_Algebra_of_ContinuousFunctions X); ::_thesis: (g + h) * f = (g * f) + (h * f)
reconsider f1 = f, g1 = g, h1 = h as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
A9: g + h = g1 + h1 by Lm4;
A10: ( g * f = g1 * f1 & h * f = h1 * f1 ) by Lm6;
A11: C_Normed_Algebra_of_BoundedFunctions the carrier of X is left-distributive by CC0SP1:28;
thus (g + h) * f = (g1 + h1) * f1 by Lm6, A9
.= (g1 * f1) + (h1 * f1) by A11, VECTSP_1:def_3
.= (g * f) + (h * f) by Lm4, A10 ; ::_thesis: verum
end;
then C_Normed_Algebra_of_ContinuousFunctions X is left-distributive left_unital complete Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Normed_Complex_Algebra by A1, A4, A5, CLOPBAN2:def_9, CLOPBAN2:def_10, CLOPBAN2:def_11, VECTSP_1:def_3;
hence C_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like ; ::_thesis: verum
end;
end;
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)
proof
let X be non empty TopSpace; ::_thesis: for f, g being Function of the carrier of X,COMPLEX holds support (f + g) c= (support f) \/ (support g)
let f, g be Function of the carrier of X,COMPLEX; ::_thesis: support (f + g) c= (support f) \/ (support g)
set CX = the carrier of X;
set h = f + g;
A1: rng (f + g) c= COMPLEX by MEMBERED:1;
dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1
.= the carrier of X /\ (dom g) by PARTFUN1:def_2
.= the carrier of X /\ the carrier of X by PARTFUN1:def_2 ;
then reconsider h = f + g as Function of the carrier of X,COMPLEX by A1, FUNCT_2:2;
( dom f = the carrier of X & dom g = the carrier of X & dom h = the carrier of X ) by FUNCT_2:def_1;
then A2: ( support f c= the carrier of X & support g c= the carrier of X & support h c= the carrier of X ) by PRE_POLY:37;
now__::_thesis:_for_x_being_set_st_x_in_(_the_carrier_of_X_\_(support_f))_/\_(_the_carrier_of_X_\_(support_g))_holds_
x_in_the_carrier_of_X_\_(support_(f_+_g))
let x be set ; ::_thesis: ( x in ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) implies x in the carrier of X \ (support (f + g)) )
assume x in ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) ; ::_thesis: x in the carrier of X \ (support (f + g))
then ( x in the carrier of X \ (support f) & x in the carrier of X \ (support g) ) by XBOOLE_0:def_4;
then ( x in the carrier of X & not x in support f & x in the carrier of X & not x in support g ) by XBOOLE_0:def_5;
then A3: ( x in the carrier of X & f . x = 0 & g . x = 0 ) by PRE_POLY:def_7;
then (f + g) . x = (f . x) + (g . x) by VALUED_1:1
.= 0 by A3 ;
then A4: ( x in the carrier of X & (f + g) . x = 0 ) by A3;
not x in support (f + g) by A4, PRE_POLY:def_7;
hence x in the carrier of X \ (support (f + g)) by A4, XBOOLE_0:def_5; ::_thesis: verum
end;
then ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) c= the carrier of X \ (support (f + g)) by TARSKI:def_3;
then the carrier of X \ ((support f) \/ (support g)) c= the carrier of X \ (support (f + g)) by XBOOLE_1:53;
then the carrier of X \ ( the carrier of X \ (support (f + g))) c= the carrier of X \ ( the carrier of X \ ((support f) \/ (support g))) by XBOOLE_1:34;
then the carrier of X /\ (support (f + g)) c= the carrier of X \ ( the carrier of X \ ((support f) \/ (support g))) by XBOOLE_1:48;
then the carrier of X /\ (support (f + g)) c= the carrier of X /\ ((support f) \/ (support g)) by XBOOLE_1:48;
then support (f + g) c= the carrier of X /\ ((support f) \/ (support g)) by A2, XBOOLE_1:28;
then support (f + g) c= ( the carrier of X /\ (support f)) \/ ( the carrier of X /\ (support g)) by XBOOLE_1:23;
then support (f + g) c= (support f) \/ ( the carrier of X /\ (support g)) by A2, XBOOLE_1:28;
hence support (f + g) c= (support f) \/ (support g) by A2, XBOOLE_1:28; ::_thesis: verum
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
proof
let X be non empty TopSpace; ::_thesis: for a being Complex
for f being Function of the carrier of X,COMPLEX holds support (a (#) f) c= support f
let a be Complex; ::_thesis: for f being Function of the carrier of X,COMPLEX holds support (a (#) f) c= support f
let f be Function of the carrier of X,COMPLEX; ::_thesis: support (a (#) f) c= support f
set CX = the carrier of X;
reconsider h = a (#) f as Function of the carrier of X,COMPLEX ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (a (#) f) or x in support f )
assume x in support (a (#) f) ; ::_thesis: x in support f
then (a (#) f) . x <> 0 by PRE_POLY:def_7;
then a * (f . x) <> 0 by VALUED_1:6;
then f . x <> 0 ;
hence x in support f by PRE_POLY:def_7; ::_thesis: verum
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)
proof
let X be non empty TopSpace; ::_thesis: for f, g being Function of the carrier of X,COMPLEX holds support (f (#) g) c= (support f) \/ (support g)
let f, g be Function of the carrier of X,COMPLEX; ::_thesis: support (f (#) g) c= (support f) \/ (support g)
set CX = the carrier of X;
reconsider h = f (#) g as Function of the carrier of X,COMPLEX ;
( dom f = the carrier of X & dom g = the carrier of X & dom h = the carrier of X ) by FUNCT_2:def_1;
then A1: ( support f c= the carrier of X & support g c= the carrier of X & support h c= the carrier of X ) by PRE_POLY:37;
now__::_thesis:_for_x_being_set_st_x_in_(_the_carrier_of_X_\_(support_f))_/\_(_the_carrier_of_X_\_(support_g))_holds_
x_in_the_carrier_of_X_\_(support_(f_(#)_g))
let x be set ; ::_thesis: ( x in ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) implies x in the carrier of X \ (support (f (#) g)) )
assume x in ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) ; ::_thesis: x in the carrier of X \ (support (f (#) g))
then ( x in the carrier of X \ (support f) & x in the carrier of X \ (support g) ) by XBOOLE_0:def_4;
then ( x in the carrier of X & not x in support f & x in the carrier of X & not x in support g ) by XBOOLE_0:def_5;
then A2: ( x in the carrier of X & f . x = 0 & g . x = 0 ) by PRE_POLY:def_7;
(f (#) g) . x = 0 * 0 by A2, VALUED_1:5;
then A3: ( x in the carrier of X & (f (#) g) . x = 0 ) by A2;
not x in support (f (#) g) by A3, PRE_POLY:def_7;
hence x in the carrier of X \ (support (f (#) g)) by A3, XBOOLE_0:def_5; ::_thesis: verum
end;
then ( the carrier of X \ (support f)) /\ ( the carrier of X \ (support g)) c= the carrier of X \ (support (f (#) g)) by TARSKI:def_3;
then the carrier of X \ ((support f) \/ (support g)) c= the carrier of X \ (support (f (#) g)) by XBOOLE_1:53;
then the carrier of X \ ( the carrier of X \ (support (f (#) g))) c= the carrier of X \ ( the carrier of X \ ((support f) \/ (support g))) by XBOOLE_1:34;
then the carrier of X /\ (support (f (#) g)) c= the carrier of X \ ( the carrier of X \ ((support f) \/ (support g))) by XBOOLE_1:48;
then the carrier of X /\ (support (f (#) g)) c= the carrier of X /\ ((support f) \/ (support g)) by XBOOLE_1:48;
then support (f (#) g) c= the carrier of X /\ ((support f) \/ (support g)) by A1, XBOOLE_1:28;
then support (f (#) g) c= ( the carrier of X /\ (support f)) \/ ( the carrier of X /\ (support g)) by XBOOLE_1:23;
then support (f (#) g) c= (support f) \/ ( the carrier of X /\ (support g)) by A1, XBOOLE_1:28;
hence support (f (#) g) c= (support f) \/ (support g) by A1, XBOOLE_1:28; ::_thesis: verum
end;
definition
let X be non empty TopSpace;
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
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
A1: { 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 ) ) ) } c= Funcs ( the carrier of X,COMPLEX)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { 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 ) ) ) } or x in Funcs ( the carrier of X,COMPLEX) )
assume x in { 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 ) ) ) } ; ::_thesis: x in Funcs ( the carrier of X,COMPLEX)
then ex f being Function of the carrier of X,COMPLEX st
( x = f & 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 ) ) ) ;
hence x in Funcs ( the carrier of X,COMPLEX) by FUNCT_2:8; ::_thesis: verum
end;
not { 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 empty
proof
set g = the carrier of X --> 0c;
reconsider g = the carrier of X --> 0c as Function of the carrier of X,COMPLEX ;
A2: g is continuous
proof
for P being Subset of COMPLEX st P is closed holds
g " P is closed
proof
let P be Subset of COMPLEX; ::_thesis: ( P is closed implies g " P is closed )
assume P is closed ; ::_thesis: g " P is closed
set F = the carrier of X --> 0;
set H = the carrier of X;
set HX = [#] X;
percases ( 0 in P or not 0 in P ) ;
suppose 0 in P ; ::_thesis: g " P is closed
then g " P = [#] X by FUNCOP_1:14;
hence g " P is closed ; ::_thesis: verum
end;
suppose not 0 in P ; ::_thesis: g " P is closed
then ( the carrier of X --> 0) " P = {} X by FUNCOP_1:16;
hence g " P is closed ; ::_thesis: verum
end;
end;
end;
hence g is continuous by Def1; ::_thesis: verum
end;
A3: ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support g holds
Cl A is Subset of Y ) )
proof
set S = the non empty compact Subset of X;
for A being Subset of X st A = support g holds
Cl A is Subset of the non empty compact Subset of X
proof
let A be Subset of X; ::_thesis: ( A = support g implies Cl A is Subset of the non empty compact Subset of X )
assume A4: A = support g ; ::_thesis: Cl A is Subset of the non empty compact Subset of X
A5: A = {}
proof
assume A6: not A = {} ; ::_thesis: contradiction
set p = the Element of support g;
A7: the Element of support g in A by A6, A4;
then g . the Element of support g <> 0 by A4, PRE_POLY:def_7;
hence contradiction by A7, FUNCOP_1:7; ::_thesis: verum
end;
Cl ({} X) = {} by PRE_TOPC:22;
hence Cl A is Subset of the non empty compact Subset of X by A5, XBOOLE_1:2; ::_thesis: verum
end;
hence ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support g holds
Cl A is Subset of Y ) ) ; ::_thesis: verum
end;
g in { 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 ) ) ) } by A2, A3;
hence not { 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 empty ; ::_thesis: verum
end;
hence { 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) by A1; ::_thesis: verum
end;
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 ) ) ) } ;
theorem :: CC0SP2:36
for X being non empty TopSpace holds CC_0_Functions X is non empty Subset of (CAlgebra the carrier of X) ;
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
let X be non empty TopSpace; ::_thesis: 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
set W = CC_0_Functions X;
set V = CAlgebra the carrier of X;
let u, v be Element of (CAlgebra the carrier of X); ::_thesis: ( u in CC_0_Functions X & v in CC_0_Functions X implies u + v in CC_0_Functions X )
assume A1: ( u in CC_0_Functions X & v in CC_0_Functions X ) ; ::_thesis: u + v in CC_0_Functions X
consider u1 being Function of the carrier of X,COMPLEX such that
A2: ( u1 = u & u1 is continuous & ex Y1 being non empty Subset of X st
( Y1 is compact & ( for A1 being Subset of X st A1 = support u1 holds
Cl A1 is Subset of Y1 ) ) ) by A1;
consider Y1 being non empty Subset of X such that
A3: ( Y1 is compact & ( for A1 being Subset of X st A1 = support u1 holds
Cl A1 is Subset of Y1 ) ) by A2;
consider v1 being Function of the carrier of X,COMPLEX such that
A4: ( v1 = v & v1 is continuous & ex Y2 being non empty Subset of X st
( Y2 is compact & ( for A2 being Subset of X st A2 = support v1 holds
Cl A2 is Subset of Y2 ) ) ) by A1;
consider Y2 being non empty Subset of X such that
A5: ( Y2 is compact & ( for A2 being Subset of X st A2 = support v1 holds
Cl A2 is Subset of Y2 ) ) by A4;
A6: u in CContinuousFunctions X by A2;
A7: v in CContinuousFunctions X by A4;
CContinuousFunctions X is add-closed by CC0SP1:def_2;
then v + u in CContinuousFunctions X by A6, A7, IDEAL_1:def_1;
then consider fvu being continuous Function of the carrier of X,COMPLEX such that
A8: v + u = fvu ;
A9: Y1 \/ Y2 is compact by A3, A5, COMPTS_1:10;
( dom u1 = the carrier of X & dom v1 = the carrier of X ) by FUNCT_2:def_1;
then A10: ( support u1 c= the carrier of X & support v1 c= the carrier of X ) by PRE_POLY:37;
then reconsider A1 = support u1, A2 = support v1 as Subset of X ;
A11: (dom v1) /\ (dom u1) = the carrier of X /\ (dom u1) by FUNCT_2:def_1
.= the carrier of X /\ the carrier of X by FUNCT_2:def_1
.= the carrier of X ;
dom (v1 + u1) = (dom v1) /\ (dom u1) by VALUED_1:def_1;
then A12: support (v1 + u1) c= the carrier of X by A11, PRE_POLY:37;
reconsider A1 = support u1, A2 = support v1 as Subset of X by A10;
reconsider A3 = support (v1 + u1) as Subset of X by A12;
A13: Cl A3 c= Cl (A2 \/ A1) by Th33, PRE_TOPC:19;
A14: Cl A3 c= (Cl A2) \/ (Cl A1) by A13, PRE_TOPC:20;
Cl A1 is Subset of Y1 by A3;
then A15: Cl A1 c= Y1 ;
Cl A2 is Subset of Y2 by A5;
then (Cl A2) \/ (Cl A1) c= Y2 \/ Y1 by A15, XBOOLE_1:13;
then A16: for A3 being Subset of X st A3 = support (v1 + u1) holds
Cl A3 is Subset of (Y2 \/ Y1) by A14, XBOOLE_1:1;
reconsider vv1 = v as Element of Funcs ( the carrier of X,COMPLEX) ;
reconsider uu1 = u as Element of Funcs ( the carrier of X,COMPLEX) ;
reconsider fvu1 = v + u as Element of Funcs ( the carrier of X,COMPLEX) ;
A17: for x being Element of the carrier of X holds fvu1 . x = (vv1 . x) + (uu1 . x) by CFUNCDOM:1;
A18: dom fvu1 = the carrier of X by FUNCT_2:def_1;
for c being set st c in dom fvu1 holds
fvu1 . c = (v1 . c) + (u1 . c) by A17, A2, A4;
then fvu1 = v1 + u1 by A18, A11, VALUED_1:def_1;
hence u + v in CC_0_Functions X by A8, A9, A16; ::_thesis: verum
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
let X be non empty TopSpace; ::_thesis: 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
set W = CC_0_Functions X;
set V = CAlgebra the carrier of X;
let a be Complex; ::_thesis: 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
let u be Element of (CAlgebra the carrier of X); ::_thesis: ( u in CC_0_Functions X implies a * u in CC_0_Functions X )
assume A1: u in CC_0_Functions X ; ::_thesis: a * u in CC_0_Functions X
consider u1 being Function of the carrier of X,COMPLEX such that
A2: ( u1 = u & u1 is continuous & ex Y1 being non empty Subset of X st
( Y1 is compact & ( for A1 being Subset of X st A1 = support u1 holds
Cl A1 is Subset of Y1 ) ) ) by A1;
consider Y1 being non empty Subset of X such that
A3: ( Y1 is compact & ( for A1 being Subset of X st A1 = support u1 holds
Cl A1 is Subset of Y1 ) ) by A2;
A4: u in CContinuousFunctions X by A2;
a * u in CContinuousFunctions X by A4, CC0SP1:def_2;
then consider fau being continuous Function of the carrier of X,COMPLEX such that
A5: a * u = fau ;
dom u1 = the carrier of X by FUNCT_2:def_1;
then A6: support u1 c= the carrier of X by PRE_POLY:37;
then reconsider A1 = support u1 as Subset of X ;
A7: dom u1 = the carrier of X by FUNCT_2:def_1;
dom (a (#) u1) = dom u1 by VALUED_1:def_5;
then A8: support (a (#) u1) c= the carrier of X by A7, PRE_POLY:37;
reconsider A1 = support u1 as Subset of X by A6;
reconsider A3 = support (a (#) u1) as Subset of X by A8;
Cl A1 is Subset of Y1 by A3;
then A9: Cl A1 c= Y1 ;
Cl A3 c= Cl A1 by Th34, PRE_TOPC:19;
then A10: for A3 being Subset of X st A3 = support (a (#) u1) holds
Cl A3 is Subset of Y1 by A9, XBOOLE_1:1;
reconsider uu1 = u as Element of Funcs ( the carrier of X,COMPLEX) ;
reconsider fau1 = a * u as Element of Funcs ( the carrier of X,COMPLEX) ;
a in COMPLEX by XCMPLX_0:def_2;
then A11: for x being Element of the carrier of X holds fau1 . x = a * (uu1 . x) by CFUNCDOM:4;
A12: dom fau1 = the carrier of X by FUNCT_2:def_1;
A13: dom u1 = the carrier of X by FUNCT_2:def_1;
for c being set st c in dom fau1 holds
fau1 . c = a * (u1 . c) by A2, A11;
then fau1 = a (#) u1 by A12, A13, VALUED_1:def_5;
hence a * u in CC_0_Functions X by A5, A3, A10; ::_thesis: verum
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
let X be non empty TopSpace; ::_thesis: for u being Element of (CAlgebra the carrier of X) st u in CC_0_Functions X holds
- u in CC_0_Functions X
set W = CC_0_Functions X;
set V = CAlgebra the carrier of X;
let u be Element of (CAlgebra the carrier of X); ::_thesis: ( u in CC_0_Functions X implies - u in CC_0_Functions X )
assume A1: u in CC_0_Functions X ; ::_thesis: - u in CC_0_Functions X
set a = - 1r;
- u = (- 1r) * u by CLVECT_1:3;
hence - u in CC_0_Functions X by A1, Lm11; ::_thesis: verum
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
proof
let X be non empty TopSpace; ::_thesis: for W being non empty Subset of (CAlgebra the carrier of X) st W = CC_0_Functions X holds
W is Cadditively-linearly-closed
let W be non empty Subset of (CAlgebra the carrier of X); ::_thesis: ( W = CC_0_Functions X implies W is Cadditively-linearly-closed )
assume A1: W = CC_0_Functions X ; ::_thesis: W is Cadditively-linearly-closed
set V = CAlgebra the carrier of X;
for v, u being Element of (CAlgebra the carrier of X) st v in W & u in W holds
v + u in W by A1, Lm10;
then A2: W is add-closed by IDEAL_1:def_1;
for v being Element of (CAlgebra the carrier of X) st v in W holds
- v in W by A1, Lm12;
then A3: W is having-inverse by C0SP1:def_1;
for a being Complex
for u being Element of (CAlgebra the carrier of X) st u in W holds
a * u in W by A1, Lm11;
hence W is Cadditively-linearly-closed by A2, A3, CC0SP1:def_2; ::_thesis: verum
end;
theorem Th38: :: CC0SP2:38
for X being non empty TopSpace holds CC_0_Functions X is add-closed
proof
let X be non empty TopSpace; ::_thesis: CC_0_Functions X is add-closed
set Y = CC_0_Functions X;
set V = ComplexVectSpace the carrier of X;
for v, u being VECTOR of (ComplexVectSpace 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
let v, u be VECTOR of (ComplexVectSpace the carrier of X); ::_thesis: ( v in CC_0_Functions X & u in CC_0_Functions X implies v + u in CC_0_Functions X )
assume A1: ( v in CC_0_Functions X & u in CC_0_Functions X ) ; ::_thesis: v + u in CC_0_Functions X
reconsider v2 = v, u2 = u as VECTOR of (CAlgebra the carrier of X) ;
v2 + u2 in CC_0_Functions X by A1, Lm10;
hence v + u in CC_0_Functions X ; ::_thesis: verum
end;
hence CC_0_Functions X is add-closed by IDEAL_1:def_1; ::_thesis: verum
end;
theorem Th39: :: CC0SP2:39
for X being non empty TopSpace holds CC_0_Functions X is linearly-closed
proof
let X be non empty TopSpace; ::_thesis: CC_0_Functions X is linearly-closed
set Y = CC_0_Functions X;
set V = ComplexVectSpace the carrier of X;
A1: for v, u being VECTOR of (ComplexVectSpace 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
let v, u be VECTOR of (ComplexVectSpace the carrier of X); ::_thesis: ( v in CC_0_Functions X & u in CC_0_Functions X implies v + u in CC_0_Functions X )
assume A2: ( v in CC_0_Functions X & u in CC_0_Functions X ) ; ::_thesis: v + u in CC_0_Functions X
reconsider v1 = v, u1 = u as Element of Funcs ( the carrier of X,COMPLEX) ;
reconsider v2 = v, u2 = u as VECTOR of (CAlgebra the carrier of X) ;
v2 + u2 in CC_0_Functions X by A2, Lm10;
hence v + u in CC_0_Functions X ; ::_thesis: verum
end;
A3: for a being Complex
for v being Element of (ComplexVectSpace the carrier of X) st v in CC_0_Functions X holds
a * v in CC_0_Functions X
proof
let a be Complex; ::_thesis: for v being Element of (ComplexVectSpace the carrier of X) st v in CC_0_Functions X holds
a * v in CC_0_Functions X
let v be VECTOR of (ComplexVectSpace the carrier of X); ::_thesis: ( v in CC_0_Functions X implies a * v in CC_0_Functions X )
assume A4: v in CC_0_Functions X ; ::_thesis: a * v in CC_0_Functions X
reconsider v1 = v as Element of Funcs ( the carrier of X,COMPLEX) ;
reconsider v2 = v as VECTOR of (CAlgebra the carrier of X) ;
a * v2 in CC_0_Functions X by A4, Lm11;
hence a * v in CC_0_Functions X ; ::_thesis: verum
end;
thus CC_0_Functions X is linearly-closed by A1, A3, CLVECT_1:def_7; ::_thesis: verum
end;
registration
let X be non empty TopSpace;
cluster CC_0_Functions X -> non empty linearly-closed ;
correctness
coherence
( not CC_0_Functions X is empty & CC_0_Functions X is linearly-closed );
by Th39;
end;
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
proof
let V be ComplexLinearSpace; ::_thesis: 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
let V1 be Subset of V; ::_thesis: ( V1 is linearly-closed & not V1 is empty implies CLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V )
assume that
A1: V1 is linearly-closed and
A2: not V1 is empty ; ::_thesis: CLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V
for v, u being VECTOR of V st v in V1 & u in V1 holds
v + u in V1 by A1, CLVECT_1:def_7;
then V1 is add-closed by IDEAL_1:def_1;
then A3: Add_ (V1,V) = the addF of V || V1 by A2, C0SP1:def_5;
A4: Mult_ (V1,V) = the Mult of V | [:COMPLEX,V1:] by A1, CSSPACE:def_9;
Zero_ (V1,V) = 0. V by A1, A2, CSSPACE:def_10;
hence CLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V by A2, A3, A4, CLVECT_1:43; ::_thesis: verum
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;
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
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;
:: 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 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
proof
let X be non empty TopSpace; ::_thesis: for x being set st x in CC_0_Functions X holds
x in ComplexBoundedFunctions the carrier of X
let x be set ; ::_thesis: ( x in CC_0_Functions X implies x in ComplexBoundedFunctions the carrier of X )
assume A1: x in CC_0_Functions X ; ::_thesis: x in ComplexBoundedFunctions the carrier of X
consider f being Function of the carrier of X,COMPLEX such that
A2: ( f = 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 ) ) ) by A1;
consider Y being non empty Subset of X such that
A3: ( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) by A2;
dom f = the carrier of X by FUNCT_2:def_1;
then reconsider A = support f as Subset of X by PRE_POLY:37;
( |.f.| is Function of the carrier of X,REAL & |.f.| is continuous ) by Th8, A2;
then consider f1 being Function of the carrier of X,REAL such that
A4: ( f1 = |.f.| & f1 is continuous ) ;
f1 .: Y is compact by A4, A3, JORDAN_A:1;
then reconsider Y1 = f1 .: Y as non empty real-bounded Subset of REAL by RCOMP_1:10;
A5: Y1 c= [.(inf Y1),(sup Y1).] by XXREAL_2:69;
reconsider r1 = inf Y1 as real number ;
reconsider r2 = sup Y1 as real number ;
consider r being real number such that
A6: r = ((abs r1) + (abs r2)) + 1 ;
for p being Element of Y holds
( r > 0 & - r < f1 . p & f1 . p < r )
proof
let p be Element of Y; ::_thesis: ( r > 0 & - r < f1 . p & f1 . p < r )
f1 . p in Y1 by FUNCT_2:35;
then f1 . p in [.r1,r2.] by A5;
then f1 . p in { t where t is Real : ( r1 <= t & t <= r2 ) } by RCOMP_1:def_1;
then consider r3 being Element of REAL such that
A7: ( r3 = f1 . p & r1 <= r3 & r3 <= r2 ) ;
- (abs r1) <= r1 by ABSVALUE:4;
then (- (abs r1)) - (abs r2) <= r1 - 0 by XREAL_1:13;
then ((- (abs r1)) - (abs r2)) - 1 < r1 - 0 by XREAL_1:15;
then A8: - r < r1 by A6;
r2 <= abs r2 by ABSVALUE:4;
then r2 + 0 <= (abs r2) + (abs r1) by XREAL_1:7;
then A9: r2 < r by A6, XREAL_1:8;
- r < f1 . p by A7, A8, XXREAL_0:2;
hence ( r > 0 & - r < f1 . p & f1 . p < r ) by A7, A9, XXREAL_0:2; ::_thesis: verum
end;
then consider r being real number such that
A10: for p being Element of Y holds
( r > 0 & - r < f1 . p & f1 . p < r ) ;
for x being Point of X holds
( - r < f1 . x & f1 . x < r )
proof
let x be Point of X; ::_thesis: ( - r < f1 . x & f1 . x < r )
A11: ( x in the carrier of X \ Y or x in Y ) by XBOOLE_0:def_5;
percases ( x in the carrier of X \ Y or x in Y ) by A11;
suppose x in the carrier of X \ Y ; ::_thesis: ( - r < f1 . x & f1 . x < r )
then A12: ( x in the carrier of X & not x in Y ) by XBOOLE_0:def_5;
Cl A is Subset of Y by A3;
then A13: Cl A c= Y ;
support f c= Cl A by PRE_TOPC:18;
then support f c= Y by A13, XBOOLE_1:1;
then A14: not x in support f by A12;
f . x = 0 by A14, PRE_POLY:def_7;
then |.(f . x).| = 0 ;
then f1 . x = 0 by A4, VALUED_1:18;
hence ( - r < f1 . x & f1 . x < r ) by A10; ::_thesis: verum
end;
suppose x in Y ; ::_thesis: ( - r < f1 . x & f1 . x < r )
hence ( - r < f1 . x & f1 . x < r ) by A10; ::_thesis: verum
end;
end;
end;
then consider s1 being real number such that
A15: for x being Point of X holds
( - s1 < f1 . x & f1 . x < s1 ) ;
for y being set st y in the carrier of X /\ (dom f1) holds
f1 . y <= s1 by A15;
then A16: f1 | the carrier of X is bounded_above by RFUNCT_1:70;
for y being set st y in the carrier of X /\ (dom f1) holds
- s1 <= f1 . y by A15;
then A17: f1 | the carrier of X is bounded_below by RFUNCT_1:71;
the carrier of X /\ the carrier of X = the carrier of X ;
then f1 | the carrier of X is bounded by A16, A17, RFUNCT_1:75;
then |.(f | the carrier of X).| is bounded by A4, RFUNCT_1:46;
then f | the carrier of X is bounded by CFUNCT_1:85;
hence x in ComplexBoundedFunctions the carrier of X by A2; ::_thesis: verum
end;
definition
let X be non empty TopSpace;
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
coherence
(ComplexBoundedFunctionsNorm the carrier of X) | (CC_0_Functions X) is Function of (CC_0_Functions X),REAL;
proof
for x being set st x in CC_0_Functions X holds
x in ComplexBoundedFunctions the carrier of X by Th42;
then CC_0_Functions X c= ComplexBoundedFunctions the carrier of X by TARSKI:def_3;
hence (ComplexBoundedFunctionsNorm the carrier of X) | (CC_0_Functions X) is Function of (CC_0_Functions X),REAL by FUNCT_2:32; ::_thesis: verum
end;
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);
definition
let X be non empty TopSpace;
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
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) #);
registration
let X be non empty TopSpace;
cluster C_Normed_Space_of_C_0_Functions X -> non empty strict ;
correctness
coherence
( C_Normed_Space_of_C_0_Functions X is strict & not C_Normed_Space_of_C_0_Functions X is empty );
;
end;
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
proof
let X be non empty TopSpace; ::_thesis: for x being set st x in CC_0_Functions X holds
x in CContinuousFunctions X
let x be set ; ::_thesis: ( x in CC_0_Functions X implies x in CContinuousFunctions X )
assume A1: x in CC_0_Functions X ; ::_thesis: x in CContinuousFunctions X
consider f being Function of the carrier of X,COMPLEX such that
A2: ( f = 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 ) ) ) by A1;
thus x in CContinuousFunctions X by A2; ::_thesis: verum
end;
theorem Th44: :: CC0SP2:44
for X being non empty TopSpace holds 0. (C_VectorSpace_of_C_0_Functions X) = X --> 0
proof
let X be non empty TopSpace; ::_thesis: 0. (C_VectorSpace_of_C_0_Functions X) = X --> 0
A1: C_VectorSpace_of_C_0_Functions X is Subspace of ComplexVectSpace the carrier of X by Th41;
0. (ComplexVectSpace the carrier of X) = X --> 0 ;
hence 0. (C_VectorSpace_of_C_0_Functions X) = X --> 0 by A1, CLVECT_1:30; ::_thesis: verum
end;
theorem Th45: :: CC0SP2:45
for X being non empty TopSpace holds 0. (C_Normed_Space_of_C_0_Functions X) = X --> 0
proof
let X be non empty TopSpace; ::_thesis: 0. (C_Normed_Space_of_C_0_Functions X) = X --> 0
0. (C_Normed_Space_of_C_0_Functions X) = 0. (C_VectorSpace_of_C_0_Functions X)
.= X --> 0 by Th44 ;
hence 0. (C_Normed_Space_of_C_0_Functions X) = X --> 0 ; ::_thesis: verum
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
let X be non empty TopSpace; ::_thesis: 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
let x1, x2 be Point of (C_Normed_Space_of_C_0_Functions X); ::_thesis: 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
let y1, y2 be Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x1 = y1 & x2 = y2 implies x1 + x2 = y1 + y2 )
A1: CC_0_Functions X is add-closed by Th38;
A2: ComplexBoundedFunctions the carrier of X is add-closed by CC0SP1:def_2;
assume A3: ( x1 = y1 & x2 = y2 ) ; ::_thesis: x1 + x2 = y1 + y2
thus x1 + x2 = ( the addF of (ComplexVectSpace the carrier of X) || (CC_0_Functions X)) . [x1,x2] by A1, C0SP1:def_5
.= the addF of (CAlgebra the carrier of X) . [x1,x2] by FUNCT_1:49
.= ( the addF of (CAlgebra the carrier of X) || (ComplexBoundedFunctions the carrier of X)) . [y1,y2] by A3, FUNCT_1:49
.= y1 + y2 by A2, C0SP1:def_5 ; ::_thesis: verum
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
let X be non empty TopSpace; ::_thesis: 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
let a be Complex; ::_thesis: 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
let x be Point of (C_Normed_Space_of_C_0_Functions X); ::_thesis: for y being Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st x = y holds
a * x = a * y
let y be Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X); ::_thesis: ( x = y implies a * x = a * y )
assume A1: x = y ; ::_thesis: a * x = a * y
reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def_2;
thus a * x = ( the Mult of (CAlgebra the carrier of X) | [:COMPLEX,(CC_0_Functions X):]) . [a1,x] by CSSPACE:def_9
.= the Mult of (CAlgebra the carrier of X) . [a1,x] by FUNCT_1:49
.= ( the Mult of (CAlgebra the carrier of X) | [:COMPLEX,(ComplexBoundedFunctions the carrier of X):]) . [a1,y] by A1, FUNCT_1:49
.= a * y by CC0SP1:def_3 ; ::_thesis: verum
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).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
proof
let a be Complex; ::_thesis: 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).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let X be non empty TopSpace; ::_thesis: 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).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let F, G be Point of (C_Normed_Space_of_C_0_Functions X); ::_thesis: ( ( ||.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).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
A1: ( ||.F.|| = 0 iff F = 0. (C_Normed_Space_of_C_0_Functions X) )
proof
reconsider FB = F as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Th42;
A2: ||.FB.|| = ||.F.|| by FUNCT_1:49;
A3: 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) = X --> 0 by CC0SP1:18;
A4: 0. (C_Normed_Space_of_C_0_Functions X) = X --> 0 by Th45;
( ||.FB.|| = 0 iff FB = 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ) by CC0SP1:25;
hence ( ||.F.|| = 0 iff F = 0. (C_Normed_Space_of_C_0_Functions X) ) by A2, A3, A4; ::_thesis: verum
end;
A5: ||.(a * F).|| = (abs a) * ||.F.||
proof
reconsider FB = F as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Th42;
A6: ||.FB.|| = ||.F.|| by FUNCT_1:49;
A7: a * FB = a * F by Lm14;
reconsider aFB = a * FB as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ;
reconsider aF = a * F as Point of (C_Normed_Space_of_C_0_Functions X) ;
A8: ||.aFB.|| = ||.aF.|| by A7, FUNCT_1:49;
||.(a * FB).|| = (abs a) * ||.FB.|| by CC0SP1:25;
hence ||.(a * F).|| = (abs a) * ||.F.|| by A6, A8; ::_thesis: verum
end;
||.(F + G).|| <= ||.F.|| + ||.G.||
proof
A9: ( F in ComplexBoundedFunctions the carrier of X & G in ComplexBoundedFunctions the carrier of X ) by Th42;
reconsider FB = F, GB = G as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by A9;
A10: ( ||.FB.|| = ||.F.|| & ||.GB.|| = ||.G.|| ) by FUNCT_1:49;
FB + GB = F + G by Lm13;
then A11: ||.(FB + GB).|| = ||.(F + G).|| by FUNCT_1:49;
reconsider aFB = FB + GB as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ;
reconsider aF = F, aG = G as Point of (C_Normed_Space_of_C_0_Functions X) ;
||.(FB + GB).|| <= ||.FB.|| + ||.GB.|| by CC0SP1:25;
hence ||.(F + G).|| <= ||.F.|| + ||.G.|| by A11, A10; ::_thesis: verum
end;
hence ( ( ||.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).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) by A1, A5; ::_thesis: verum
end;
Lm15: for X being non empty TopSpace holds C_Normed_Space_of_C_0_Functions X is ComplexNormSpace-like
proof
let X be non empty TopSpace; ::_thesis: C_Normed_Space_of_C_0_Functions X is ComplexNormSpace-like
for x, y being Point of (C_Normed_Space_of_C_0_Functions X)
for a being Complex holds
( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th46;
hence C_Normed_Space_of_C_0_Functions X is ComplexNormSpace-like by CLVECT_1:def_13; ::_thesis: verum
end;
registration
let X be non empty TopSpace;
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
A1: C_VectorSpace_of_C_0_Functions X is ComplexLinearSpace ;
A2: for x being Point of (C_Normed_Space_of_C_0_Functions X) st ||.x.|| = 0 holds
x = 0. (C_Normed_Space_of_C_0_Functions X) by Th46;
||.(0. (C_Normed_Space_of_C_0_Functions X)).|| = 0 by Th46;
hence ( 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 ) by A1, A2, Lm15, CSSPACE3:2, NORMSP_0:def_5, NORMSP_0:def_6; ::_thesis: verum
end;
end;
theorem :: CC0SP2:47
for X being non empty TopSpace holds C_Normed_Space_of_C_0_Functions X is ComplexNormSpace ;