:: Banach Algebra of Continuous Functionals and Space of Real-valued
:: Continuous Functionals with Bounded Support
:: by Katuhiko Kanazashi, Noboru Endou and Yasunari Shidama
::
:: Received October 20, 2009
:: Copyright (c) 2009-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, PSCOMP_1, NUMBERS, PRE_TOPC, ORDINAL2,
SUBSET_1, RCOMP_1, RELAT_1, XBOOLE_0, FUNCT_1, TARSKI, CARD_1, ARYTM_3,
XXREAL_1, ARYTM_1, COMPLEX1, CONNSP_2, RLVECT_1, ALGSTR_0, FUNCSDOM,
REAL_1, FUNCT_2, C0SP1, IDEAL_1, VALUED_1, MESFUNC1, RSSPACE, POLYALG1,
BINOP_1, VECTSP_1, SUPINF_2, GROUP_1, REALSET1, ZFMISC_1, RSSPACE4,
XXREAL_2, XXREAL_0, LOPBAN_2, NORMSP_1, REWRITE1, NAT_1, RSSPACE3, SEQ_2,
PARTFUN1, SEQFUNC, C0SP2, LOPBAN_1, METRIC_1, RELAT_2, PRE_POLY, RLSUB_1,
TOPMETR, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_0, REALSET1, FUNCT_1,
FUNCT_2, STRUCT_0, ALGSTR_0, IDEAL_1, BINOP_1, DOMAIN_1, RELSET_1,
PRE_TOPC, COMPTS_1, PSCOMP_1, RLVECT_1, GROUP_1, VECTSP_1, FUNCSDOM,
PARTFUN1, SEQFUNC, RSSPACE3, RCOMP_1, SEQ_2, NORMSP_0, NORMSP_1,
NFCONT_1, LOPBAN_1, LOPBAN_2, C0SP1, CONNSP_2, FUNCOP_1, PRE_POLY,
XXREAL_2, VALUED_1, RLSUB_1, RSSPACE, TOPMETR;
constructors REAL_1, REALSET1, RSSPACE3, COMPLEX1, RCOMP_1, IDEAL_1, C0SP1,
NFCONT_1, SEQFUNC, MEASURE6, PRE_POLY, TOPMETR, RLSUB_1, SEQ_4, NAGATA_1,
PSCOMP_1, COMPTS_1, COMSEQ_2, NUMBERS;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, XREAL_0, REALSET1,
ALGSTR_0, NUMBERS, ORDINAL1, MEMBERED, FUNCSDOM, VECTSP_1, VECTSP_2,
VALUED_0, LOPBAN_2, PSCOMP_1, RCOMP_1, C0SP1, COMPTS_1, XXREAL_0,
FUNCT_2, VALUED_1, XXREAL_2, TOPMETR, RELSET_1, WAYBEL_2, JORDAN5A;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions PSCOMP_1, TARSKI, FUNCSDOM, RLVECT_1, VECTSP_1, GROUP_1, NORMSP_0;
equalities REALSET1, ALGSTR_0, XCMPLX_0, RCOMP_1, FUNCSDOM, RLVECT_1,
STRUCT_0, BINOP_1, C0SP1, NORMSP_0;
expansions PSCOMP_1, ALGSTR_0, TARSKI, RCOMP_1, RLVECT_1, C0SP1, NORMSP_0;
theorems RFUNCT_1, FUNCT_1, NFCONT_1, PARTFUN1, SEQ_2, ABSVALUE, ALGSTR_0,
COMPLEX1, ZFMISC_1, TARSKI, RCOMP_1, XBOOLE_1, PSCOMP_1, IDEAL_1,
RSSPACE3, RELAT_1, XREAL_0, XXREAL_0, FUNCSDOM, NORMSP_1, LOPBAN_1,
FUNCT_2, XREAL_1, RLVECT_1, TOPS_1, FUNCOP_1, VECTSP_1, GROUP_1,
LOPBAN_2, VALUED_1, C0SP1, CONNSP_2, XXREAL_1, PRE_POLY, XBOOLE_0,
RSSPACE, COMPTS_1, PRE_TOPC, RLSUB_1, JORDAN_A, NAGATA_1, JGRAPH_2,
TOPMETR, JORDAN5A, XXREAL_2, ORDINAL1;
begin :: Banach Algebra of Continuous Functionals
definition
let X be 1-sorted, y be Real;
func X --> y -> RealMap of X equals
(the carrier of X) --> y;
coherence
proof
y in REAL by XREAL_0:def 1;
hence thesis by FUNCOP_1:45;
end;
end;
registration
let X be TopSpace, y be Real;
cluster X --> y -> continuous;
coherence
proof
set f = X --> y;
set HX=[#] X;
let P1 be Subset of REAL such that P1 is closed;
per cases;
suppose y in P1;
then f"P1 = HX by FUNCOP_1:14;
hence f"P1 is closed;
end;
suppose not y in P1;
then f"P1 = {}X by FUNCOP_1:16;
hence f"P1 is closed;
end;
end;
end;
theorem Th1:
for X being non empty TopSpace, f be RealMap of X holds f is continuous iff
for x being Point of X,V being Subset of REAL 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,f be RealMap of X;
hereby assume
A1: f is continuous;
now let x be Point of X,V being Subset of REAL;
set r = f.x;
assume r in V & V is open;
then
consider r0 be Real such that
A2: 0<r0 & ].r-r0,r+r0.[ c= V by RCOMP_1:19;
set S = ]. r-r0,r+r0 .[;
take W= f"S;
|.r-r.| < r0 by A2,COMPLEX1:44;
then
r in S by RCOMP_1:1;
hence x in W by FUNCT_2:38;
thus W is open by A1,PSCOMP_1:8;
f.:(f"S) c= S by FUNCT_1:75;
hence f.:W c= V by A2;
end;
hence for x being Point of X,V being Subset of REAL 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
A3:for x being Point of X,V being Subset of REAL 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 REAL;
assume Y is closed;
then
Y`` is closed;
then
A4: Y` is open;
for x being Point of X st x in (f"Y)` 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 REAL such that
A5: f.x in V & V is open & V c= Y` by A4;
consider W being Subset of X such that
A6: x in W & W is open & f.:W c= V by A3,A5;
take W;
thus W is a_neighborhood of x by A6,CONNSP_2:3;
f.:W c= Y` by A5,A6;
then
A7: 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 A7;
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;
definition let X be non empty TopSpace;
func ContinuousFunctions(X) -> Subset of RAlgebra the carrier of X equals
the set of all f where f is continuous RealMap of X ;
correctness
proof
set A = the set of all f where f is continuous RealMap of X ;
A c= Funcs(the carrier of X,REAL)
proof
let x be object;
assume x in A;
then ex f be continuous RealMap of X st x=f;
hence x in Funcs(the carrier of X,REAL) by FUNCT_2:8;
end;
hence thesis;
end;
end;
registration
let X be non empty TopSpace;
cluster ContinuousFunctions(X) -> non empty;
coherence
proof
X-->0 in the set of all f where f is continuous RealMap of X ;
hence thesis;
end;
end;
registration
let X be non empty TopSpace;
cluster ContinuousFunctions(X) -> additively-linearly-closed
multiplicatively-closed;
coherence
proof
set W = ContinuousFunctions(X);
set V = RAlgebra the carrier of X;
A1:RAlgebra the carrier of X is RealLinearSpace by C0SP1:7;
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
A2: v in W & u in W;
consider v1 be continuous RealMap of X such that
A3: v1=v by A2;
consider u1 be continuous RealMap of X such that
A4: u1=u by A2;
A5: v1+u1 is Function of the carrier of X,REAL & v1+u1 is continuous
by NAGATA_1:22;
reconsider h = v+u as Element of Funcs(the carrier of X,REAL);
A6: ex f being Function st
h = f & dom f = the carrier of X & rng f c= REAL by FUNCT_2:def 2;
dom v1 /\ dom u1 = (the carrier of X) /\ dom u1 by FUNCT_2:def 1;
then
A7: 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 A3,A4,FUNCSDOM:1;
then v+u=v1+u1 by A7,A6,VALUED_1:def 1;
hence v+u in W by A5;
end;
then
A8: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
A9: v in W;
consider v1 be continuous RealMap of X such that
A10: v1=v by A9;
A11:-v1 is continuous RealMap of X by PSCOMP_1:9;
reconsider h = -v, v2 = v as Element of Funcs(the carrier of X,REAL);
A12:h=(-1)*v by A1,RLVECT_1:16;
A13:ex f being Function st
h = f & dom f = the carrier of X & rng f c= REAL by FUNCT_2:def 2;
A14: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;
h.x = (-1)*(v2.y) by A12,FUNCSDOM:4;
hence h.x = -v1.x by A10;
end;
then -v=-v1 by A14,A13,VALUED_1:9;
hence -v in W by A11;
end;
then
A15:W is having-inverse;
for a be Real, u be Element of V st u in W holds a * u in W
proof
let a be Real, u be Element of V such that
A16: u in W;
consider u1 be continuous RealMap of X such that
A17: u1=u by A16;
A18:a(#)u1 is continuous RealMap of X
proof
reconsider U = u1 as continuous Function of X,R^1
by JORDAN5A:27,TOPMETR:17;
set c = the carrier of X;
consider H being Function of X,R^1 such that
A19: for p being Point of X
for r1 being Real st U . p = r1 holds
H . p = a * r1 and
A20: H is continuous by JGRAPH_2:23;
reconsider h = H as RealMap of X by TOPMETR:17;
A21: dom h = the carrier of X by FUNCT_2:def 1
.= dom u1 by FUNCT_2:def 1;
for c being object st c in dom h holds
h . c = a * (u1 . c) by A19;
then h = a (#) u1 by A21,VALUED_1:def 5;
hence a (#) u1 is continuous RealMap of X by A20,JORDAN5A:27;
end;
reconsider h = a*u as Element of Funcs(the carrier of X,REAL);
A22:ex f being Function st
h = f & dom f = the carrier of X & rng f c= REAL by FUNCT_2:def 2;
A23: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 A17,FUNCSDOM:4;
then
a*u=a(#)u1 by A23,A22,VALUED_1:def 5;
hence a*u in W by A18;
end;
hence ContinuousFunctions(X) is additively-linearly-closed
by A8,A15;
A24: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
A25: v in W & u in W;
consider v1 be continuous RealMap of X such that
A26: v1=v by A25;
consider u1 be continuous RealMap of X such that
A27: u1=u by A25;
A28:v1(#)u1 is continuous RealMap of X
proof
reconsider V = v1, U = u1 as continuous Function of X,R^1
by JORDAN5A:27,TOPMETR:17;
consider H being Function of X,R^1 such that
A29: for p being Point of X
for r1, r2 being Real st V . p = r1 & U . p = r2 holds
H . p = r1 * r2 and
A30: H is continuous by JGRAPH_2:25;
reconsider h = H as RealMap of X by TOPMETR:17;
A31: dom h = (the carrier of X) /\ (the carrier of X) by FUNCT_2:def 1
.= (the carrier of X) /\ (dom u1) by FUNCT_2:def 1
.= (dom v1) /\ (dom u1) by FUNCT_2:def 1;
for c being object st c in dom h holds
h . c = (v1 . c) * (u1 . c) by A29;
then h = v1 (#) u1 by A31,VALUED_1:def 4;
hence v1 (#) u1 is continuous RealMap of X by A30,JORDAN5A:27;
end;
reconsider h = v*u as Element of Funcs(the carrier of X,REAL);
A32:ex f being Function st
h = f & dom f = the carrier of X & rng f c= REAL by FUNCT_2:def 2;
dom v1 /\ dom u1 = (the carrier of X) /\ dom u1 by FUNCT_2:def 1;
then
A33: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 A26,A27,FUNCSDOM:2; then
v*u=v1(#)u1 by A33,A32,VALUED_1:def 4;
hence v*u in W by A28;
end;
reconsider g = RealFuncUnit the carrier of X as RealMap of X;
g = X --> 1;
then 1.V in W;
hence thesis by A24;
end;
end;
definition
let X be non empty TopSpace;
func R_Algebra_of_ContinuousFunctions(X) -> AlgebraStr equals
AlgebraStr (# ContinuousFunctions(X),
mult_(ContinuousFunctions(X),RAlgebra the carrier of X),
Add_(ContinuousFunctions(X),RAlgebra the carrier of X),
Mult_(ContinuousFunctions(X),RAlgebra the carrier of X),
One_(ContinuousFunctions(X),RAlgebra the carrier of X),
Zero_(ContinuousFunctions(X),RAlgebra the carrier of X) #);
coherence;
end;
theorem
for X being non empty TopSpace holds
R_Algebra_of_ContinuousFunctions(X)
is Subalgebra of RAlgebra the carrier of X by C0SP1:6;
registration
let X be non empty TopSpace;
cluster R_Algebra_of_ContinuousFunctions(X) -> strict non empty;
coherence;
end;
registration
let X be non empty TopSpace;
cluster R_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 R_Algebra_of_ContinuousFunctions(X);
reconsider v1=v as VECTOR of RAlgebra the carrier of X by TARSKI:def 3;
R_Algebra_of_ContinuousFunctions(X)
is Subalgebra of RAlgebra the carrier of X by C0SP1:6;
then
1 * v = 1*v1 by C0SP1:8;
hence 1 * v =v by FUNCSDOM:12;
end;
hence thesis by C0SP1:6;
end;
end;
theorem Th3:
for X being non empty TopSpace
for F,G,H being VECTOR of R_Algebra_of_ContinuousFunctions(X)
for f,g,h being RealMap of X holds
(f=F & g=G & h=H implies ( H = F+G iff (for x be 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 R_Algebra_of_ContinuousFunctions(X);
let f,g,h be RealMap of X;
assume
A1: f=F & g=G & h=H;
A2:R_Algebra_of_ContinuousFunctions(X) is
Subalgebra of RAlgebra the carrier of X by C0SP1:6;
reconsider f1=F, g1=G, h1=H as VECTOR of
RAlgebra 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,C0SP1:8;
hence h.x = f.x+g.x by A1,FUNCSDOM:1;
end;
assume for x be Element of X holds h.x = f.x+g.x;
then h1=f1+g1 by A1,FUNCSDOM:1;
hence H =F+G by A2,C0SP1:8;
end;
theorem Th4:
for X being non empty TopSpace
for F,G,H being VECTOR of R_Algebra_of_ContinuousFunctions(X)
for f,g,h being RealMap of X
for a being Real
holds
(f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x ))
proof
let X be non empty TopSpace;
let F,G,H be VECTOR of R_Algebra_of_ContinuousFunctions(X);
let f,g,h be RealMap of X;
let a be Real;
assume
A1: f=F & g=G;
A2:R_Algebra_of_ContinuousFunctions(X) is
Subalgebra of RAlgebra the carrier of X by C0SP1:6;
reconsider f1=F, g1=G as VECTOR of
RAlgebra 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,C0SP1:8;
hence g.x=a*f.x by A1,FUNCSDOM:4;
end;
assume for x be Element of the carrier of X holds g.x=a*f.x;
then g1=a*f1 by A1,FUNCSDOM:4;
hence G =a*F by A2,C0SP1:8;
end;
theorem Th5:
for X being non empty TopSpace
for F,G,H being VECTOR of R_Algebra_of_ContinuousFunctions(X)
for f,g,h being RealMap of X holds
(f=F & g=G & h=H implies ( H = F*G iff (for x be 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 R_Algebra_of_ContinuousFunctions(X);
let f,g,h be RealMap of X;
assume
A1: f=F & g=G & h=H;
A2:R_Algebra_of_ContinuousFunctions(X) is
Subalgebra of RAlgebra the carrier of X by C0SP1:6;
reconsider f1=F, g1=G, h1=H as VECTOR of
RAlgebra 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,C0SP1:8;
hence h.x = f.x * g.x by A1,FUNCSDOM:2;
end;
assume for x be Element of X holds h.x = f.x * g.x;
then
h1 = f1 * g1 by A1,FUNCSDOM:2;
hence H = F * G by A2,C0SP1:8;
end;
theorem Th6:
for X being non empty TopSpace holds
0.R_Algebra_of_ContinuousFunctions(X) = X --> 0
proof
let X be non empty TopSpace;
A1:R_Algebra_of_ContinuousFunctions(X)
is Subalgebra of RAlgebra the carrier of X by C0SP1:6;
0.RAlgebra the carrier of X = X --> 0;
hence thesis by A1,C0SP1:8;
end;
theorem Th7:
for X being non empty TopSpace holds
1_R_Algebra_of_ContinuousFunctions(X) = X --> 1
proof
let X be non empty TopSpace;
A1:R_Algebra_of_ContinuousFunctions(X)
is Subalgebra of RAlgebra the carrier of X by C0SP1:6;
1_RAlgebra the carrier of X = X --> 1;
hence thesis by A1,C0SP1:8;
end;
theorem Th8:
for A being Algebra, A1,A2 being Subalgebra of A holds
the carrier of A1 c= the carrier of A2 implies A1 is Subalgebra of A2
proof
let A be Algebra, A1,A2 be Subalgebra 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 C0SP1:def 9;
A3:the addF of A1 = (the addF of A2)||the carrier of A1
proof
the addF of A1 = AA||CA1 & the addF of A2 = AA||CA2 &
[:CA1,CA1:] c= [:CA2,CA2:] by A1,C0SP1:def 9,ZFMISC_1:96;
hence thesis by FUNCT_1:51;
end;
A4:the multF of A1 = (the multF of A2)||the carrier of A1
proof
the multF of A1 = mA||CA1 & the multF of A2 = mA||CA2 &
[:CA1,CA1:] c= [:CA2,CA2:] by A1,C0SP1:def 9,ZFMISC_1:96;
hence thesis by FUNCT_1:51;
end;
the Mult of A1 = (the Mult of A2) | [:REAL,CA1:]
proof
the Mult of A1 = MA|[:REAL,CA1:] & the Mult of A2 = MA|[:REAL,CA2:] &
[:REAL,CA1:] c= [:REAL,CA2:] by A1,C0SP1:def 9,ZFMISC_1:96;
hence thesis by FUNCT_1:51;
end;
hence thesis by A1,A2,A3,A4,C0SP1:def 9;
end;
Lm1:
for X being compact non empty TopSpace
for x being set st x in ContinuousFunctions(X) holds
x in BoundedFunctions the carrier of X
proof
let X be compact non empty TopSpace;
let x be set;
assume x in ContinuousFunctions(X);
then
consider h be continuous RealMap of X such that
A1: x=h;
A2:h is bounded_above & h is bounded_below by SEQ_2:def 8; then
consider r1 being Real such that
A3: for y being object st y in dom h holds h.y < r1 by SEQ_2:def 1;
A4:(the carrier of X) /\ dom h c= dom h by XBOOLE_1:17; then
for y being object st y in (the carrier of X) /\ dom h holds h.y<=r1 by A3;
then
A5:h|(the carrier of X) is bounded_above by RFUNCT_1:70;
consider r2 being Real such that
A6:for y being object st y in dom h holds r2<h.y by A2,SEQ_2:def 2;
for y being object st y in (the carrier of X) /\ dom h holds
r2<=h.y by A4,A6;
then
A7:h|(the carrier of X) is bounded_below by RFUNCT_1:71;
(the carrier of X ) /\ (the carrier of X ) =(the carrier of X );
then
h|(the carrier of X ) is bounded by A5,A7,RFUNCT_1:75;
hence x in BoundedFunctions the carrier of X by A1;
end;
theorem
for X being compact non empty TopSpace holds
(R_Algebra_of_ContinuousFunctions(X) is
Subalgebra of R_Algebra_of_BoundedFunctions the carrier of X)
proof
let X be compact non empty TopSpace;
A1:the carrier of R_Algebra_of_ContinuousFunctions(X)
c= the carrier of R_Algebra_of_BoundedFunctions the carrier of X
by Lm1;
A2:R_Algebra_of_ContinuousFunctions(X) is
Subalgebra of RAlgebra (the carrier of X) by C0SP1:6;
R_Algebra_of_BoundedFunctions the carrier of X is
Subalgebra of RAlgebra (the carrier of X) by C0SP1:10;
hence thesis by A1,A2,Th8;
end;
definition
let X be compact non empty TopSpace;
func ContinuousFunctionsNorm(X) -> Function of (ContinuousFunctions(X)),REAL
equals
(BoundedFunctionsNorm the carrier of X)|(ContinuousFunctions(X));
correctness
proof
for x being object st x in ContinuousFunctions(X) holds
x in BoundedFunctions the carrier of X by Lm1;
then
ContinuousFunctions(X) c= BoundedFunctions the carrier of X;
hence thesis by FUNCT_2:32;
end;
end;
definition
let X be compact non empty TopSpace;
func R_Normed_Algebra_of_ContinuousFunctions(X) -> Normed_AlgebraStr equals
Normed_AlgebraStr (# ContinuousFunctions(X),
mult_(ContinuousFunctions(X),RAlgebra the carrier of X),
Add_(ContinuousFunctions(X),RAlgebra the carrier of X),
Mult_(ContinuousFunctions(X),RAlgebra the carrier of X),
One_(ContinuousFunctions(X),RAlgebra the carrier of X),
Zero_(ContinuousFunctions(X),RAlgebra the carrier of X),
ContinuousFunctionsNorm(X) #);
correctness;
end;
registration
let X be compact non empty TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> strict non empty;
correctness;
end;
Lm2:
now
let X be compact non empty TopSpace;
set F = R_Normed_Algebra_of_ContinuousFunctions(X);
let x,e be Element of F;
assume
A1: e = One_(ContinuousFunctions(X),RAlgebra the carrier of X);
set X1 = ContinuousFunctions(X);
reconsider f = x as Element of X1;
1_RAlgebra the carrier of X = X-->1
.= 1_R_Algebra_of_ContinuousFunctions(X) by Th7;
then
A2:[f,1_RAlgebra the carrier of X] in [:X1,X1:] &
[1_RAlgebra the carrier of X,f] in [:X1,X1:] by ZFMISC_1:87;
x * e = (mult_(X1,RAlgebra the carrier of X))
.(f,1_RAlgebra the carrier of X) by A1,C0SP1:def 8;
then
x * e = ((the multF of RAlgebra the carrier of X)||X1)
.(f,1_RAlgebra the carrier of X) by C0SP1:def 6;
then
x * e = f * 1_RAlgebra the carrier of X by A2,FUNCT_1:49;
hence x * e = x;
e * x = (mult_(X1,RAlgebra the carrier of X))
.(1_RAlgebra the carrier of X,f) by A1,C0SP1:def 8;
then
e * x = ((the multF of RAlgebra the carrier of X)||X1)
.(1_RAlgebra the carrier of X,f) by C0SP1:def 6;
then
e * x = (1_RAlgebra the carrier of X )* f by A2,FUNCT_1:49;
hence e * x = x;
end;
registration
let X be compact non empty TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> unital;
correctness
proof
reconsider e = One_(ContinuousFunctions(X), RAlgebra the carrier of X) as
Element of R_Normed_Algebra_of_ContinuousFunctions(X);
take e;
thus thesis by Lm2;
end;
end;
theorem Th10:
for W be Normed_AlgebraStr, V be Algebra st
the AlgebraStr of W = V holds W is Algebra
proof
let W be Normed_AlgebraStr,V be Algebra such that
A1: the AlgebraStr of W = V;
reconsider W as non empty AlgebraStr by A1;
A2:for x,y being VECTOR of W holds x + y = y + x
proof
let x,y be VECTOR of W;
reconsider x1 = x, y1 = y as VECTOR of V by A1;
x + y = x1+y1 by A1;
then
x + y =y1 + x1;
hence x + y = y + x by A1;
end;
A3:for x,y,z being VECTOR of W holds (x + y) + z = x + (y + z)
proof
let x,y,z be VECTOR of W;
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1;
(x + y) + z = (x1 + y1) + z1 by A1;
then
(x + y) + z = x1 + (y1 + z1) by RLVECT_1:def 3;
hence (x + y) + z = x + (y + z) by A1;
end;
A4:for x being VECTOR of W holds x + 0.W = x
proof
let x be VECTOR of W;
reconsider y = x as VECTOR of V by A1;
x + 0.W = y + 0.V by A1;
hence x + 0.W = x by RLVECT_1:4;
end;
A5:for x being Element of W holds x is right_complementable
proof
let x be Element of W;
reconsider x1 = x as Element of V by A1;
consider v be Element of V such that
A6: x1 + v = 0.V by ALGSTR_0:def 11;
reconsider y = v as Element of W by A1;
x + y = 0.W by A6,A1;
hence thesis;
end;
A7:for v,w being Element of W holds v * w = w * v
proof
let v,w be Element of W;
reconsider v1 = v, w1 = w as Element of V by A1;
v * w = v1*w1 by A1; then
v * w = w1*v1;
hence v * w =w*v by A1;
end;
A8:for a,b,x being Element of W holds (a * b) * x = a * (b * x)
proof
let a,b,x be Element of W;
reconsider y = x, a1 = a, b1 = b as Element of V by A1;
(a * b) * x = (a1 * b1) * y by A1; then
(a * b) * x = a1 * (b1 * y) by GROUP_1:def 3;
hence (a * b) * x = a * (b * x) by A1;
end;
A9:W is right_unital
proof
let x be Element of W;
reconsider x1 = x as Element of V by A1;
x*1.W = x1*1.V by A1;
hence x*1.W = x;
end;
A10:W is right-distributive
proof
let x,y,z being Element of W;
reconsider x1 = x, y1 = y, z1 = z as Element of V by A1;
x*(y+z) = x1*(y1+z1) by A1; then
x*(y+z) = x1*y1 + x1*z1 by VECTSP_1:def 2;
hence x*(y+z) = x*y + x*z by A1;
end;
W is vector-distributive scalar-distributive scalar-associative
vector-associative
proof
thus W is vector-distributive
proof
let a be Real;
let x,y be Element of W;
reconsider x1 = x, y1 = y as Element of V by A1;
a*(x+y) = a*(x1+y1) by A1; then
a*(x+y) = a*x1 + a*y1 by RLVECT_1:def 5;
hence a*(x+y) = a*x + a*y by A1;
end;
thus W is scalar-distributive
proof
let a,b be Real;
let x be Element of W;
reconsider x1 = x as Element of V by A1;
(a+b)*x = (a+b)*x1 by A1; then
(a+b)*x = a*x1 + b*x1 by RLVECT_1:def 6;
hence (a+b)*x =a*x + b*x by A1;
end;
thus W is scalar-associative
proof
let a,b be Real;
let x being Element of W;
reconsider x1 = x as Element of V by A1;
(a*b)*x = (a*b)*x1 by A1; then
(a*b)*x = a*(b*x1) by RLVECT_1:def 7;
hence (a*b)*x = a*(b*x) by A1;
end;
let x,y be Element of W;
let a be Real;
reconsider x1 = x, y1 = y as Element of V by A1;
a*(x*y) = a*(x1*y1) by A1; then
a*(x*y) = (a*x1)*y1 by FUNCSDOM:def 9;
hence a*(x*y) = (a*x)*y by A1;
end;
hence thesis by A2,A3,A4,A5,A7,A8,A9,A10,ALGSTR_0:def 16,GROUP_1:def 3,def 12
,RLVECT_1:def 2,def 3,def 4;
end;
Lm3:
for X being compact non empty TopSpace
for x be Point of R_Normed_Algebra_of_ContinuousFunctions(X),
y be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X
st x=y holds ||.x.||= ||.y.|| by FUNCT_1:49;
Lm4:
for X being compact non empty TopSpace
for x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions(X),
y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X
st x1=y1 & x2=y2 holds x1+x2=y1+y2
proof
let X be compact non empty TopSpace;
let x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions(X),
y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions
the carrier of X;
assume A1: x1=y1 & x2=y2;
thus x1+x2 = ((the addF of RAlgebra the carrier of X)
||(ContinuousFunctions(X))).([x1,x2]) by C0SP1:def 5
.= (the addF of RAlgebra the carrier of X).([x1,x2]) by FUNCT_1:49
.= ((the addF of RAlgebra the carrier of X)
||(BoundedFunctions the carrier of X)).([y1,y2]) by A1,FUNCT_1:49
.=y1+y2 by C0SP1:def 5;
end;
Lm5:
for X being compact non empty TopSpace
for a be Real,
x be Point of R_Normed_Algebra_of_ContinuousFunctions(X),
y be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X
st x=y holds a*x=a*y
proof
let X be compact non empty TopSpace;
let a be Real,
x be Point of R_Normed_Algebra_of_ContinuousFunctions(X),
y be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume
A1: x=y;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
thus a*x = ((the Mult of RAlgebra the carrier of X)|
[:REAL,(ContinuousFunctions(X)):]).([a,x]) by C0SP1:def 11
.= (the Mult of RAlgebra the carrier of X).([aa,x]) by FUNCT_1:49
.= ((the Mult of RAlgebra the carrier of X)
|[:REAL,(BoundedFunctions the carrier of X):]). [aa,y] by A1,FUNCT_1:49
.=a*y by C0SP1:def 11;
end;
Lm6:
for X be compact non empty TopSpace
for x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions(X),
y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X
st x1=y1 & x2=y2 holds x1*x2=y1*y2
proof
let X be compact non empty TopSpace;
let x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions(X),
y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume
A1: x1=y1 & x2=y2;
thus x1*x2 = ((the multF of RAlgebra the carrier of X)||
(ContinuousFunctions(X))).([x1,x2]) by C0SP1:def 6
.= (the multF of RAlgebra the carrier of X).([x1,x2]) by FUNCT_1:49
.= ((the multF of RAlgebra the carrier of X)
||(BoundedFunctions the carrier of X)).([y1,y2]) by A1,FUNCT_1:49
.=y1*y2 by C0SP1:def 6;
end;
registration
let X be compact non empty TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions(X) ->
Abelian add-associative right_zeroed right_complementable
commutative associative right_unital right-distributive
vector-distributive scalar-distributive scalar-associative
vector-associative;
coherence
proof
1.(R_Normed_Algebra_of_ContinuousFunctions(X))
= 1_R_Algebra_of_ContinuousFunctions(X);
hence thesis by Th10;
end;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem Th11:
for X being compact non empty TopSpace
for F being Point of R_Normed_Algebra_of_ContinuousFunctions(X) holds
(Mult_(ContinuousFunctions(X), RAlgebra the carrier of X)).(1,F) = F
proof
let X be compact non empty TopSpace;
let F be Point of R_Normed_Algebra_of_ContinuousFunctions(X);
set X1 = ContinuousFunctions(X);
reconsider f1 = F as Element of X1;
A1:[jj,f1] in [:REAL,X1:];
thus (Mult_(ContinuousFunctions(X), RAlgebra the carrier of X)).(1,F)
= ((the Mult of RAlgebra the carrier of X)| [:REAL,X1:]).(1,f1)
by C0SP1:def 11
.= (the Mult of RAlgebra the carrier of X).(1,f1) by A1,FUNCT_1:49
.= F by FUNCSDOM:12;
end;
registration
let X be compact non empty TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> vector-distributive
scalar-distributive scalar-associative scalar-unital;
coherence
by Th11;
end;
theorem Th12:
for X being compact non empty TopSpace holds
X --> 0 = 0.R_Normed_Algebra_of_ContinuousFunctions(X)
proof
let X be compact non empty TopSpace;
X-->0 = 0.R_Algebra_of_ContinuousFunctions(X) by Th6;
hence thesis;
end;
Lm7:
for X being compact non empty TopSpace holds
0.R_Normed_Algebra_of_ContinuousFunctions(X)
= 0.R_Normed_Algebra_of_BoundedFunctions the carrier of X
proof
let X be compact non empty TopSpace;
thus 0.R_Normed_Algebra_of_ContinuousFunctions(X) = X-->0 by Th12
.= 0.R_Normed_Algebra_of_BoundedFunctions the carrier of X by C0SP1:25;
end;
Lm8:
for X being compact non empty TopSpace holds
1.R_Normed_Algebra_of_ContinuousFunctions(X)
= 1.R_Normed_Algebra_of_BoundedFunctions the carrier of X
proof
let X be compact non empty TopSpace;
thus 1.R_Normed_Algebra_of_ContinuousFunctions(X)
=1_R_Algebra_of_ContinuousFunctions(X)
.= X-->1 by Th7
.= 1_R_Algebra_of_BoundedFunctions the carrier of X by C0SP1:16
.= 1.R_Normed_Algebra_of_BoundedFunctions the carrier of X;
end;
theorem
for X be compact non empty TopSpace
for F be Point of R_Normed_Algebra_of_ContinuousFunctions(X)
holds 0 <= ||.F.||
proof
let X be compact non empty TopSpace;
let F be Point of R_Normed_Algebra_of_ContinuousFunctions(X);
reconsider F1=F as Point of
R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
||.F.|| =||.F1.|| by FUNCT_1:49;
hence thesis by C0SP1:27;
end;
theorem
for X being compact non empty TopSpace
for F be Point of R_Normed_Algebra_of_ContinuousFunctions(X) holds
F = 0.R_Normed_Algebra_of_ContinuousFunctions(X) implies 0 = ||.F.||
proof
let X be compact non empty TopSpace;
let F be Point of R_Normed_Algebra_of_ContinuousFunctions(X);
assume
A1: F = 0.R_Normed_Algebra_of_ContinuousFunctions(X);
reconsider F1=F as Point of
R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
A2:||.F.|| =||.F1.|| by FUNCT_1:49;
F= X--> 0 by A1,Th12; then
F1 = 0.R_Normed_Algebra_of_BoundedFunctions the carrier of X by C0SP1:25;
hence thesis by A2,C0SP1:28;
end;
theorem Th15:
for X being compact non empty TopSpace
for F,G,H being Point of R_Normed_Algebra_of_ContinuousFunctions(X)
for f,g,h be RealMap of X
holds
(f=F & g=G & h=H implies
(H = F+G iff for x be Element of X holds h.x = f.x + g.x))
proof
let X be compact non empty TopSpace;
let F,G,H be Point of R_Normed_Algebra_of_ContinuousFunctions(X);
let f,g,h be RealMap of X;
reconsider f1=F, g1=G, h1=H as VECTOR of R_Algebra_of_ContinuousFunctions(X);
H=F+G iff h1=f1+g1;
hence thesis by Th3;
end;
theorem
for a be Real
for X being compact non empty TopSpace
for F,G being Point of R_Normed_Algebra_of_ContinuousFunctions(X)
for f,g being RealMap of X holds
(f=F & g=G implies ( G = a*F iff for x be Element of X holds g.x = a*f.x ))
proof
let a be Real;
let X be compact non empty TopSpace;
let F,G be Point of R_Normed_Algebra_of_ContinuousFunctions(X);
let f,g be RealMap of X;
reconsider f1=F, g1=G as VECTOR of R_Algebra_of_ContinuousFunctions(X);
G=a*F iff g1=a*f1;
hence thesis by Th4;
end;
theorem
for X being compact non empty TopSpace
for F,G,H being Point of R_Normed_Algebra_of_ContinuousFunctions(X)
for f,g,h being RealMap of X holds
(f=F & g=G & h=H implies
(H = F*G iff for x be Element of X holds h.x = f.x * g.x))
proof
let X be compact non empty TopSpace;
let F,G,H be Point of R_Normed_Algebra_of_ContinuousFunctions(X);
let f,g,h be RealMap of X;
reconsider f1=F, g1=G, h1=H as VECTOR of R_Algebra_of_ContinuousFunctions(X);
H=F*G iff h1=f1*g1;
hence thesis by Th5;
end;
theorem Th18:
for a being Real
for X being compact non empty TopSpace
for F,G being Point of R_Normed_Algebra_of_ContinuousFunctions(X) holds
( ||.F.|| = 0 iff F = 0.R_Normed_Algebra_of_ContinuousFunctions(X)) &
(||.a*F.|| = |.a.| * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||)
proof
let a be Real;
let X be compact non empty TopSpace;
let F,G be Point of R_Normed_Algebra_of_ContinuousFunctions(X);
reconsider F1=F, G1=G as Point of
R_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;
||.F1.|| = 0 iff
F1=0.R_Normed_Algebra_of_BoundedFunctions the carrier of X by C0SP1:32;
hence ||.F.|| = 0 iff F = 0.R_Normed_Algebra_of_ContinuousFunctions(X)
by Lm7,FUNCT_1:49;
thus ||.a*F.|| = ||.a*F1.|| by Lm5,Lm3
.=|.a.| * ||.F1.|| by C0SP1:32
.=|.a.| * ||.F.|| by FUNCT_1:49;
thus ||.F+G.|| <= ||.F.|| + ||.G.|| by A1,A2,A3,C0SP1:32;
end;
registration
let X be compact non empty TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions(X) ->
reflexive discerning RealNormSpace-like;
coherence
proof set R = R_Normed_Algebra_of_ContinuousFunctions(X);
thus ||.0.R.|| = 0 by Th18;
for x,y being Point of R_Normed_Algebra_of_ContinuousFunctions(X)
for a be Real holds
( ||.x.|| = 0 iff x = 0.R_Normed_Algebra_of_ContinuousFunctions(X) ) &
||.a*x.|| = |.a.| * ||.x.|| &
||.x+y.|| <= ||.x.|| + ||.y.|| by Th18;
hence thesis by NORMSP_1:def 1;
end;
end;
Lm9:
for X be compact non empty TopSpace
for x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions(X),
y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X
st x1=y1 & x2=y2 holds x1-x2=y1-y2
proof
let X be compact non empty TopSpace;
let x1,x2 be Point of R_Normed_Algebra_of_ContinuousFunctions(X),
y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume
A1: x1=y1 & x2=y2;
-x2=(-1)*x2 by RLVECT_1:16
.=(-1)*y2 by A1,Lm5
.= -y2 by RLVECT_1:16;
hence x1-x2 =y1-y2 by A1,Lm4;
end;
theorem
for X be compact non empty TopSpace
for F,G,H be Point of R_Normed_Algebra_of_ContinuousFunctions(X)
for f,g,h be RealMap of X holds
f=F & g=G & h=H implies
(H = F-G iff (for x be Element of X holds h.x = f.x - g.x))
proof
let X be compact non empty TopSpace;
let F,G,H be Point of R_Normed_Algebra_of_ContinuousFunctions(X);
let f,g,h be RealMap of 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.R_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,Th15;
hence f.x-g.x=h.x;
end;
hence for x be Element of X holds h.x = f.x - g.x;
end;
now assume
A4: for x be 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,Th15; then
F-G=H+(G-G) by RLVECT_1:def 3; then
F-G=H+0.R_Normed_Algebra_of_ContinuousFunctions(X) by RLVECT_1:15;
hence F-G=H by RLVECT_1:4;
end;
hence thesis by A2;
end;
theorem Th20:
for X be RealBanachSpace, Y be Subset of X, seq be sequence of X st
Y is closed & rng seq c= Y & seq is Cauchy_sequence_by_Norm holds
seq is convergent & lim seq in Y
by LOPBAN_1:def 15,NFCONT_1:def 3;
theorem Th21:
for X be compact non empty TopSpace
for Y be Subset of R_Normed_Algebra_of_BoundedFunctions the carrier of X st
Y = ContinuousFunctions(X) holds Y is closed
proof
let X be compact non empty TopSpace;
let Y be Subset of R_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume
A1: Y = ContinuousFunctions(X);
now let seq be sequence of
R_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume
A2: rng seq c= Y & seq is convergent;
lim seq in BoundedFunctions the carrier of X;
then
consider f be Function of (the carrier of X),REAL such that
A3: f=lim seq & f|(the carrier of X) is bounded;
now let z be object;
assume z in BoundedFunctions (the carrier of X); then
ex f be RealMap of X st f=z & f|(the carrier of X) is bounded;
hence z in PFuncs(the carrier of X,REAL) by PARTFUN1:45;
end; then
BoundedFunctions (the carrier of X) c= PFuncs(the carrier of X,REAL); then
reconsider H = seq as Functional_Sequence of (the carrier of X),REAL
by FUNCT_2:7;
A4: for p be Real st p>0 ex k be Element of NAT st
for n be Element of NAT, x be 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 be Nat such that
A5: for n be Nat st n >= k holds
||.seq.n - lim seq.|| < p by A2,NORMSP_1:def 7;
reconsider k as Element of NAT by ORDINAL1:def 12;
take k;
hereby let n be Element of NAT, 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 BoundedFunctions the carrier of X; then
consider g be RealMap of X such that
A8: g=seq.n - lim seq & g|(the carrier of X) is bounded;
seq.n in BoundedFunctions the carrier of X; then
consider s be RealMap of X 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,C0SP1:34;
|.g.x0.| <= ||.seq.n - lim seq.|| by A8,C0SP1:26;
hence |.(H.n).x - f.x.| < p by A10,A9,A7,XXREAL_0:2;
end;
end;
f is continuous
proof
for x being Point of X,V being Subset of REAL 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,V be Subset of REAL;
set r=f.x;
assume f.x in V & V is open;
then
consider r0 being Real such that
A11: 0<r0 & ].r-r0,r+r0.[ c= V by RCOMP_1:19;
consider k being Element of NAT such that
A12: for n be Element of NAT,x be set st n>=k & x in the carrier of X
holds |.(H.n).x - f.x.| < r0/3 by A4,A11,XREAL_1:222;
A13: |.(H.k).x - f.x.| < r0/3 by A12;
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 be continuous RealMap of X such that
A14: H.k=h by A1;
set r1 = h.x;
set G1 = ]. r1-r0/3,r1+r0/3 .[;
A15: r1<r1+r0/3 by A11,XREAL_1:29,222; then
r1-r0/3<r1 by XREAL_1:19; then
h.x in G1 by A15; then
consider W1 being Subset of X such that
A16: x in W1 & W1 is open & h.:W1 c= G1 by Th1;
now let x0 be object;
assume x0 in f.:W1; then
consider z0 being object such that
A17: z0 in dom f & z0 in W1 & f.z0=x0 by FUNCT_1:def 6;
h.z0 in h.:W1 by A17,FUNCT_2:35;
then h.x - r0/3 < h.z0 & h.z0 < h.x + r0/3 by A16,XXREAL_1:4;
then h.x-r0/3 -h.x < h.z0-h.x & h.z0 - h.x < h.x + r0/3 -h.x
by XREAL_1:9;
then
A18: |.h.z0 - h.x.| <= r0/3 by ABSVALUE:5;
A19: |.-(h.x - f.x).| < r0/3 by A13,A14,COMPLEX1:52;
|.h.z0 - f.z0.| < r0/3 by A17,A12,A14; then
|.-(h.z0 - f.z0).| < r0/3 by COMPLEX1:52; then
|.f.z0 - h.z0.|+|.f.x - h.x.| < r0/3 + r0/3 by A19,XREAL_1:8;
then
A20: |.f.z0 - h.z0.|+|.f.x - h.x.|+|.h.z0 - h.x.|
< r0/3 + r0/3 + r0/3 by A18,XREAL_1:8;
|. f.z0 -f.x .| = |.(f.z0 - h.z0)- (f.x - h.x) +(h.z0-h.x).|;
then
A21: |. f.z0 -f.x .| <= |.(f.z0 - h.z0)- (f.x - h.x).|
+|.h.z0-h.x.| by COMPLEX1:56;
|.(f.z0 - h.z0)- (f.x - h.x).|
<= |.f.z0 - h.z0.| + |.f.x - h.x.| by COMPLEX1:57;
then
|.(f.z0 - h.z0)- (f.x - h.x).|+|.h.z0-h.x.|
<= |.f.z0 - h.z0.| + |.f.x - h.x.| +|.h.z0-h.x.| by XREAL_1:6;
then
|. f.z0 -f.x .| <= |.f.z0 - h.z0.|+|.f.x - h.x.|
+|.h.z0-h.x.| by A21,XXREAL_0:2; then
|. f.z0 -f.x .| <r0 by A20,XXREAL_0:2; then
-r0<f.z0 -f.x & f.z0 -f.x <r0 by SEQ_2:1; then
-r0 + r < f.z0 -r + r & f.z0 - r + r <r0 + r by XREAL_1:6;
hence x0 in ].r-r0,r+r0.[ by A17;
end; then
f.:W1 c= ].r-r0,r+r0.[;
hence ex W being Subset of X st x in W & W is open & f.:W c= V
by A16,A11,XBOOLE_1:1;
end;
hence thesis by Th1;
end;
hence lim seq in Y by A3,A1;
end;
hence thesis by NFCONT_1:def 3;
end;
theorem Th22:
for X be compact non empty TopSpace
for seq be sequence of R_Normed_Algebra_of_ContinuousFunctions(X) st
seq is Cauchy_sequence_by_Norm holds seq is convergent
proof
let X be compact non empty TopSpace;
let vseq be sequence of R_Normed_Algebra_of_ContinuousFunctions(X);
assume
A1: vseq is Cauchy_sequence_by_Norm;
A2:for x being object st x in ContinuousFunctions(X) holds
x in BoundedFunctions the carrier of X by Lm1;
then
ContinuousFunctions(X) c= BoundedFunctions the carrier of X;
then rng vseq c= BoundedFunctions the carrier of X;
then reconsider vseq1=vseq as sequence of
R_Normed_Algebra_of_BoundedFunctions the carrier of X by FUNCT_2:6;
now let e be Real such that
A3: e >0;
consider k be Nat such that
A4: for n,m be Nat st n >= k & m >= k holds
||. vseq.n - vseq.m .|| < e by A1,A3,RSSPACE3:8;
take k;
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;
then
A5:vseq1 is Cauchy_sequence_by_Norm by RSSPACE3:8;
then
A6: vseq1 is convergent by C0SP1:35;
reconsider Y = ContinuousFunctions(X) as Subset of
R_Normed_Algebra_of_BoundedFunctions the carrier of X by A2,TARSKI:def 3;
A7:rng vseq c= ContinuousFunctions(X);
Y is closed by Th21;
then
reconsider tv=lim vseq1 as Point of
R_Normed_Algebra_of_ContinuousFunctions(X) by A7,A5,Th20;
for e be Real
st e > 0 ex k be Nat st for n be Nat st
n >= k holds ||.vseq.n - tv.|| < e
proof
let e be Real;
assume e > 0;
then
consider k be Nat such that
A8: for n be Nat st n >= k holds
||.vseq1.n - lim vseq1.|| < e by A6,NORMSP_1:def 7;
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 be Nat st n >= k holds ||.vseq.n - tv.|| < e;
end;
hence thesis by NORMSP_1:def 6;
end;
registration
let X be compact non empty TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> complete;
coherence
proof
for seq be sequence of R_Normed_Algebra_of_ContinuousFunctions(X) st
seq is Cauchy_sequence_by_Norm holds seq is convergent by Th22;
hence thesis by LOPBAN_1:def 15;
end;
end;
registration
let X be compact non empty TopSpace;
cluster R_Normed_Algebra_of_ContinuousFunctions(X) -> Banach_Algebra-like;
coherence
proof
set B = R_Normed_Algebra_of_ContinuousFunctions(X);
A1:now let f,g be Element of B;
reconsider f1=f, g1=g as Point of
R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
A2: ||.f.|| =||.f1.|| & ||.g.|| =||.g1.|| & ||.f*g.|| =||.f1*g1.||
by Lm6,Lm3;
thus ||. f*g .|| <= ||.f.|| * ||.g.|| by A2,LOPBAN_2:def 9;
end;
A3:||.(1.B).||=||. 1.R_Normed_Algebra_of_BoundedFunctions the carrier of X.||
by Lm8,Lm3
.= 1 by LOPBAN_2:def 10;
A4:now let a be Real, f,g be Element of B;
reconsider f1=f, g1=g as Point of
R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
A5: a*g1=a*g by Lm5;
A6: f*g=f1*g1 by Lm6;
a*(f*g) =a*(f1*g1) by A6,Lm5;
then
a*(f*g) =f1*(a*g1) by LOPBAN_2:def 11;
hence a*(f*g) =f*(a*g) by A5,Lm6;
end;
now let f,g,h be Element of B;
reconsider f1=f, g1=g, h1=h as Point of
R_Normed_Algebra_of_BoundedFunctions the carrier of X by Lm1;
A7: g+h = g1+h1 by Lm4;
A8:g*f = g1*f1 & h*f = h1*f1 by Lm6;
thus (g+h)*f =(g1+h1)*f1 by Lm6,A7
.= g1*f1 + h1*f1 by VECTSP_1:def 3
.= g*f + h*f by Lm4,A8;
end;
then B is Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3
left-distributive left_unital complete Normed_Algebra
by A1,A3,A4,LOPBAN_2:def 9,def 10,def 11,VECTSP_1:def 3;
hence thesis;
end;
end;
begin :: Some properties of support
theorem Th23:
for X be non empty TopSpace
for f,g be RealMap of X holds
support(f+g) c= support(f) \/ support(g)
proof
let X be non empty TopSpace;
let f,g be RealMap of X;
set CX= the carrier of X;
reconsider h=f+g as RealMap of X;
A1:dom f = CX & dom g = CX & dom h = CX by FUNCT_2:def 1;
now let x be object;
assume A2: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;
A4: (f+g).x = 0 + 0 by A3,VALUED_1:1;
not x in support(f+g) by A4,PRE_POLY:def 7;
hence x in CX\ support(f+g) by A2,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,PRE_POLY:37,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,PRE_POLY:37,XBOOLE_1:28;
hence thesis by A1,PRE_POLY:37,XBOOLE_1:28;
end;
theorem Th24:
for X be non empty TopSpace
for a be Real,f be RealMap of X holds
support(a(#)f) c= support(f)
proof
let X be non empty TopSpace;
let a be Real,f be RealMap of X;
set CX= the carrier of X;
reconsider h=a(#)f as RealMap of X;
now let x be object;
assume x in support(a(#)f); then
(a(#)f).x <>0 by PRE_POLY:def 7; then
A1: a*f.x <> 0 by VALUED_1:6;
f.x <> 0 by A1;
hence x in support(f) by PRE_POLY:def 7;
end;
hence thesis;
end;
theorem
for X be non empty TopSpace
for f,g be RealMap of X holds support(f(#)g) c= support(f) \/ support(g)
proof
let X be non empty TopSpace;
let f,g be RealMap of X;
set CX= the carrier of X;
reconsider h=f(#)g as RealMap of X;
A1: dom f = CX & dom g = CX & dom h = CX by FUNCT_2:def 1;
now let x be object;
assume A2: 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;
A4: (f(#)g).x = 0 * 0 by A3,VALUED_1:5;
not x in support(f(#)g) by A4,PRE_POLY:def 7;
hence x in CX\ support(f(#)g) by A2,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,PRE_POLY:37,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,PRE_POLY:37,XBOOLE_1:28;
hence thesis by A1,PRE_POLY:37,XBOOLE_1:28;
end;
begin :: Space of Real-valued Continuous Functionals with Bounded Support
definition
let X be non empty TopSpace;
func C_0_Functions(X) -> non empty Subset of RealVectSpace the carrier of X
equals
{ f where f is RealMap of 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))};
correctness
proof
A1:{ f where f is RealMap of 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))}
c= Funcs(the carrier of X,REAL)
proof
for x being object
st x in { f where f is RealMap of 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))}
holds x in Funcs(the carrier of X,REAL)
proof
let x be object;
assume x in { f where f is RealMap of 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))};
then
ex f be RealMap of X 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,REAL) by FUNCT_2:8;
end;
hence thesis;
end;
{ f where f is RealMap of 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))}
is non empty
proof
set g= (the carrier of X) --> In(0,REAL);
reconsider g as RealMap of X;
A2: g is continuous
proof
for P being Subset of REAL st P is closed holds g"P is closed
proof
let P being Subset of REAL 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;
A4: 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
A5: A=support(g);
A6: A={}
proof
assume
A7: not thesis;
set p = the Element of support(g);
A8: p in A by A7,A5;
g.p<>0 by A5,A7,PRE_POLY:def 7;
hence contradiction by A8,FUNCOP_1:7;
end;
Cl(A)={}X by A6,PRE_TOPC:22;
hence thesis by XBOOLE_1:2;
end;
thus thesis by A4;
end;
g in { f where f is RealMap of 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 A2,A3;
hence thesis;
end;
hence thesis by A1;
end;
end;
theorem
for X be non empty TopSpace holds
C_0_Functions(X) is non empty Subset of RAlgebra the carrier of X;
Lm10:
for X be non empty TopSpace
for v,u be Element of RAlgebra the carrier of X
st v in C_0_Functions(X) & u in C_0_Functions(X)
holds v + u in C_0_Functions(X)
proof
let X be non empty TopSpace;
set W = C_0_Functions(X);
set V = RAlgebra the carrier of X;
let u,v be Element of V such that
A1: u in W & v in W;
consider u1 be RealMap of X 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 RealMap of X 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 ContinuousFunctions(X) by A2;
A7:v in ContinuousFunctions(X) by A4;
v + u in ContinuousFunctions(X) by A6,A7,IDEAL_1:def 1;
then
consider fvu be continuous RealMap of X such that
A8: v+u = fvu;
A9:Y1 \/ Y2 is compact by A3,A5,COMPTS_1:10;
A10: dom u1 = the carrier of X & dom v1 = the carrier of X by FUNCT_2:def 1;
reconsider A1= support(u1),A2= support(v1) as Subset of X by A10,PRE_POLY:37;
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);
A12:dom (v1+u1) = dom v1 /\ dom u1 by VALUED_1:def 1;
reconsider A1= support(u1),A2= support(v1) as Subset of X by A10,PRE_POLY:37;
reconsider A3= support(v1+u1) as Subset of X by A12,A11,PRE_POLY:37;
Cl(A3) c= Cl(A2 \/ A1) by Th23,PRE_TOPC:19; then
A13:Cl(A3) c= Cl(A2) \/ Cl(A1) by PRE_TOPC:20;
A14: Cl(A1) is Subset of Y1 by A3;
Cl(A2) is Subset of Y2 by A5;
then Cl(A2) \/ Cl(A1) c= Y2 \/ Y1 by A14,XBOOLE_1:13; then
A15:for A3 being Subset of X st A3=support(v1+u1) holds Cl(A3)
is Subset of Y2 \/ Y1 by A13,XBOOLE_1:1;
reconsider vv1=v as Element of Funcs((the carrier of X),REAL);
reconsider uu1=u as Element of Funcs((the carrier of X),REAL);
reconsider fvu1=v+u as Element of Funcs((the carrier of X),REAL);
A16: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 A2,A4,FUNCSDOM:1;
then fvu1 = v1+u1 by A16,A11,VALUED_1:def 1;
hence thesis by A8,A9,A15;
end;
Lm11:
for X be non empty TopSpace
for a be Real,u be Element of RAlgebra the carrier of X
st u in C_0_Functions(X) holds a * u in C_0_Functions(X)
proof
let X be non empty TopSpace;
set W = C_0_Functions(X);
set V = RAlgebra the carrier of X;
let a be Real;
let u be Element of V;
assume
A1: u in W;
consider u1 be RealMap of X 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 ContinuousFunctions(X) by A2;
reconsider aa=a as Real;
aa * u in ContinuousFunctions(X) by A4,C0SP1:def 10; then
consider fau being continuous RealMap of X such that
A5: fau = a*u;
A6: dom u1 = the carrier of X by FUNCT_2:def 1; then
reconsider A1= support(u1) as Subset of X by PRE_POLY:37;
A7:dom u1 = (the carrier of X) by FUNCT_2:def 1;
A8: dom (a(#)u1) = dom u1 by VALUED_1:def 5;
reconsider A1= support(u1) as Subset of X by A6,PRE_POLY:37;
reconsider A3= support(a(#)u1) as Subset of X by A8,A7,PRE_POLY:37;
A9:Cl(A1) is Subset of Y1 by A3;
Cl(A3) c= Cl(A1) by Th24,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),REAL);
reconsider fau1=a*u as Element of Funcs((the carrier of X),REAL);
A11:dom fau1 = the carrier of X by FUNCT_2:def 1;
A12: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,FUNCSDOM:4;
then fau1 = a(#)u1 by A11,A12,VALUED_1:def 5;
hence thesis by A3,A10,A5;
end;
Lm12:
for X be non empty TopSpace
for u be Element of RAlgebra the carrier of X st u in C_0_Functions(X)
holds -u in C_0_Functions(X)
proof
let X be non empty TopSpace;
set W = C_0_Functions(X);
set V = RAlgebra the carrier of X;
let u be Element of V;
assume
A1: u in W;
set a=-1;
RAlgebra the carrier of X is RealLinearSpace by C0SP1:7; then
-u = a*u by RLVECT_1:16;
hence thesis by Lm11,A1;
end;
theorem
for X be non empty TopSpace
for W be non empty Subset of RAlgebra the carrier of X
st W = C_0_Functions(X) holds W is additively-linearly-closed
proof
let X be non empty TopSpace;
let W be non empty Subset of RAlgebra the carrier of X;
assume
A1: W = C_0_Functions(X);
set V = RAlgebra 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;
for a be Real, u be Element of V st u in W holds a * u in W by A1,Lm11;
hence W is additively-linearly-closed by A2,A3;
end;
theorem Th28:
for X be non empty TopSpace holds
C_0_Functions(X) is linearly-closed
proof
let X be non empty TopSpace;
set Y = C_0_Functions(X);
set V = RealVectSpace(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),REAL);
reconsider v2=v, u2=u as VECTOR of RAlgebra the carrier of X;
v2+u2 in Y by A2,Lm10;
hence thesis;
end;
for a be Real, v be Element of V st v in Y holds a * v in Y
proof
let a be Real,v be VECTOR of V;
assume
A3: v in Y;
reconsider v1=v as Element of Funcs((the carrier of X),REAL);
reconsider v2=v as VECTOR of RAlgebra the carrier of X;
a*v2 in Y by A3,Lm11;
hence thesis;
end;
hence thesis by A1,RLSUB_1:def 1;
end;
registration
let X be non empty TopSpace;
cluster C_0_Functions(X) -> non empty linearly-closed;
correctness by Th28;
end;
definition
let X be non empty TopSpace;
func R_VectorSpace_of_C_0_Functions(X) -> RealLinearSpace equals
RLSStruct (# C_0_Functions(X),
Zero_(C_0_Functions(X), RealVectSpace(the carrier of X)),
Add_(C_0_Functions(X), RealVectSpace(the carrier of X)),
Mult_(C_0_Functions(X), RealVectSpace(the carrier of X)) #);
correctness by RSSPACE:11;
end;
theorem
for X be non empty TopSpace holds
R_VectorSpace_of_C_0_Functions(X)
is Subspace of RealVectSpace(the carrier of X) by RSSPACE:11;
theorem Th30:
for X be non empty TopSpace
for x being set st x in C_0_Functions(X) holds
x in BoundedFunctions the carrier of X
proof
let X be non empty TopSpace;
let x be set such that
A1: x in C_0_Functions(X);
consider f be RealMap of X 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;
reconsider Y1 = f.:Y as non empty real-bounded Subset of REAL
by A2,A3,JORDAN_A:1,RCOMP_1:10;
A4:Y1 c= [. inf Y1,sup Y1 .] by XXREAL_2:69;
reconsider r1 = inf Y1, r2 = sup Y1 as Real;
consider r be Real such that
A5: r=|.r1.|+|.r2.|+1;
for p being Element of Y holds r>0 & -r< f.p & f.p <r
proof
let p be Element of Y;
f.p in Y1 by FUNCT_2:35; then
f.p in [.r1,r2.] by A4; then
consider r3 be Real such that
A6: r3=f.p & r1<=r3 & r3<=r2;
A7: |.r1.|>=0 & |.r2.|>=0 by COMPLEX1:46;
-|.r1.| <= r1 by ABSVALUE:4; then
-|.r1.| - |.r2.| <= r1 - 0 by A7,XREAL_1:13; then
-|.r1.| - |.r2.| - 1 < r1 - 0 by XREAL_1:15; then
A8:-r < r1 by A5;
r2 <= |.r2.| by ABSVALUE:4; then
r2 + 0 <= |.r2.|+|.r1.| by A7,XREAL_1:7; then
r2 < r by A5,XREAL_1:8;
hence thesis by A6,A8,XXREAL_0:2;
end;
then consider r be Real such that
A9: for p being Element of Y holds r>0 & -r< f.p & f.p <r;
for x be Point of X holds (-r< f.x & f.x <r)
proof
let x be Point of X;
per cases by XBOOLE_0:def 5;
suppose
A10: x in (the carrier of X) \ Y;
A11: Cl(A) is Subset of Y by A3;
support(f) c= Cl(A) by PRE_TOPC:18; then
support(f) c= Y by A11,XBOOLE_1:1; then
not x in support(f) by A10,XBOOLE_0:def 5; then
A12: f.x=0 by PRE_POLY:def 7;
(-1)*r < (-1)*0 by A9,XREAL_1:69;
hence -r< f.x & f.x <r by A12;
end;
suppose x in Y;
hence thesis by A9;
end;
end; then
consider s1 be Real such that
A13: for x be Point of X holds (-s1< f.x & f.x <s1);
for y being object st y in (the carrier of X) /\ dom f holds f.y<=s1
by A13; then
A14:f|(the carrier of X) is bounded_above by RFUNCT_1:70;
for y being object st y in (the carrier of X) /\ dom f
holds -s1<=f.y by A13; then
A15:f|(the carrier of X) is bounded_below by RFUNCT_1:71;
(the carrier of X ) /\ (the carrier of X ) = (the carrier of X);
then f|(the carrier of X ) is bounded by A14,A15,RFUNCT_1:75;
hence x in BoundedFunctions the carrier of X by A2;
end;
definition
let X be non empty TopSpace;
func C_0_FunctionsNorm X -> Function of (C_0_Functions(X)),REAL equals
(BoundedFunctionsNorm the carrier of X)|(C_0_Functions(X));
correctness
proof
for x being object st x in C_0_Functions(X) holds
x in BoundedFunctions the carrier of X by Th30; then
C_0_Functions(X) c= BoundedFunctions the carrier of X;
hence thesis by FUNCT_2:32;
end;
end;
definition
let X be non empty TopSpace;
func R_Normed_Space_of_C_0_Functions(X) -> non empty NORMSTR equals
NORMSTR (# C_0_Functions(X),
Zero_(C_0_Functions(X), RealVectSpace(the carrier of X)),
Add_(C_0_Functions(X), RealVectSpace(the carrier of X)),
Mult_(C_0_Functions(X), RealVectSpace(the carrier of X)),
C_0_FunctionsNorm X #);
correctness;
end;
registration
let X be non empty TopSpace;
cluster R_Normed_Space_of_C_0_Functions(X) -> strict non empty;
correctness;
end;
theorem
for X be non empty TopSpace
for x being set st x in C_0_Functions(X) holds
x in ContinuousFunctions(X)
proof
let X be non empty TopSpace;
let x be set such that
A1: x in C_0_Functions(X);
consider f be RealMap of X 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 Th32:
for X be non empty TopSpace holds
0.R_VectorSpace_of_C_0_Functions(X) = X -->0
proof
let X be non empty TopSpace;
A1:R_VectorSpace_of_C_0_Functions(X) is
Subspace of RealVectSpace(the carrier of X) by RSSPACE:11;
0.RealVectSpace(the carrier of X) = X -->0;
hence thesis by A1,RLSUB_1:11;
end;
theorem Th33:
for X be non empty TopSpace holds
0.R_Normed_Space_of_C_0_Functions(X) = X --> 0
proof
let X be non empty TopSpace;
0.R_Normed_Space_of_C_0_Functions(X)
=0.R_VectorSpace_of_C_0_Functions(X)
.=X --> 0 by Th32;
hence thesis;
end;
Lm13:
for X be non empty TopSpace
for x1,x2 be Point of R_Normed_Space_of_C_0_Functions(X),
y1,y2 be Point of R_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 R_Normed_Space_of_C_0_Functions(X),
y1,y2 be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume
A1: x1=y1 & x2=y2;
thus x1+x2 = ((the addF of RealVectSpace(the carrier of X))
||C_0_Functions(X)).([x1,x2]) by RSSPACE:def 8
.= (the addF of RAlgebra the carrier of X).([x1,x2]) by FUNCT_1:49
.= ((the addF of RAlgebra the carrier of X)
||(BoundedFunctions the carrier of X)).([y1,y2]) by A1,FUNCT_1:49
.=y1+y2 by C0SP1:def 5;
end;
Lm14:
for X be non empty TopSpace
for a be Real,x be Point of R_Normed_Space_of_C_0_Functions(X),
y be Point of R_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 Real, x be Point of R_Normed_Space_of_C_0_Functions(X),
y be Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X;
assume
A1: x=y;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
thus a*x = ((the Mult of RAlgebra the carrier of X)|
[:REAL,(C_0_Functions(X)):]).([a,x]) by RSSPACE:def 9
.= (the Mult of RAlgebra the carrier of X).([aa,x]) by FUNCT_1:49
.= ((the Mult of RAlgebra the carrier of X)
|[:REAL,(BoundedFunctions the carrier of X):]).([aa,y]) by A1,FUNCT_1:49
.=a*y by C0SP1:def 11;
end;
theorem Th34:
for a be Real
for X be non empty TopSpace
for F,G be Point of R_Normed_Space_of_C_0_Functions(X) holds
(||.F.|| = 0 iff F = 0.R_Normed_Space_of_C_0_Functions(X) ) &
||.a*F.|| = |.a.| * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||
proof
let a be Real;
let X be non empty TopSpace;
let F,G be Point of R_Normed_Space_of_C_0_Functions(X);
A1:||.F.|| = 0 iff F = 0.R_Normed_Space_of_C_0_Functions(X)
proof
reconsider FB=F as
Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X by Th30;
A2: 0.R_Normed_Space_of_C_0_Functions(X) =X-->0 by Th33;
||.FB.|| = 0 iff
FB = 0.R_Normed_Algebra_of_BoundedFunctions the carrier of X
by C0SP1:32;
hence thesis by A2,C0SP1:25,FUNCT_1:49;
end;
A3:||.a*F.|| = |.a.| * ||.F.||
proof
reconsider FB=F as
Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X by Th30;
A4: ||.FB.||=||.F.|| by FUNCT_1:49;
A5: a*FB=a*F by Lm14;
reconsider aFB=a*FB as Point of R_Normed_Algebra_of_BoundedFunctions
the carrier of X;
reconsider aF=a*F as Point of R_Normed_Space_of_C_0_Functions(X);
||.aFB.||=||.aF.|| by A5,FUNCT_1:49;
hence thesis by A4,C0SP1:32;
end;
||.F+G.|| <= ||.F.|| + ||.G.||
proof
reconsider FB=F,GB=G as
Point of R_Normed_Algebra_of_BoundedFunctions the carrier of X by Th30;
A6:||.FB.||=||.F.|| & ||.GB.||=||.G.|| by FUNCT_1:49;
FB+GB=F+G by Lm13; then
A7:||.FB+GB.||=||.F+G.|| by FUNCT_1:49;
reconsider aFB=FB+GB as Point of R_Normed_Algebra_of_BoundedFunctions
the carrier of X;
reconsider aF=F,aG=G as Point of R_Normed_Space_of_C_0_Functions(X);
thus thesis by A7,A6,C0SP1:32;
end;
hence thesis by A1,A3;
end;
theorem Th35:
for X be non empty TopSpace holds
R_Normed_Space_of_C_0_Functions(X) is RealNormSpace-like
proof
let X be non empty TopSpace;
for x, y being Point of R_Normed_Space_of_C_0_Functions(X)
for a be Real holds ||.a*x.|| = |.a.| * ||.x.|| &
||.x+y.|| <= ||.x.|| + ||.y.|| by Th34;
hence thesis by NORMSP_1:def 1;
end;
registration
let X be non empty TopSpace;
cluster R_Normed_Space_of_C_0_Functions(X) ->
reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
coherence
proof
A1:R_VectorSpace_of_C_0_Functions(X) is RealLinearSpace;
A2:for x be Point of R_Normed_Space_of_C_0_Functions(X)
st ||.x.|| = 0 holds
x = 0.(R_Normed_Space_of_C_0_Functions(X)) by Th34;
||.0.(R_Normed_Space_of_C_0_Functions(X)).|| = 0 by Th34;
hence thesis by A1,A2,Th35,RSSPACE3:2;
end;
end;
theorem
for X be non empty TopSpace holds
R_Normed_Space_of_C_0_Functions(X) is RealNormSpace;