:: Banach Algebra of Complex-Valued Continuous Functionals and Space of
:: Complex-valued Continuous Functionals with Bounded Support
:: by Katuhiko Kanazashi , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received May 30, 2011
:: Copyright (c) 2011-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, FUNCOP_1, NUMBERS, PRE_TOPC, ORDINAL2, SUBSET_1,
RELAT_1, XBOOLE_0, FUNCT_1, TARSKI, CARD_1, ARYTM_3, ARYTM_1, COMPLEX1,
ALGSTR_0, FUNCSDOM, REAL_1, FUNCT_2, C0SP1, IDEAL_1, VALUED_1, MESFUNC1,
RSSPACE, BINOP_1, SUPINF_2, GROUP_1, REALSET1, ZFMISC_1, XXREAL_2,
XXREAL_0, NORMSP_1, CFUNCDOM, CLVECT_1, VECTSP_1, RELAT_2, CLOPBAN2,
METRIC_1, XCMPLX_0, RCOMP_1, CONNSP_2, CC0SP1, CC0SP2, RLVECT_1,
XXREAL_1, NAT_1, CLOPBAN1, SEQ_2, RSSPACE3, LOPBAN_2, SEQFUNC, REWRITE1,
CSSPACE4, PARTFUN1, PRE_POLY, RLSUB_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, COMPLEX1, XXREAL_2, REALSET1,
VALUED_1, COMSEQ_2, SEQ_2, RCOMP_1, CFDIFF_1, SEQFUNC, PRE_POLY,
STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, GROUP_1, VECTSP_1, COMPTS_1,
NORMSP_0, CONNSP_2, PSCOMP_1, IDEAL_1, CLVECT_1, CSSPACE, CSSPACE3,
CLOPBAN1, CFUNCDOM, CLOPBAN2, NCFCONT1, C0SP1, CC0SP1;
constructors REAL_1, REALSET1, IDEAL_1, C0SP1, PARTFUN3, BINOP_2, SEQ_4,
MEASURE6, CSSPACE3, COMSEQ_3, CFDIFF_1, CC0SP1, WEIERSTR, PSCOMP_1,
NCFCONT1, SEQFUNC, INTEGRA2, PRE_POLY, C0SP2, COMSEQ_2, TOPS_2;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, XREAL_0, REALSET1, NUMBERS,
MEMBERED, VECTSP_1, VECTSP_2, VALUED_0, XXREAL_0, FUNCT_2, VALUED_1,
COMPLEX1, CFUNCDOM, XCMPLX_0, PRE_TOPC, CC0SP1, PSCOMP_1, ORDINAL1,
CLOPBAN2, COMPTS_1, RELSET_1, JORDAN5A, XXREAL_2, WAYBEL_2;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, GROUP_1;
equalities REALSET1, ALGSTR_0, XCMPLX_0, STRUCT_0, BINOP_1, VALUED_1,
CFUNCDOM, CLVECT_1, COMPLEX1, NORMSP_0, SUBSET_1, CC0SP1;
expansions TARSKI, CLVECT_1, NORMSP_0, CC0SP1;
theorems FUNCT_1, SEQ_2, COMPLEX1, ZFMISC_1, TARSKI, IDEAL_1, RELAT_1,
XXREAL_0, FUNCT_2, XBOOLE_0, XREAL_1, XCMPLX_0, FUNCOP_1, VECTSP_1,
VALUED_1, C0SP1, CFUNCDOM, CLVECT_1, CFUNCT_1, XBOOLE_1, XCMPLX_1,
ABSVALUE, CFDIFF_1, PRE_TOPC, TOPS_1, CONNSP_2, CC0SP1, RLVECT_1,
RCOMP_1, C0SP2, CLOPBAN1, NCFCONT1, CSSPACE3, NORMSP_1, PARTFUN1,
CLOPBAN2, PRE_POLY, COMPTS_1, CSSPACE, RFUNCT_1, JORDAN_A, MEMBERED,
COMSEQ_2, XXREAL_2, ORDINAL1;
begin :: Banach Algebra of Complex-Valued Continuous Functionals
definition
let X be TopStruct;
let f be Function of the carrier of X,COMPLEX;
attr f is continuous means :: PSCOMP_1:def 25
for Y being Subset of COMPLEX st Y is closed holds
f " Y is closed;
end;
definition
let X be 1-sorted, y be Complex;
func X --> y -> Function of the carrier of X,COMPLEX equals
(the carrier of X) --> y;
coherence
proof
y in COMPLEX by XCMPLX_0:def 2;
hence thesis by FUNCOP_1: 45;
end;
end;
theorem Th1:
for X being non empty TopSpace
for y being Complex
for f being Function of the carrier of X,COMPLEX st f=X --> y
holds f is continuous
proof
let X be non empty TopSpace;
let y be Complex;
let f be Function of the carrier of X,COMPLEX such that
A1: f = X --> y;
set H = the carrier of X;
set HX=[#] X;
let P1 be Subset of COMPLEX such that P1 is closed;
per cases;
suppose y in P1;
then f"P1 = HX by A1,FUNCOP_1:14;
hence f"P1 is closed;
end;
suppose not y in P1;
then f"P1 = {}X by A1,FUNCOP_1:16;
hence f"P1 is closed;
end;
end;
registration
let X be non empty TopSpace, y be Complex;
cluster X --> y -> continuous;
coherence by Th1;
end;
registration
let X be non empty TopSpace;
cluster continuous for Function of the carrier of X,COMPLEX;
existence
proof
take f = X --> 0c;
thus thesis;
end;
end;
theorem Th2:
for X being non empty TopSpace,
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,
f be Function of the carrier of X,COMPLEX;
hereby
assume
A1: f is continuous;
let Y be Subset of COMPLEX;
assume Y is open;
then Y` is closed by CFDIFF_1:def 11;
then
A2: f"(Y`) is closed by A1;
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;
end;
assume
A3: for Y being Subset of COMPLEX st Y is open holds f"Y is open;
let Y be Subset of COMPLEX;
assume
A4: 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;
end;
theorem Th3: :: LMcont
for X being non empty TopSpace
for f be 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;
let f be Function of the carrier of X,COMPLEX;
hereby
assume
A1: f is continuous;
now
let x be Point of X;
let V be Subset of COMPLEX;
set z = f.x;
reconsider z0 = z as Complex;
assume z in V & V is open; then
consider N be 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 };
S c= COMPLEX
proof
let z be object;
assume z in S;
then ex y being Complex st z = y & |.(y - z0).| < g;
hence z in COMPLEX by XCMPLX_0:def 2;
end;
then reconsider S1=S as Subset of COMPLEX;
take W = f"S;
A4: S1 is open by CFDIFF_1:13;
S is Neighbourhood of z0 by A3,CFDIFF_1:6;
then f.x in S by CFDIFF_1:7;
hence x in W by FUNCT_2:38;
thus W is open by A1,A4,Th2;
f.:(f"S) c= S by FUNCT_1:75;
then f.:W c= N by A3;
hence f .: W c= V by A2;
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;
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;
now
let Y be Subset of COMPLEX;
assume 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;
assume x in (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;
thus W is a_neighborhood of x by A8,CONNSP_2:3;
f .: W c= Y` by A7,A8;
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;
hence W c= (f"Y)` by FUNCT_2:100;
end;
then (f " Y)` is open by CONNSP_2:7;
then ((f " Y)`)` is closed by TOPS_1:4;
hence f " Y is closed;
end;
hence f is continuous;
end;
theorem Th4:
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,
f,g be continuous Function of the carrier of X,COMPLEX;
set h=f+g;
A1: rng h c= COMPLEX;
dom h = 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 as Function of the carrier of X,COMPLEX by A1,FUNCT_2:2;
A2:for x be Point of X holds h.x=f.x + g.x by VALUED_1:1;
for p being Point of X,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,V be Subset of COMPLEX;
assume
A3: h.p in V & V is open;
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 };
reconsider z1=f.p as Complex;
set S1={y where y is Complex:|.(y-z1).| < r/2 };
S1 c= COMPLEX
proof
let z be object;
assume z in S1;
then ex y being Complex st z = y & |.(y - z1).| < r/2;
hence z in COMPLEX by XCMPLX_0:def 2;
end; then
reconsider T1=S1 as Subset of COMPLEX;
A6: T1 is open by CFDIFF_1:13;
|.(z1 - z1).|=0;
then z1 in S1 by A5;
then consider W1 being Subset of X such that
A7: p in W1 & W1 is open & f.:W1 c= S1 by A6,Th3;
reconsider z2=g.p as Complex;
set S2={y where y is Complex:|.(y-z2).| < r/2 };
S2 c= COMPLEX
proof
let z be object;
assume z in S2;
then ex y being Complex st z = y & |.(y - z2).| < r/2;
hence z in COMPLEX by XCMPLX_0:def 2;
end;
then reconsider T2=S2 as Subset of COMPLEX;
A8: T2 is open by CFDIFF_1:13;
|.(z2 - z2).|=0;
then z2 in S2 by A5;
then consider W2 being Subset of X such that
A9: p in W2 & W2 is open & g.:W2 c= S2 by A8,Th3;
set W=W1 /\ W2;
A10:W is open by A7,A9,TOPS_1:11;
A11:p in W by A7,A9,XBOOLE_0:def 4;
h.:W c= S
proof
let z3 be object;
assume z3 in h.:W;
then consider x3 being object such that
A12: x3 in dom h & x3 in W & h.x3=z3 by FUNCT_1:def 6;
A13: x3 in W1 by A12,XBOOLE_0:def 4;
reconsider px=x3 as Point of X by A12;
A14: 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
A15: f.px in S1 by A7;
reconsider a1=f.px as Complex;
A16: ex aa1 be Complex st f.px = aa1 & |.(aa1-z1).| < r/2 by A15;
A17: x3 in W2 by A12,XBOOLE_0:def 4;
px in dom g by A14,FUNCT_2:def 1;
then g.px in g.:W2 by A17,FUNCT_1:def 6;
then
A18: g.px in S2 by A9;
reconsider a2=g.px as Complex;
ex aa2 be Complex st g.px = aa2 & |.(aa2-z2).| < r/2 by A18;
then
A19: |.(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
A20: |.(h.px - z0).| <= |.(a1-z1).|+|.(a2-z2).| by COMPLEX1:56;
A21: |.(a1-z1).|+|.(a2-z2).| < r/2 + |.(a2-z2).| by A16,XREAL_1:8;
r/2 + |.(a2-z2).| < r/2 + r/2 by A19,XREAL_1:8;
then |.(a1-z1).|+|.(a2-z2).| < r by A21,XXREAL_0:2;
then |.(h.px - z0).| < r by A20,XXREAL_0:2;
hence z3 in S by A12;
end;
then h.:W c= N by A5;
hence ex W being Subset of X st p in W & W is open & h.:W c= V
by A10,A11,A4,XBOOLE_1:1;
end;
hence thesis by Th3;
end;
theorem Th5:
for X being non empty TopSpace
for a being Complex
for f being continuous Function of the carrier of X,COMPLEX
holds a(#)f is continuous Function of the carrier of X,COMPLEX
proof
let X be non empty TopSpace;
let a be Complex;
let f be continuous Function of the carrier of X,COMPLEX;
set h=a(#)f;
A1:for x be Point of X holds h.x=a*f.x by VALUED_1:6;
now per cases;
suppose
A2: a<>0;
for p being Point of X,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,V be Subset of COMPLEX;
assume
A3: h.p in V & V is open;
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: |.a.|>0 by A2;
A7: r/|.a.|>0 by A2,A5;
reconsider z1=f.p as Complex;
set S1={y where y is Complex:|.(y-z1).| < r/|.a.| };
S1 c= COMPLEX
proof
let z be object;
assume z in S1;
then ex y being Complex st
z = y & |.(y - z1).| < r/|.a.|;
hence z in COMPLEX by XCMPLX_0:def 2;
end;
then reconsider T1=S1 as Subset of COMPLEX;
A8: T1 is open by CFDIFF_1:13;
|.(z1 - z1).|=0;
then z1 in S1 by A7;
then consider W1 being Subset of X such that
A9: p in W1 & W1 is open & f.:W1 c= S1 by A8,Th3;
set W=W1;
A10: W is open by A9;
A11: p in W by A9;
h.:W c= S
proof
let z3 be object;
assume z3 in h.:W;
then consider x3 being object such that
A12: x3 in dom h & x3 in W & h.x3=z3 by FUNCT_1:def 6;
reconsider px=x3 as Point of X by A12;
px in the carrier of X;
then px in dom f by FUNCT_2:def 1;
then f.px in f.:W1 by A12,FUNCT_1:def 6;
then
A13: f.px in S1 by A9;
reconsider a1=f.px as Complex;
ex aa1 be Complex st f.px = aa1 & |.(aa1-z1).| < r/|.a.| by A13;
then
A14: |.(a1 - z1).| < r/|.a.|;
A15: |.(h.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;
A16: |.a.|*|.(a1 - z1).| < |.a.|*(r/|.a.|) by A6,A14,XREAL_1:68;
|.a.|*(r/|.a.|) = r*(|.a.|/|.a.|)
.= r*1 by A6,XCMPLX_1:60
.= r;
then |.(h.px - z0).| < r by A15,A16;
hence z3 in S by A12;
end;
then h.:W c= N by A5;
hence ex W being Subset of X st p in W & W is open & h.:W c= V
by A10,A11,A4,XBOOLE_1:1;
end;
hence a(#)f is continuous by Th3;
end;
suppose
A17: a=0;
set g = X --> 0c;
set CX=the carrier of X;
A18:dom g = CX by FUNCOP_1:13;
dom h = CX by FUNCT_2:def 1;
then
A19: dom g = dom h by A18;
for z be object st z in dom h holds g.z =h.z
proof
let z be object;
assume
A20: z in dom h;
h.z = 0*(f.z) by A17,VALUED_1:6
.= 0;
hence thesis by A20,FUNCOP_1:7;
end;
hence a(#)f is continuous by A19,FUNCT_1:def 11;
end;
end;
hence thesis;
end;
theorem
for X being non empty TopSpace,
f,g be 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;
let f,g be continuous Function of the carrier of X,COMPLEX;
(-1)(#)g is continuous by Th5;
hence thesis by Th4;
end;
theorem Th7:
for X being non empty TopSpace,
f,g be 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,
f,g be continuous Function of the carrier of X,COMPLEX;
set h=f(#)g;
A1:for x be Point of X holds h.x=f.x * g.x by VALUED_1:5;
for p being Point of X,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,V be Subset of COMPLEX;
assume
A2: h.p in V & V is open;
reconsider z0=h.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;
set S1={y where y is Complex:|.(y-z1).| < r/a };
S1 c= COMPLEX
proof
let z be object;
assume z in S1;
then ex y being Complex st z = y & |.(y - z1).| < r/a;
hence z in COMPLEX by XCMPLX_0:def 2;
end;
then reconsider T1=S1 as Subset of COMPLEX;
A5: T1 is open by CFDIFF_1:13;
|.(z1 - z1).|=0;
then z1 in S1 by A4;
then consider W1 being Subset of X such that
A6: p in W1 & W1 is open & f.:W1 c= S1 by A5,Th3;
set S2={y where y is Complex:|.(y-z2).| < r/a };
S2 c= COMPLEX
proof
let z be object;
assume z in S2;
then ex y being Complex st z = y & |.(y - z2).| < r/a;
hence z in COMPLEX by XCMPLX_0:def 2;
end;
then
reconsider T2=S2 as Subset of COMPLEX;
A7: T2 is open by CFDIFF_1:13;
|.(z2 - z2).|=0;
then z2 in S2 by A4;
then consider W2 being Subset of X such that
A8: p in W2 & W2 is open & g.:W2 c= S2 by A7,Th3;
reconsider jj=1 as Real;
set S3={y where y is Complex:|.(y-z1).| < jj };
S3 c= COMPLEX
proof
let z be object;
assume z in S3;
then ex y being Complex st
z = y & |.(y - z1).| < 1;
hence z in COMPLEX by XCMPLX_0:def 2;
end;
then reconsider T3=S3 as Subset of COMPLEX;
A9:T3 is open by CFDIFF_1:13;
|.(z1 - z1).|=0;
then z1 in S3;
then consider W3 being Subset of X such that
A10:p in W3 & W3 is open & f.:W3 c= S3 by A9,Th3;
set W = W1 /\ W2 /\ W3;
W1 /\ W2 is open by A6,A8,TOPS_1:11;
then
A11: W is open by A10,TOPS_1:11;
p in W1 /\ W2 by A6,A8,XBOOLE_0:def 4;
then
A12: p in W by A10,XBOOLE_0:def 4;
h.:W c= S
proof
let z3 be object;
assume z3 in h.:W;
then consider x3 being object such that
A13: x3 in dom h & x3 in W & h.x3=z3 by FUNCT_1:def 6;
A14: x3 in W1 /\ W2 by A13,XBOOLE_0:def 4;
then
A15: x3 in W1 by XBOOLE_0:def 4;
reconsider px=x3 as Point of X by A13;
A16: px in the carrier of X;
then px in dom f by FUNCT_2:def 1;
then f.px in f.:W1 by A15,FUNCT_1:def 6;
then
A17: f.px in S1 by A6;
reconsider a1=f.px as Complex;
ex aa1 be Complex st f.px = aa1 & |.(aa1-z1).| < r/a by A17;
then
A18: |.(a1 - z1).| < r/a;
A19: x3 in W2 by A14,XBOOLE_0:def 4;
px in dom g by A16,FUNCT_2:def 1;
then g.px in g.:W2 by A19,FUNCT_1:def 6;
then
A20: g.px in S2 by A8;
reconsider a2=g.px as Complex;
ex aa2 be Complex st g.px = aa2 & |.(aa2-z2).| < r/a by A20;
then
A21: |.(a2 - z2).| < r/a;
A22: x3 in W3 by A13,XBOOLE_0:def 4;
px in dom f by A16,FUNCT_2:def 1;
then f.px in f.:W3 by A22,FUNCT_1:def 6;
then
A23: f.px in S3 by A10;
reconsider a3=f.px as Complex;
ex aa3 be Complex st f.px = aa3 & |.(aa3-z1).| < 1 by A23;
then
A24: |.(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 A24,XXREAL_0:2;
then (|.a1.|-|.z1.|)+|.z1.| < 1+|.z1.| by XREAL_1:8;
then
A25: |.a1.|< 1+|.z1.|;
A26: |.h.x3 - z0.| = |.(f.px)*(g.px) - z0.| by A1
.= |.a1*a2 - z1*z2.| by A1
.= |.(a1*a2 - a1*z2) + (a1*z2 -z1*z2).|;
A27: |.(h.x3 - z0).| <= |.a1*a2 - a1*z2.|+|.a1*z2 -z1*z2.|
by A26,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
A28: |.(h.x3 - z0).| <= |.a1.|*|.a2-z2.|+|.z2.|*|.a1-z1.| by A27;
A29: |.a1.|*|.a2-z2.|<=|.a1.|*(r/a) by A21,XREAL_1:66;
|.a1.|*(r/a) < (1+|.z1.|)*(r/a) by A25,A4,XREAL_1:68;
then
A30: |.a1.|*|.a2-z2.| < (1+|.z1.|)*(r/a) by A29,XXREAL_0:2;
A31: |.z2.|*|.a1-z1.|<=|.z2.|*(r/a) by A18,XREAL_1:66;
A32: |.a1.|*|.a2-z2.|+|.z2.|*|.a1-z1.|<(1+|.z1.|)*(r/a)+|.z2.|*|.a1-z1.|
by A30,XREAL_1:8;
(1+|.z1.|)*(r/a)+|.z2.|*|.a1-z1.|<=(1+|.z1.|)*(r/a)+|.z2.|*(r/a)
by A31,XREAL_1:6;
then
|.a1.|*|.a2-z2.|+|.z2.|*|.a1-z1.| < (1+|.z1.|)*(r/a)+|.z2.|*(r/a)
by A32,XXREAL_0:2;
then
A33: |.(h.x3 - z0).| < r*(a/a) by A28,XXREAL_0:2;
a/a = 1 by XCMPLX_0:def 7;
then |.(h.px - z0).| < r by A33;
hence z3 in S by A13;
end;
then h.:W c= N by A4;
hence ex W being Subset of X st p in W & W is open & h.:W c= V
by A11,A12,A3,XBOOLE_1:1;
end;
hence thesis by Th3;
end;
theorem Th8:
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,
f be continuous Function of the carrier of X,COMPLEX;
reconsider h = |.f.| as Function of the carrier of X,REAL;
for p being Point of X,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,V be Subset of REAL;
assume
A1: h.p in V & V is open;
reconsider r0=h.p as Real;
consider r being Real 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 };
S1 c= COMPLEX
proof
let z be object;
assume z in S1;
then ex y being Complex st
z = y & |.(y - z1).| < r;
hence z in COMPLEX by XCMPLX_0:def 2;
end; then
reconsider T1=S1 as Subset of COMPLEX;
A3: T1 is open by CFDIFF_1:13;
|.(z1 - z1).|=0;
then z1 in S1 by A2;
then consider W1 being Subset of X such that
A4: p in W1 & W1 is open & f.:W1 c= S1 by A3,Th3;
set W=W1;
A5: W is open by A4;
A6: p in W by A4;
h.:W c= ].r0-r,r0+r.[
proof
let x be object;
assume x in h.:W;
then consider z being object such that
A7: z in dom h & z in W & 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 S1 by A4;
reconsider a1=f.pz as Complex;
ex aa1 be 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 S by A7,A11,RCOMP_1:1;
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;
end;
hence thesis by C0SP2:1;
end;
definition
let X be non empty TopSpace;
func CContinuousFunctions(X) -> Subset of CAlgebra the carrier of X equals
the set of all f where f is continuous Function of the carrier of X,COMPLEX;
correctness
proof
set A = the set of all
f where f is continuous Function of the carrier of X,COMPLEX;
A c= Funcs(the carrier of X,COMPLEX)
proof
let x be object;
assume x in A;
then ex f be continuous Function of the carrier of X,COMPLEX st x=f;
hence x in Funcs(the carrier of X,COMPLEX) by FUNCT_2:8;
end;
hence thesis;
end;
end;
registration
let X be non empty TopSpace;
cluster CContinuousFunctions(X) -> non empty;
coherence
proof
X-->0c in the set of all
f where f is continuous Function of the carrier of X,COMPLEX;
hence thesis;
end;
end;
registration
let X be non empty TopSpace;
cluster CContinuousFunctions X -> Cadditively-linearly-closed
multiplicatively-closed;
coherence
proof
set W = CContinuousFunctions X;
set V = CAlgebra the carrier of X;
for v,u be Element of V st v in W & u in W holds v + u in W
proof
let v,u be Element of V such that
A1: v in W & u in W;
consider v1 be continuous Function of the carrier of X,COMPLEX such that
A2: v1=v by A1;
consider u1 be 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 be object 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 W by A6;
end; then
A7:W is add-closed by IDEAL_1:def 1;
for v be Element of V st v in W holds -v in W
proof
let v be Element of V such that
A8: v in W;
consider v1 be 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 let x be object;
assume x in dom h;
then reconsider y=x as Element of the carrier of X;
reconsider mj = -1 as Element of COMPLEX by XCMPLX_0:def 2;
h.x = mj*(v2.y) by A10,CFUNCDOM:4;
hence h.x = -v1.x by A9;
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 W by A13;
end;
then
A14:W is having-inverse by C0SP1:def 1;
for a be Complex, u be Element of V st u in W holds a * u in W
proof
let a be Complex, u be Element of V such that
A15: u in W;
consider u1 be 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;
for x be object 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 W by A19;
end;
hence CContinuousFunctions X is Cadditively-linearly-closed
by A7,A14;
A20:for v,u be Element of V st v in W & u in W holds v * u in W
proof
let v,u be Element of V such that
A21: v in W & u in W;
consider v1 be continuous Function of the carrier of X,COMPLEX such that
A22: v1=v by A21;
consider u1 be 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 be object 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 W by A26;
end;
reconsider g = ComplexFuncUnit the carrier of X
as Function of the carrier of X,COMPLEX;
g = X --> 1r;
then 1.V in W;
hence thesis by A20,C0SP1:def 4;
end;
end;
definition
let X be non empty TopSpace;
func C_Algebra_of_ContinuousFunctions X -> ComplexAlgebra equals
ComplexAlgebraStr (# CContinuousFunctions X,
mult_(CContinuousFunctions X,CAlgebra the carrier of X),
Add_(CContinuousFunctions X,CAlgebra the carrier of X),
Mult_(CContinuousFunctions X,CAlgebra the carrier of X),
One_(CContinuousFunctions X,CAlgebra the carrier of X),
Zero_(CContinuousFunctions X,CAlgebra the carrier of X) #);
coherence by CC0SP1:2;
end;
theorem
for X be 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 non empty;
coherence;
end;
registration
let X be non empty TopSpace;
cluster C_Algebra_of_ContinuousFunctions X -> Abelian add-associative
right_zeroed right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital
commutative associative right_unital right-distributive
vector-distributive scalar-distributive scalar-associative
vector-associative;
coherence
proof
now let v be VECTOR of C_Algebra_of_ContinuousFunctions X;
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;
end;
hence thesis;
end;
end;
theorem Th10:
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;
let F, G, H be VECTOR of (C_Algebra_of_ContinuousFunctions X);
let f, g, h be Function of the carrier of X,COMPLEX;
assume
A1: f = F & g = G & h = H;
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
assume A3: H = F + G;
let x be Element of the carrier of X;
h1 = f1 + g1 by A2,A3,CC0SP1:3;
hence h . x = (f . x) + (g . x) by A1,CFUNCDOM:1;
end;
assume for x being Element of X holds h . x = (f . x) + (g . x);
then h1 = f1 + g1 by A1,CFUNCDOM:1;
hence H = F + G by A2,CC0SP1:3;
end;
theorem Th11:
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;
let F, G be VECTOR of (C_Algebra_of_ContinuousFunctions X);
let f, g be Function of the carrier of X,COMPLEX;
let a be Complex;
assume
A1: f = F & g = G;
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;
hereby
assume
A3: G = a * F;
let x be Element of the carrier of X;
g1 = a * f1 by A2,A3,CC0SP1:3;
hence g . x = a * (f . x) by A1,CFUNCDOM:4;
end;
assume for x being Element of the carrier of X holds g . x = a * (f . x);
then g1 = a * f1 by A1,CFUNCDOM:4;
hence G = a * F by A2,CC0SP1:3;
end;
theorem Th12:
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;
let F, G, H be VECTOR of (C_Algebra_of_ContinuousFunctions X);
let f, g, h be Function of the carrier of X,COMPLEX;
assume
A1: f = F & g = G & h = H;
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
assume
A3: H = F * G;
let x be Element of the carrier of X;
h1 = f1 * g1 by A2,A3,CC0SP1:3;
hence h . x = (f . x) * (g . x) by A1,CFUNCDOM:2;
end;
assume for x being Element of X holds h . x = (f . x) * (g . x);
then h1 = f1 * g1 by A1,CFUNCDOM:2;
hence H = F * G by A2,CC0SP1:3;
end;
theorem Th13:
for X being non empty TopSpace holds
0.(C_Algebra_of_ContinuousFunctions X) = X --> 0c
proof
let X be non empty TopSpace;
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;
end;
theorem Th14:
for X being non empty TopSpace holds
1_(C_Algebra_of_ContinuousFunctions X) = X --> 1r
proof
let X be non empty TopSpace;
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;
end;
theorem Th15:
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;
let A1, A2 be ComplexSubAlgebra of A;
assume
A1: the carrier of A1 c= the carrier 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;
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;
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;
end;
hence A1 is ComplexSubAlgebra of A2 by A1,A2,A3,A4,CC0SP1:def 1;
end;
Lm1:
for X being compact non empty TopSpace
for x being set st x in CContinuousFunctions X holds
x in ComplexBoundedFunctions the carrier of X
proof
let X be compact non empty TopSpace;
let x be set;
assume x in CContinuousFunctions 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 such that
A3: for y being object 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 |.h.y.| < r1
proof
let y be set;
assume
A5: y in dom h;
A6: dom h1 = dom h by A2,VALUED_1:def 11;
h1.y = |.h.y.| by A2,VALUED_1:18
.= |.h.y.|;
hence thesis by A3,A5,A6;
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;
end;
theorem
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;
A1:the carrier of (C_Algebra_of_ContinuousFunctions X)
c= the carrier of (C_Algebra_of_BoundedFunctions the carrier of X)
by Lm1;
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;
end;
definition
let X be non empty compact TopSpace;
func CContinuousFunctionsNorm X -> Function of (CContinuousFunctions X),REAL
equals
(ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X);
correctness
proof
for x being object st x in CContinuousFunctions X holds
x in ComplexBoundedFunctions the carrier of X by Lm1;
then CContinuousFunctions X c= ComplexBoundedFunctions the carrier of X;
hence thesis by FUNCT_2:32;
end;
end;
definition
let X be non empty compact TopSpace;
func C_Normed_Algebra_of_ContinuousFunctions X -> Normed_Complex_AlgebraStr
equals
Normed_Complex_AlgebraStr(# (CContinuousFunctions X),
(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),
(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),
(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),
(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),
(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),
(CContinuousFunctionsNorm X) #);
correctness;
end;
registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> non empty strict;
correctness;
end;
Lm2:
now
let X be non empty compact TopSpace;
set F = C_Normed_Algebra_of_ContinuousFunctions X;
let x, e be Element of (C_Normed_Algebra_of_ContinuousFunctions X);
assume
A1: e = One_ ((CContinuousFunctions X),(CAlgebra the carrier of 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;
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;
end;
registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> unital;
correctness
proof
reconsider e = One_(CContinuousFunctions X,CAlgebra the carrier of X) as
Element of C_Normed_Algebra_of_ContinuousFunctions X;
take e;
thus for b1 being Element of
the carrier of (C_Normed_Algebra_of_ContinuousFunctions X) holds
b1 * e = b1 & e * b1 = b1 by Lm2;
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;
let x1, x2 be Point of C_Normed_Algebra_of_ContinuousFunctions X;
let y1, y2 be Point of C_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume
A1: x1 = y1 & x2 = 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;
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;
let a be Complex;
let x be Point of C_Normed_Algebra_of_ContinuousFunctions X;
let y be Point of C_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume
A1: x = 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;
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;
let x1, x2 be Point of C_Normed_Algebra_of_ContinuousFunctions X;
let y1, y2 be Point of C_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume
A1: x1 = y1 & x2 = 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;
end;
theorem Th17:
for X being non empty compact TopSpace holds
C_Normed_Algebra_of_ContinuousFunctions X is ComplexAlgebra
proof
let X being non empty compact TopSpace;
1.(C_Normed_Algebra_of_ContinuousFunctions X)
= 1_C_Algebra_of_ContinuousFunctions X;
hence thesis by CC0SP1:14;
end;
registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> right_complementable
Abelian add-associative right_zeroed vector-distributive scalar-distributive
scalar-associative associative commutative right-distributive right_unital
vector-associative;
coherence by Th17;
end;
theorem
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;
let F be Point of C_Normed_Algebra_of_ContinuousFunctions X;
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 thesis;
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
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;
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 thesis by A1;
end;
hence C_Normed_Algebra_of_ContinuousFunctions X is vector-distributive &
C_Normed_Algebra_of_ContinuousFunctions X is scalar-distributive
scalar-associative scalar-unital;
end;
end;
theorem
for X being non empty compact TopSpace holds
C_Normed_Algebra_of_ContinuousFunctions X is ComplexLinearSpace;
theorem Th20:
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;
X --> 0 = 0.(C_Algebra_of_ContinuousFunctions X) by Th13;
hence X --> 0 = 0.(C_Normed_Algebra_of_ContinuousFunctions X);
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;
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;
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;
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);
end;
theorem
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;
let F be Point of C_Normed_Algebra_of_ContinuousFunctions X;
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;
end;
theorem Th22:
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;
let f, g, h be Function of the carrier of X,COMPLEX;
let F, G, H be Point of C_Normed_Algebra_of_ContinuousFunctions X;
reconsider f1 = F, g1 = G, h1 = H as
VECTOR of C_Algebra_of_ContinuousFunctions X;
(H=F+G iff h1=f1+g1);
hence thesis by Th10;
end;
theorem
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;
let X be non empty compact TopSpace;
let f, g be Function of the carrier of X,COMPLEX;
let F, G be Point of C_Normed_Algebra_of_ContinuousFunctions X;
reconsider f1 = F, g1 = G as VECTOR of C_Algebra_of_ContinuousFunctions X;
(G = a*F iff g1 = a*f1);
hence thesis by Th11;
end;
theorem
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;
let f, g, h be Function of the carrier of X,COMPLEX;
let F, G, H be Point of C_Normed_Algebra_of_ContinuousFunctions X;
reconsider f1 = F, g1 = G, h1 = H
as VECTOR of C_Algebra_of_ContinuousFunctions X;
H = F*G iff h1 = f1*g1;
hence thesis by Th12;
end;
theorem Th25:
for X being non empty compact TopSpace holds
||.0.C_Normed_Algebra_of_ContinuousFunctions X.|| = 0
proof
let X be non empty compact TopSpace;
set 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 thesis by Lm7,FUNCT_1:49;
end;
theorem Th26:
for X being non empty compact TopSpace
for F being Point of C_Normed_Algebra_of_ContinuousFunctions X holds
||.F.|| = 0 implies F = 0.C_Normed_Algebra_of_ContinuousFunctions X
proof
let X be non empty compact TopSpace;
let F be Point of 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 thesis by Lm7,FUNCT_1:49;
end;
theorem Th27:
for a being Complex
for X being non empty compact TopSpace
for F being Point of C_Normed_Algebra_of_ContinuousFunctions X holds
||.(a*F).|| = |.a.|*||.F.||
proof
let a be Complex;
let X be non empty compact TopSpace;
let F be Point of C_Normed_Algebra_of_ContinuousFunctions X;
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
.= |.a.| * ||.F1.|| by CC0SP1:25
.= |.a.| * ||.F.|| by FUNCT_1:49;
end;
theorem Th28:
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;
let F, G be Point of C_Normed_Algebra_of_ContinuousFunctions X;
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;
end;
registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X ->
discerning reflexive ComplexNormSpace-like;
coherence
by Th25,Th26,Th27,Th28;
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;
let x1, x2 be Point of C_Normed_Algebra_of_ContinuousFunctions X;
let y1, y2 be Point of C_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume
A1: x1 = y1 & x2 = 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;
end;
theorem
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;
let f, g, h be Function of the carrier of X,COMPLEX;
let F, G, H be Point of C_Normed_Algebra_of_ContinuousFunctions X;
assume
A1: f = F & g = G & h = H;
A2:now
assume H = F - G;
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
let x be Element of X;
f.x = (h.x) + (g.x) by A1,A3,Th22;
hence (f.x) - (g.x) = h.x;
end;
hence for x being Element of X holds h . x = (f . x) - (g . x);
end;
now
assume
A4: for x being Element of X holds h.x = (f.x) - (g.x);
now
let x be Element of X;
h . x = (f . x) - (g . x) by A4;
hence (h . x) + (g . x) = f . x;
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;
end;
hence H = F - G iff for x being Element of X holds h.x = (f.x)-(g.x)
by A2;
end;
theorem Th30:
for X being ComplexBanachSpace
for Y being Subset of X
for seq being sequence of X st Y is closed & rng seq c= Y
& seq is CCauchy
holds seq is convergent & lim seq in Y
by CLOPBAN1:def 13,NCFCONT1:def 3;
theorem Th31:
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;
let Y be Subset of C_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume
A1:Y = CContinuousFunctions X;
now
let seq be sequence of
C_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume
A2: rng seq c= Y & seq is convergent;
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
let z be object;
assume z in ComplexBoundedFunctions the carrier of X;
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;
end;
then
ComplexBoundedFunctions the carrier of X
c= PFuncs ( the carrier of X,COMPLEX);
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 Nat st
for n being Nat
for x being set st n >= k & x in the carrier of X holds
|.((H . n) . x) - (f . x).| < p
proof
let p be Real;
assume p > 0;
then
consider k being Nat such that
A5: for n being Nat st n >= k holds
||.((seq . n) - (lim seq)).|| < p by A2,CLVECT_1:def 16;
take k;
hereby
let n be Nat;
let x be set;
assume
A6: n >= k & x in the carrier of X;
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;
|.g . x0.| <= ||.((seq . n) - (lim seq)).|| by A8,CC0SP1:19;
hence |.((H . n) . x) - (f . x).| < p by A10,A9,A7,XXREAL_0:2;
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;
let V be Subset of COMPLEX;
assume
A11: f.x in V & V is open;
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;
consider k being Nat such that
A15: for n be Nat,x be set st n>=k & x in the carrier of X
holds |.(H.n).x - f.x.| < r/3 by A4,A14;
k in NAT by ORDINAL1:def 12;
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 be 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-z1).| < r/3 };
G1 c= COMPLEX
proof
let z be object;
assume z in G1;
then ex y being Complex st
z = y & |.(y - z1).| < r/3;
hence z in COMPLEX by XCMPLX_0:def 2;
end;
then
reconsider T1=G1 as Subset of COMPLEX;
A17: T1 is open by CFDIFF_1:13;
|.(z1 - z1).|=0;
then z1 in G1 by A13;
then
consider W1 being Subset of X such that
A18: x in W1 & W1 is open & h.:W1 c= G1 by A17,Th3;
now
let zz0 be object;
assume
zz0 in f.:W1;
then
consider xx0 being object 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 G1 by A18;
then
consider hx0 being Complex such that
A20: hx0=h.xx0 & |.hx0-z1.| < 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 S by A19;
end;
then f.:W1 c= S;
then f.:W1 c= N by A13;
hence ex W being Subset of X st
x in W & W is open & f .: W c= V by A18,A12,XBOOLE_1:1;
end;
hence f is continuous by Th3;
end;
hence lim seq in Y by A3,A1;
end;
hence Y is closed by NCFCONT1:def 3;
end;
theorem Th32:
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;
let vseq be sequence of (C_Normed_Algebra_of_ContinuousFunctions X);
assume
A1: vseq is CCauchy;
A2:for x being object st x in CContinuousFunctions X holds
x in ComplexBoundedFunctions the carrier of X by Lm1;
then
CContinuousFunctions X c= ComplexBoundedFunctions the carrier of X;
then
rng vseq c= ComplexBoundedFunctions the carrier of X;
then
reconsider vseq1 = vseq
as sequence of (C_Normed_Algebra_of_BoundedFunctions the carrier of X)
by FUNCT_2:6;
now
let e be Real;
assume
A3: e > 0;
consider k being Nat such that
A4: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1,A3,CSSPACE3:8;
take k;
now
let n, m be Nat;
assume n >= k & m >= k;
then ||.((vseq . n) - (vseq . m)).|| < e by A4;
hence ||.((vseq1 . n) - (vseq1 . m)).|| < e by Lm9,Lm3;
end;
hence for n, m being Nat st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e;
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 Nat st
for n being Nat st n >= k holds ||.((vseq . n) - tv).|| < e
proof
let e be Real;
assume e > 0;
then
consider k being Nat such that
A8: for n being Nat st n >= k holds
||.((vseq1 . n) - (lim vseq1)).|| < e by A6,CLVECT_1:def 16;
take k;
now
let n be Nat;
assume n >= k;
then ||.((vseq1 . n) - (lim vseq1)).|| < e by A8;
hence ||.((vseq . n) - tv).|| < e by Lm9,Lm3;
end;
hence for n being Nat st n >= k holds
||.((vseq . n) - tv).|| < e;
end;
hence vseq is convergent;
end;
registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> complete;
coherence
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;
end;
end;
registration
let X be non empty compact TopSpace;
cluster C_Normed_Algebra_of_ContinuousFunctions X -> Banach_Algebra-like;
coherence
proof
set B = C_Normed_Algebra_of_ContinuousFunctions X;
A1:now
let f, g be Element of (C_Normed_Algebra_of_ContinuousFunctions X);
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;
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
let a be Complex;
let f, g be Element of (C_Normed_Algebra_of_ContinuousFunctions X);
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;
end;
now
let f, g, h be Element of (C_Normed_Algebra_of_ContinuousFunctions X);
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;
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,def 10,def 11,VECTSP_1:def 3;
hence C_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like;
end;
end;
:: Some properties of support
theorem Th33:
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;
let f,g be Function of the carrier of X,COMPLEX;
set CX= the carrier of X;
set h=f+g;
A1: rng h c= COMPLEX;
dom h = 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 as Function of the carrier of X,COMPLEX by A1,FUNCT_2:2;
dom f = CX & dom g = CX & dom h = CX by FUNCT_2:def 1;
then
A2: support(f) c= CX & support(g) c= CX & support(h) c= CX by PRE_POLY:37;
now let x be object;
assume
x in (CX\ support(f)) /\ (CX\ support(g));
then
x in (CX\ support(f)) & x in (CX\ support(g)) by XBOOLE_0:def 4;
then
x in CX & not x in support(f) & x in CX & not x in support(g)
by XBOOLE_0:def 5;
then
A3: x in CX & 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 CX & (f+g).x =0 by A3;
not x in support(f+g) by A4,PRE_POLY:def 7;
hence x in CX\ support(f+g) by A4,XBOOLE_0:def 5;
end;
then
(CX\ support(f)) /\ (CX\ support(g)) c= CX\ support(f+g);
then
CX\ ( support(f) \/ support(g) ) c= CX\ support(f+g) by XBOOLE_1:53;
then CX\ (CX\ support(f+g)) c=CX\ (CX\ (support(f) \/ support(g)))
by XBOOLE_1:34;
then
CX/\ support(f+g) c=CX\ (CX\ (support(f) \/ support(g))) by XBOOLE_1:48;
then
CX/\ support(f+g) c= CX/\ (support(f) \/ support(g)) by XBOOLE_1:48;
then
support(f+g) c= CX/\ (support(f) \/ support(g)) by A2,XBOOLE_1:28;
then support(f+g) c= (CX/\ support(f)) \/ (CX/\ support(g))
by XBOOLE_1:23;
then support(f+g) c= support(f) \/ (CX/\ support(g)) by A2,XBOOLE_1:28;
hence support(f+g) c= support(f) \/ support(g) by A2,XBOOLE_1:28;
end;
theorem Th34:
for X being non empty TopSpace
for a be Complex,f be Function of the carrier of X,COMPLEX
holds support(a(#)f) c= support(f)
proof
let X be non empty TopSpace;
let a be Complex,f be Function of the carrier of X,COMPLEX;
set CX= the carrier of X;
reconsider h=a(#)f as Function of the carrier of X,COMPLEX;
let x be object;
assume x in support(a(#)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;
end;
theorem
for X being non empty TopSpace
for f,g be Function of the carrier of X,COMPLEX
holds support(f(#)g) c= support(f) \/ support(g)
proof
let X be non empty TopSpace;
let f,g be Function of the carrier of X,COMPLEX;
set CX = the carrier of X;
reconsider h=f(#)g as Function of the carrier of X,COMPLEX;
dom f = CX & dom g = CX & dom h = CX by FUNCT_2:def 1;
then
A1: support(f) c= CX & support(g) c= CX & support(h) c= CX by PRE_POLY:37;
now let x be object;
assume x in (CX\ support(f)) /\ (CX\ support(g));
then
x in (CX\ support(f)) & x in (CX\ support(g)) by XBOOLE_0:def 4;
then
x in CX& not x in support(f) & x in CX & not x in support(g)
by XBOOLE_0:def 5;
then
A2: x in CX& 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 CX & (f(#)g).x =0 by A2;
not x in support(f(#)g) by A3,PRE_POLY:def 7;
hence x in CX\ support(f(#)g) by A3,XBOOLE_0:def 5;
end;
then (CX\ support(f)) /\ (CX\ support(g)) c= CX\ support(f(#)g);
then
CX\ (support(f) \/ support(g) ) c= CX\ support(f(#)g) by XBOOLE_1:53;
then CX\ (CX\ support(f(#)g)) c=CX\ (CX\ (support(f) \/ support(g)))
by XBOOLE_1:34;
then
CX/\ support(f(#)g) c=CX\ (CX\ (support(f) \/ support(g))) by XBOOLE_1:48;
then
CX/\ support(f(#)g) c= CX/\ (support(f) \/ support(g)) by XBOOLE_1:48;
then
support(f(#)g) c= CX/\ (support(f) \/ support(g)) by A1,XBOOLE_1:28;
then
support(f(#)g) c= (CX/\ support(f)) \/ (CX/\ support(g)) by XBOOLE_1:23;
then support(f(#)g) c= support(f) \/ (CX/\ support(g)) by A1,XBOOLE_1:28;
hence support(f(#)g) c= support(f) \/ support(g) by A1,XBOOLE_1:28;
end;
:: Space of Complex-Valued Continuous Functionals with bounded support
definition
let X be non empty TopSpace;
func CC_0_Functions(X) -> non empty Subset of
ComplexVectSpace the carrier of X equals
{ f where f is Function of the carrier of X,COMPLEX : f is continuous &
ex Y be 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
proof
A1:{ f where f is Function of the carrier of X,COMPLEX : f is continuous &
ex Y be 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 object;
assume x in { f where f is Function of the carrier of X,COMPLEX
: f is continuous &
ex Y be 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))};
then
ex f be Function of the carrier of X,COMPLEX
st x=f & f is continuous & ex Y be 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;
end;
{ f where f is Function of the carrier of X,COMPLEX : f is continuous &
ex Y be 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
proof
set g= (the carrier of X) --> 0c;
reconsider g 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 being Subset of COMPLEX such that P is closed;
set F = (the carrier of X) --> 0, H = the carrier of X;
set HX=[#] X;
per cases;
suppose 0 in P;
then g"P = HX by FUNCOP_1:14;
hence g"P is closed;
end;
suppose not 0 in P;
then F"P = {}X by FUNCOP_1:16;
hence g"P is closed;
end;
end;
hence thesis;
end;
A3: ex Y be 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 compact non empty Subset of X;
for A being Subset of X st A=support(g) holds Cl(A) is Subset of S
proof
let A be Subset of X;
assume
A4: A=support(g);
A5: A={}
proof
assume
A6: not thesis;
set p = the Element of support(g);
A7: p in A by A6,A4; then
g.p<>0 by A4,PRE_POLY:def 7;
hence contradiction by A7,FUNCOP_1:7;
end;
Cl({}X)={} by PRE_TOPC:22;
hence thesis by A5,XBOOLE_1:2;
end;
hence thesis;
end;
g in { f where f is Function of the carrier of X,COMPLEX
: f is continuous &
ex Y be 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 thesis;
end;
hence thesis by A1;
end;
end;
theorem
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 be 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;
set W = CC_0_Functions(X);
set V = CAlgebra the carrier of X;
let u,v be Element of V such that
A1:u in W & v in W;
consider u1 be Function of the carrier of X,COMPLEX such that
A2: u1=u & u1 is continuous
& (ex Y1 be 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 be 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 be Function of the carrier of X,COMPLEX such that
A4: v1=v & v1 is continuous
& (ex Y2 be 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 be 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 be 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 be 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 object 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 thesis by A8,A9,A16;
end;
Lm11:
for X being non empty TopSpace
for a be Complex,u be 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;
set W = CC_0_Functions(X);
set V = CAlgebra the carrier of X;
let a be Complex;
let u be Element of V;
assume
A1: u in W;
consider u1 be Function of the carrier of X,COMPLEX such that
A2: u1=u & u1 is continuous
& (ex Y1 be 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 be 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 be 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);
A11:for x be 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 object 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 thesis by A5,A3,A10;
end;
Lm12:
for X being non empty TopSpace
for u be 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;
set W = CC_0_Functions(X);
set V = CAlgebra the carrier of X;
let u be Element of V;
assume
A1: u in W;
set a=-1r;
-u = a*u by CLVECT_1:3;
hence thesis by A1,Lm11;
end;
theorem
for X being non empty TopSpace
for W be non empty Subset of CAlgebra the carrier of X
st W= CC_0_Functions X
holds W is Cadditively-linearly-closed
proof
let X being non empty TopSpace;
let W be non empty Subset of CAlgebra the carrier of X;
assume
A1: W= CC_0_Functions X;
set V = CAlgebra the carrier of X;
for v,u be Element of V 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 be Element of V st v in W holds -v in W by A1,Lm12;
then
A3: W is having-inverse by C0SP1:def 1;
for a be Complex, u be Element of V st u in W holds a * u in W
by A1,Lm11;
hence W is Cadditively-linearly-closed by A2,A3;
end;
theorem Th38:
for X being non empty TopSpace holds
CC_0_Functions X is add-closed
proof
let X be non empty TopSpace;
set Y = CC_0_Functions X;
set V = ComplexVectSpace(the carrier of X);
for v,u be VECTOR of V st v in Y & u in Y holds v + u in Y
proof
let v,u be VECTOR of V;
assume
A1: v in Y & u in Y;
reconsider v2=v, u2=u as VECTOR of CAlgebra the carrier of X;
v2+u2 in Y by A1,Lm10;
hence thesis;
end;
hence thesis by IDEAL_1:def 1;
end;
theorem Th39:
for X being non empty TopSpace holds
CC_0_Functions X is linearly-closed
proof
let X be non empty TopSpace;
set Y = CC_0_Functions X;
set V = ComplexVectSpace(the carrier of X);
A1:for v,u be VECTOR of V st v in Y & u in Y holds v + u in Y
proof
let v,u be VECTOR of V;
assume
A2: v in Y & u in Y;
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 Y by A2,Lm10;
hence thesis;
end;
A3:for a be Complex, v be Element of V st v in Y holds a * v in Y
proof
let a be Complex, v be VECTOR of V;
assume
A4: v in Y;
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 Y by A4,Lm11;
hence thesis;
end;
thus thesis by A1,A3;
end;
registration
let X being non empty TopSpace;
cluster CC_0_Functions X -> non empty linearly-closed;
correctness by Th39;
end;
theorem Th40: :: CSSPACE:13
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;
let V1 be Subset of V;
assume that
A1: V1 is linearly-closed and
A2: not V1 is empty;
for v, u being VECTOR of V st v in V1 & u in V1 holds
v + u in V1 by A1;
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;
end;
theorem Th41:
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
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 by Th41;
end;
theorem Th42:
for X be 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;
let x be set such that
A1: x in CC_0_Functions(X);
consider f be Function of the carrier of X,COMPLEX such that
A2: f=x & f is continuous
& (ex Y be 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 be 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;
reconsider r2 = sup Y1 as Real;
consider r be Real such that
A6: r=|.r1.|+|.r2.|+1;
for p being Element of Y holds r>0 & -r < f1.p & f1.p <r
proof
let p be Element of Y;
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 be Real such that
A7: r3=f1.p & r1<=r3 & r3<=r2;
-|.r1.| <= r1 by ABSVALUE:4;
then -|.r1.| - |.r2.| <= r1 - 0 by XREAL_1:13;
then -|.r1.| - |.r2.| - 1 < r1 - 0 by XREAL_1:15;
then
A8: -r < r1 by A6;
r2 <= |.r2.| by ABSVALUE:4;
then r2 + 0 <= |.r2.|+|.r1.| by XREAL_1:7;
then
A9: r2 < r by A6,XREAL_1:8;
-r < f1.p by A7,A8,XXREAL_0:2;
hence thesis by A7,A9,XXREAL_0:2;
end;
then consider r be Real such that
A10: for p being Element of Y holds r>0 & -r< f1.p & f1.p <r;
for x be Point of X holds -r< f1.x & f1.x <r
proof
let x be Point of X;
A11:x in (the carrier of X) \ Y or x in Y by XBOOLE_0:def 5;
per cases by A11;
suppose
x in (the carrier of X) \ Y;
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;
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;
end;
suppose x in Y;
hence thesis by A10;
end;
end;
then
consider s1 be Real such that
A15: for x be Point of X holds (-s1< f1.x & f1.x <s1);
for y being object 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 object 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;
end;
definition
let X be non empty TopSpace;
func CC_0_FunctionsNorm X -> Function of CC_0_Functions(X),REAL equals
(ComplexBoundedFunctionsNorm the carrier of X)|(CC_0_Functions(X));
correctness
proof
for x being object 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;
hence thesis by FUNCT_2:32;
end;
end;
definition
let X be non empty TopSpace;
func C_Normed_Space_of_C_0_Functions X -> CNORMSTR equals
CNORMSTR (# CC_0_Functions X,
Zero_(CC_0_Functions X, ComplexVectSpace(the carrier of X)),
Add_(CC_0_Functions X, ComplexVectSpace(the carrier of X)),
Mult_(CC_0_Functions X, ComplexVectSpace(the carrier of X)),
CC_0_FunctionsNorm X #);
correctness;
end;
registration
let X be non empty TopSpace;
cluster C_Normed_Space_of_C_0_Functions X -> strict non empty;
correctness;
end;
theorem
for X be non empty TopSpace
for x be set st x in CC_0_Functions(X) holds
x in CContinuousFunctions X
proof
let X be non empty TopSpace;
let x be set such that
A1: x in CC_0_Functions(X);
consider f be Function of the carrier of X,COMPLEX such that
A2: f=x & f is continuous
& (ex Y be 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 thesis by A2;
end;
theorem Th44:
for X be non empty TopSpace holds
0.C_VectorSpace_of_C_0_Functions X = X --> 0
proof
let X be non empty TopSpace;
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 thesis by A1,CLVECT_1:30;
end;
theorem Th45:
for X be non empty TopSpace holds
0.C_Normed_Space_of_C_0_Functions X = X --> 0
proof
let X be non empty TopSpace;
0.C_Normed_Space_of_C_0_Functions X
=0.C_VectorSpace_of_C_0_Functions X
.=X --> 0 by Th44;
hence thesis;
end;
Lm13:
for X be non empty TopSpace
for x1,x2 be Point of C_Normed_Space_of_C_0_Functions X,
y1,y2 be 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;
let x1,x2 be Point of C_Normed_Space_of_C_0_Functions X,
y1,y2 be Point of C_Normed_Algebra_of_BoundedFunctions the carrier of X;
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;
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;
end;
Lm14:
for X be non empty TopSpace
for a be Complex,x be Point of C_Normed_Space_of_C_0_Functions(X),
y be 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;
let a be Complex, x be Point of C_Normed_Space_of_C_0_Functions(X),
y be Point of C_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume
A1: x=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;
end;
theorem Th46:
for a be Complex
for X be non empty TopSpace
for F,G be Point of C_Normed_Space_of_C_0_Functions(X) holds
(||.F.|| = 0 iff F = 0.C_Normed_Space_of_C_0_Functions(X) ) &
||.a*F.|| = |.a.| * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||
proof
let a be Complex;
let X be non empty TopSpace;
let F,G be Point of C_Normed_Space_of_C_0_Functions(X);
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 thesis by A2,A3,A4;
end;
A5:||.a*F.|| = |.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.|| = |.a.| * ||.FB.|| by CC0SP1:25;
hence thesis by A6,A8;
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 thesis by A11,A10;
end;
hence thesis by A1,A5;
end;
Lm15: for X be non empty TopSpace holds
C_Normed_Space_of_C_0_Functions(X) is ComplexNormSpace-like
by Th46;
registration
let X be non empty TopSpace;
cluster C_Normed_Space_of_C_0_Functions(X) -> reflexive discerning
ComplexNormSpace-like vector-distributive scalar-distributive
scalar-associative scalar-unital Abelian add-associative right_zeroed
right_complementable;
coherence
proof
A1:C_VectorSpace_of_C_0_Functions(X) is ComplexLinearSpace;
A2:for x be Point of C_Normed_Space_of_C_0_Functions(X)
holds ( ||.x.|| = 0 implies
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 thesis by A1,A2,Lm15,CSSPACE3:2;
end;
end;
theorem
for X be non empty TopSpace holds
C_Normed_Space_of_C_0_Functions(X) is ComplexNormSpace;