:: Functional Space Consisted by Continuous Functions on Topological Space
:: by Hiroshi Yamazaki , Keiichi Miyajima and Yasunari Shidama
::
:: Received March 30, 2021
:: Copyright (c) 2021-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, VALUED_0, PRE_TOPC, ORDINAL2,
SUBSET_1, RCOMP_1, RELAT_1, XBOOLE_0, FUNCT_1, TARSKI, CARD_1, ARYTM_3,
ARYTM_1, COMPLEX1, CONNSP_2, RLVECT_1, ALGSTR_0, FUNCSDOM, REAL_1,
FUNCT_2, VALUED_1, RSSPACE, BINOP_1, SUPINF_2, REALSET1, ZFMISC_1,
RSSPACE4, XXREAL_2, XXREAL_0, NORMSP_1, NORMSP_2, REWRITE1, NAT_1,
MONOID_0, NORMSP_0, FRECHET, RSSPACE3, SEQ_2, TMAP_1, ORDEQ_01, PARTFUN1,
SEQFUNC, C0SP2, LOPBAN_1, METRIC_1, RELAT_2, PRE_POLY, RLSUB_1, RLTOPSP1,
SETFAM_1, FINSET_1, FCONT_1, CFCONT_1, SEQ_4, C0SP3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1,
REALSET1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1,
XXREAL_2, VALUED_0, SEQ_2, SEQ_4, RCOMP_1, SEQFUNC, STRUCT_0, ALGSTR_0,
PRE_POLY, RLVECT_1, RLSUB_1, NORMSP_0, NORMSP_1, NFCONT_1, PRE_TOPC,
TOPS_2, COMPTS_1, FRECHET, FRECHET2, VFUNCT_1, CONNSP_2, RUSUB_4, TMAP_1,
CONVEX1, RLTOPSP1, RSSPACE, RSSPACE3, LOPBAN_1, NORMSP_2, MONOID_0,
RSSPACE4, SEQFUNC2;
constructors REALSET1, RSSPACE3, COMPLEX1, RCOMP_1, C0SP1, FRECHET, FRECHET2,
NFCONT_1, SEQFUNC, MEASURE6, TOPMETR, SEQ_4, COMPTS_1, COMSEQ_2,
NORMSP_2, VFUNCT_1, TMAP_1, RUSUB_4, CONVEX1, TOPS_2, MONOID_0, RSSPACE4,
PRE_POLY, SEQFUNC2;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, XREAL_0, REALSET1,
NUMBERS, ORDINAL1, VALUED_0, PSCOMP_1, XXREAL_0, FUNCT_2, XXREAL_2,
RELSET_1, WAYBEL_2, VFUNCT_1, NORMSP_0, NORMSP_1, NORMSP_2, RLVECT_1,
RLTOPSP1, BORSUK_1, MONOID_0, RSSPACE4;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, RLVECT_1, NORMSP_0, STRUCT_0, ALGSTR_0, PRE_TOPC,
NFCONT_1;
equalities REALSET1, ALGSTR_0, RLVECT_1, STRUCT_0, BINOP_1, NORMSP_0,
NORMSP_2, CONVEX1, LOPBAN_1, RUSUB_4, RSSPACE4, PCOMPS_1;
expansions TARSKI, RLVECT_1, NORMSP_0, NORMSP_1, RLTOPSP1, NFCONT_1, PRE_TOPC,
RLSUB_1, SEQFUNC2, FRECHET;
theorems FUNCT_1, NFCONT_1, PARTFUN1, COMPLEX1, TARSKI, RCOMP_1, XBOOLE_1,
RSSPACE3, RELAT_1, XREAL_0, XXREAL_0, NORMSP_0, NORMSP_1, NORMSP_2,
LOPBAN_1, RLTOPSP1, FUNCT_2, XREAL_1, RLVECT_1, FUNCOP_1, CONNSP_2,
XBOOLE_0, RSSPACE, COMPTS_1, PRE_TOPC, RLSUB_1, SEQ_4, PARTFUN2,
ORDINAL1, TOPMETR4, FRECHET2, TMAP_1, VFUNCT_1, C0SP2, TOPS_2, WEIERSTR,
MONOID_0, RSSPACE4, RLVECT_4, SEQFUNC, SEQFUNC2;
schemes XBOOLE_0;
begin :: Real Vector Space of Continuous Functions
reserve
S for non empty TopSpace,
T for LinearTopSpace,
X for non empty Subset of the carrier of S;
theorem Th1:
for X be non empty TopSpace, S be non empty LinearTopSpace,
f,g be Function of X,S,
x be Point of X
st f is_continuous_at x & g is_continuous_at x
holds f+g is_continuous_at x
proof
let X be non empty TopSpace, S be non empty LinearTopSpace,
f,g be Function of X,S,
x be Point of X;
assume A1: f is_continuous_at x & g is_continuous_at x;
for G being a_neighborhood of (f+g) . x
ex H being a_neighborhood of x st
(f+g) .: H c= G
proof
let G be a_neighborhood of (f+g) . x;
A2: dom f = the carrier of X by FUNCT_2:def 1;
A3: dom g = the carrier of X by FUNCT_2:def 1;
A4: dom (f+g) = (dom f) /\ (dom g) by VFUNCT_1:def 1
.= the carrier of X by A2,A3;
A5:(f+g) . x =(f+g)/. x
.=f/.x+g/.x by VFUNCT_1:def 1,A4
.=f.x +g.x;
consider W being Subset of S such that
A6: W is open & W c= G & (f+g).x in W by CONNSP_2:6;
consider W1, W2 being Subset of S such that
A7: W1 is open & W2 is open & f.x in W1 & g.x in W2
& W1 + W2 c= W by A5,A6,RLTOPSP1:def 8;
reconsider W1 as a_neighborhood of f.x by A7,CONNSP_2:3;
reconsider W2 as a_neighborhood of g.x by A7,CONNSP_2:3;
consider H1 being a_neighborhood of x such that
A8: f .: H1 c= W1 by TMAP_1:def 2,A1;
consider H2 being a_neighborhood of x such that
A9: g .: H2 c= W2 by TMAP_1:def 2,A1;
reconsider H = H1/\ H2 as a_neighborhood of x by CONNSP_2:2;
take H;
thus (f+g) .: H c= G
proof
let y be object;
assume y in (f+g) .: H; then
consider z be object such that
A10: z in the carrier of X
& z in H
& y=(f+g).z by FUNCT_2:64;
reconsider z as Point of X by A10;
A11: (f+g) . z =(f+g)/. z
.=f/.z+g/.z by VFUNCT_1:def 1,A4
.=f.z +g.z;
z in H1 by XBOOLE_0:def 4,A10; then
A12: f.z in f.:H1 by FUNCT_2:35;
z in H2 by XBOOLE_0:def 4,A10; then
g.z in g.:H2 by FUNCT_2:35; then
f.z+g.z in W1+W2 by A12,A8,A9;
hence y in G by A6,A7,A10,A11;
end;
end;
hence thesis by TMAP_1:def 2;
end;
theorem Th2:
for X be non empty TopSpace, S be non empty LinearTopSpace,
f be Function of X,S,
x be Point of X,
a be Real
st f is_continuous_at x
holds a(#)f is_continuous_at x
proof
let X be non empty TopSpace, S be non empty LinearTopSpace,
f be Function of X,S,
x be Point of X,
a be Real;
assume A1: f is_continuous_at x;
for G being a_neighborhood of (a(#)f) . x
ex H being a_neighborhood of x st
(a(#)f) .: H c= G
proof
let G be a_neighborhood of (a(#)f) . x;
A2: dom (a(#)f) = the carrier of X by FUNCT_2:def 1;
A3: ((a(#)f)) . x =((a(#)f))/. x
.=a*f/.x by VFUNCT_1:def 4,A2
.=a*f.x;
consider W being Subset of S such that
A4: W is open & W c= G & ((a(#)f)).x in W by CONNSP_2:6;
consider r be positive Real,W1 being Subset of S such that
A5:W1 is open & f.x in W1
& for s being Real st |.(s - a).| < r holds
s * W1 c= W by A3,A4,RLTOPSP1:def 9;
|.a-a.| = 0 by COMPLEX1:61; then
A6: a * W1 c= W by A5;
reconsider W1 as a_neighborhood of f.x by A5,CONNSP_2:3;
consider H1 being a_neighborhood of x such that
A7: f .: H1 c= W1 by TMAP_1:def 2,A1;
take H1;
thus (a(#)f) .: H1 c= G
proof
let y be object;
assume y in (a(#)f ) .: H1; then
consider z be object such that
A8: z in the carrier of X
& z in H1
& y=(a(#)f).z by FUNCT_2:64;
reconsider z as Point of X by A8;
A9: (a(#)f) . z =(a(#)f)/. z
.=a*f/.z by VFUNCT_1:def 4,A2
.=a*f.z;
f.z in f.:H1 by FUNCT_2:35,A8; then
a*f.z in a*W1 by A7;
hence y in G by A4,A6,A8,A9;
end;
end;
hence thesis by TMAP_1:def 2;
end;
theorem Th3:
for X be non empty TopSpace, S be non empty LinearTopSpace,
f,g be Function of X,S
st f is continuous & g is continuous
holds f+g is continuous
proof
let X be non empty TopSpace, S be non empty LinearTopSpace,
f,g be Function of X,S;
assume A1: f is continuous & g is continuous;
for x being Point of X holds (f+g) is_continuous_at x
proof
let x be Point of X;
f is_continuous_at x & g is_continuous_at x by A1,TMAP_1:44;
hence (f+g) is_continuous_at x by Th1;
end;
hence thesis by TMAP_1:44;
end;
theorem Th4:
for X be non empty TopSpace, S be non empty LinearTopSpace,
f be Function of X,S,
a be Real
st f is continuous
holds a(#)f is continuous
proof
let X be non empty TopSpace, S be non empty LinearTopSpace,
f be Function of X,S,
a be Real;
assume f is continuous; then
for x being Point of X holds a(#)f is_continuous_at x by TMAP_1:44,Th2;
hence thesis by TMAP_1:44;
end;
definition
let S be non empty TopSpace, T be non empty LinearTopSpace;
func ContinuousFunctions(S,T) -> Subset of
RealVectSpace(the carrier of S,T) equals
{ f where f is Function of the carrier of S,
the carrier of T :f is continuous };
correctness
proof
set A = {f where f is Function of the carrier of S,
the carrier of T : f is continuous};
A c= Funcs(the carrier of S, the carrier of T)
proof
let x be object;
assume x in A;
then ex f be Function of the carrier of S,
the carrier of T st x=f & f is continuous;
hence x in Funcs(the carrier of S, the carrier of T) by FUNCT_2:8;
end;
hence thesis;
end;
end;
registration
let S be non empty TopSpace, T be non empty LinearTopSpace;
cluster ContinuousFunctions(S,T) -> non empty functional;
coherence
proof
set f = S --> 0.T;
reconsider f as Function of the carrier of S, the carrier of T;
f in ContinuousFunctions(S,T);
hence ContinuousFunctions(S,T) is non empty;
for x be object st x in ContinuousFunctions(S,T) holds x is Function
proof
let x be object;
assume x in ContinuousFunctions(S,T);
then ex f be Function of the carrier of S, the carrier of T
st x=f & f is continuous;
hence thesis;
end;
hence thesis by FUNCT_1:def 13;
end;
end;
theorem Th5:
for S be non empty TopSpace, T be non empty LinearTopSpace
holds ContinuousFunctions(S,T) is linearly-closed
proof
let S be non empty TopSpace, T be non empty LinearTopSpace;
set W = ContinuousFunctions(S,T);
A1: for v,u be VECTOR of
RealVectSpace(the carrier of S,T) st
v in ContinuousFunctions(S,T)
& u in ContinuousFunctions(S,T)
holds v + u in ContinuousFunctions (S,T)
proof
let v,u be VECTOR of RealVectSpace(the carrier of S,T) such that
A2: v in W and
A3: u in W;
consider f be Function of the carrier of S, the carrier of T such that
A4:v=f & f is continuous by A2;
consider g be Function of the carrier of S, the carrier of T such that
A5:u=g & g is continuous by A3;
reconsider u1 = u as Element of Funcs (the carrier of S,the carrier of T);
reconsider v1 = v as Element of Funcs (the carrier of S,the carrier of T);
reconsider h = f+g as Element of
Funcs (the carrier of S,the carrier of T) by FUNCT_2:8;
A6: dom (f+g) = (dom f) /\ (dom g) by VFUNCT_1:def 1
.= (the carrier of S) /\ (dom g) by FUNCT_2:def 1
.= (the carrier of S) /\ (the carrier of S) by FUNCT_2:def 1
.= the carrier of S;
for x be Element of the carrier of S holds h.x = v1.x + u1.x
proof
let x be Element of the carrier of S;
thus h.x = h/.x
.=f/.x + g/.x by VFUNCT_1:def 1,A6
.=v1.x + u1.x by A4,A5;
end; then
A7: h = v+u by LOPBAN_1:1;
f+g is continuous by A4,A5,Th3;
hence v+u in W by A7;
end;
for a be Real
for v be VECTOR of RealVectSpace(the carrier of S,T) st v
in W holds a * v in W
proof
let a be Real;
let v be VECTOR of RealVectSpace(the carrier of S,T) such that
A8: v in W;
consider f be Function of the carrier of S, the carrier of T such that
A9:v=f & f is continuous by A8;
reconsider v1 = v as Element of Funcs (the carrier of S,the carrier of T);
reconsider h = a(#)f as Element of Funcs (the carrier of S,the carrier of T)
by FUNCT_2:8;
A10: dom (a(#)f) = the carrier of S by FUNCT_2:def 1;
for x be Element of the carrier of S holds h.x = a*v1.x
proof
let x be Element of the carrier of S;
thus h.x = h/.x
.=a*f/.x by VFUNCT_1:def 4,A10
.=a*v1.x by A9;
end; then
A11: h = a*v by LOPBAN_1:2;
a(#)f is continuous by A9,Th4;
hence a*v in W by A11;
end;
hence thesis by A1;
end;
theorem
for S be non empty TopSpace, T be non empty LinearTopSpace
holds RLSStruct
(# ContinuousFunctions(S,T),
Zero_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Add_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Mult_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T))
#) is Subspace of RealVectSpace(the carrier of S,T) by Th5,RSSPACE:11;
registration
let S be non empty TopSpace, T be non empty LinearTopSpace;
cluster RLSStruct (# ContinuousFunctions(S,T),
Zero_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Add_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T)),
Mult_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T))
#) -> Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative
scalar-unital;
coherence by Th5,RSSPACE:11;
end;
definition
let S be non empty TopSpace, T be non empty LinearTopSpace;
func R_VectorSpace_of_ContinuousFunctions(S,T) -> strict RealLinearSpace
equals
RLSStruct (# ContinuousFunctions(S,T),
Zero_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Add_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T)),
Mult_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T))
#);
coherence;
end;
registration
let S be non empty TopSpace, T be non empty LinearTopSpace;
cluster R_VectorSpace_of_ContinuousFunctions(S,T) -> constituted-Functions;
coherence by MONOID_0:80;
end;
definition
let S be non empty TopSpace, T be non empty LinearTopSpace,
f be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T);
let v be Element of S;
redefine func f .v -> VECTOR of T; :: redefines . (FUNCT_1, definition)
correctness
proof
f in ContinuousFunctions(S,T); then
ex x be Function of the carrier of S,
the carrier of T st f=x & x is continuous; then
reconsider f as Function of S,T;
f.v is VECTOR of T;
hence thesis;
end;
end;
theorem Th7:
for S be non empty TopSpace, T be non empty LinearTopSpace
for f,g,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T)
holds h = f+g iff
for x be Element of S holds h.x = f.x + g.x
proof
let S be non empty TopSpace, T be non empty LinearTopSpace;
let f,g,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T);
set G = { f where f is Function of the carrier of S,
the carrier of T :f is continuous };
A1: f in G & g in G & h in G; then
ex x be Function of the carrier of S,
the carrier of T st f=x & x is continuous; then
reconsider f9=f as Function of S,T;
ex x be Function of the carrier of S,
the carrier of T st g=x & x is continuous by A1; then
reconsider g9=g as Function of S,T;
ex x be Function of the carrier of S,
the carrier of T st h=x & x is continuous by A1; then
reconsider h9=h as Function of S,T;
A2: R_VectorSpace_of_ContinuousFunctions(S,T)
is Subspace of RealVectSpace(the carrier of S,T) by Th5,RSSPACE:11;
then reconsider f1=f as VECTOR of RealVectSpace(the carrier of S,T)
by RLSUB_1:10;
reconsider h1=h as VECTOR of RealVectSpace(the carrier of S,T)
by A2,RLSUB_1:10;
reconsider g1=g as VECTOR of RealVectSpace(the carrier of S,T)
by A2,RLSUB_1:10;
A3: now
assume
A4: h = f+g;
let x be Element of S;
h1=f1+g1 by A2,A4,RLSUB_1:13;
hence h9.x=f9.x+g9.x by LOPBAN_1:1;
end;
now
assume for x be Element of S holds h9.x=f9.x+g9.x;
then h1=f1+g1 by LOPBAN_1:1;
hence h =f+g by A2,RLSUB_1:13;
end;
hence thesis by A3;
end;
theorem Th8:
for S be non empty TopSpace, T be non empty LinearTopSpace
for f,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T)
for a be Real holds h = a*f iff for x be Element of S holds h.x = a * f.x
proof
let S be non empty TopSpace, T be non empty LinearTopSpace;
let f,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T);
set G = { f where f is Function of the carrier of S,
the carrier of T :f is continuous };
A1: f in G & h in G; then
ex x be Function of the carrier of S,
the carrier of T st f=x & x is continuous; then
reconsider f9=f as Function of S,T;
ex x be Function of the carrier of S,
the carrier of T st h=x & x is continuous by A1; then
reconsider h9=h as Function of S,T;
let a be Real;
A2: R_VectorSpace_of_ContinuousFunctions(S,T)
is Subspace of RealVectSpace(the carrier of S,T) by Th5,RSSPACE:11;
then reconsider f1=f as VECTOR of RealVectSpace(the carrier of S,T)
by RLSUB_1:10;
reconsider h1=h as VECTOR of RealVectSpace(the carrier of S,T)
by A2,RLSUB_1:10;
A3: now
assume
A4: h = a*f;
let x be Element of S;
h1=a*f1 by A2,A4,RLSUB_1:14;
hence h9.x=a*f9.x by LOPBAN_1:2;
end;
now
assume for x be Element of S holds h9.x=a*f9.x;
then h1=a*f1 by LOPBAN_1:2;
hence h =a*f by A2,RLSUB_1:14;
end;
hence thesis by A3;
end;
theorem Th9:
for S be non empty TopSpace, T be non empty LinearTopSpace
holds 0. R_VectorSpace_of_ContinuousFunctions(S,T)
= (the carrier of S) --> 0.T
proof
let S be non empty TopSpace, T be non empty LinearTopSpace;
A1: 0.RealVectSpace(the carrier of S,T)
=((the carrier of S) -->0.T);
R_VectorSpace_of_ContinuousFunctions(S,T) is Subspace of
RealVectSpace(the carrier of S,T) by Th5,RSSPACE:11;
hence thesis by A1,RLSUB_1:11;
end;
registration
let S be non empty TopSpace, T be non empty LinearTopSpace;
cluster the carrier of R_VectorSpace_of_ContinuousFunctions(S,T) ->
functional;
coherence;
end;
::::::::::::Norm Space version::::::::::::::::::::::::::::
begin :: Real Vector Space of Continuous Functions
reserve
S,T for RealNormSpace,
X for non empty Subset of the carrier of S;
theorem Th10:
for x being Point of T holds
(the carrier of S) --> x is_continuous_on the carrier of S
proof
let x be Point of T;
A1: now
let x1 be Point of S;
let r be Real;
assume that x1 in the carrier of S and
A2: 0 < r;
take s = r;
thus 0 < s by A2;
let x2 be Point of S;
assume x2 in the carrier of S & ||.(x2 - x1).|| < s;
reconsider xx1 = x1, xx2 = x2 as Point of S;
( ((the carrier of S) --> x) /. xx1 = x
& ((the carrier of S) --> x) /. xx2 = x ) by FUNCOP_1:7;
hence ||.((((the carrier of S) --> x) /. x2)
- (((the carrier of S) --> x) /. x1)).|| < r by A2,NORMSP_1:6;
end;
dom ((the carrier of S) --> x) = the carrier of S by FUNCOP_1:13;
hence (the carrier of S) --> x is_continuous_on the carrier of S
by A1, NFCONT_1:19;
end;
definition
let S,T be RealNormSpace;
func ContinuousFunctions(S,T) -> Subset of
RealVectSpace(the carrier of S,T) equals
{ f where f is Function of the carrier of S,
the carrier of T :f is_continuous_on the carrier of S };
correctness
proof
set A = {f where f is Function of the carrier of S,
the carrier of T : f is_continuous_on the carrier of S};
A c= Funcs(the carrier of S, the carrier of T)
proof
let x be object;
assume x in A;
then ex f be Function of the carrier of S,
the carrier of T
st x=f & f is_continuous_on the carrier of S;
hence x in Funcs(the carrier of S, the carrier of T) by FUNCT_2:8;
end;
hence thesis;
end;
end;
registration
let S,T be RealNormSpace;
cluster ContinuousFunctions(S,T) -> non empty functional;
coherence
proof
set f = (the carrier of S) --> 0.T;
reconsider f as Function of the carrier of S, the carrier of T;
f is_continuous_on the carrier of S by Th10; then
f in ContinuousFunctions(S,T);
hence ContinuousFunctions(S,T) is non empty;
for x be object st x in ContinuousFunctions(S,T)
holds x is Function
proof
let x be object;
assume x in ContinuousFunctions(S,T);
then ex f be Function of the carrier of S, the carrier of T
st x=f & f is_continuous_on the carrier of S;
hence thesis;
end;
hence thesis by FUNCT_1:def 13;
end;
end;
theorem Th11:
for S,T be RealNormSpace
holds ContinuousFunctions(S,T) is linearly-closed
proof
let S,T be RealNormSpace;
set W = ContinuousFunctions(S,T);
A1: for v,u be VECTOR of RealVectSpace(the carrier of S,T) st
v in ContinuousFunctions(S,T)
& u in ContinuousFunctions(S,T)
holds v + u in ContinuousFunctions (S,T)
proof
let v,u be VECTOR of RealVectSpace(the carrier of S,T) such that
A2: v in W and
A3: u in W;
consider f be Function of the carrier of S, the carrier of T such that
A4:v=f & f is_continuous_on the carrier of S by A2;
consider g be Function of the carrier of S, the carrier of T such that
A5:u=g & g is_continuous_on the carrier of S by A3;
reconsider u1 = u as Element of Funcs (the carrier of S,the carrier of T);
reconsider v1 = v as Element of Funcs (the carrier of S,the carrier of T);
reconsider h = f+g as Element of Funcs (the carrier of S,the carrier of T)
by FUNCT_2:8;
A6: dom (f+g) = (dom f) /\ (dom g) by VFUNCT_1:def 1
.= (the carrier of S) /\ (dom g) by FUNCT_2:def 1
.= (the carrier of S) /\ (the carrier of S) by FUNCT_2:def 1
.= the carrier of S;
for x be Element of the carrier of S holds h.x = v1.x + u1.x
proof
let x be Element of the carrier of S;
thus h.x = h/.x
.=f/.x + g/.x by VFUNCT_1:def 1,A6
.=v1.x + u1.x by A4,A5;
end; then
A7: h = v+u by LOPBAN_1:1;
f+g is_continuous_on the carrier of S by A4,A5,NFCONT_1:25;
hence v+u in W by A7;
end;
for a be Real
for v be VECTOR of RealVectSpace(the carrier of S,T) st v
in W holds a * v in W
proof
let a be Real;
let v be VECTOR of RealVectSpace(the carrier of S,T);
assume v in W; then
consider f be Function of the carrier of S,
the carrier of T such that
A9:v=f & f is_continuous_on the carrier of S;
reconsider v1 = v as Element of Funcs (the carrier of S,the carrier of T);
reconsider h = a(#)f as Element of
Funcs (the carrier of S,the carrier of T) by FUNCT_2:8;
A10: dom (a(#)f) = the carrier of S by FUNCT_2:def 1;
for x be Element of the carrier of S holds h.x = a*v1.x
proof
let x be Element of the carrier of S;
thus h.x = h/.x
.=a*f/.x by VFUNCT_1:def 4,A10
.=a*v1.x by A9;
end; then
A11: h = a*v by LOPBAN_1:2;
a(#)f is_continuous_on the carrier of S by A9,NFCONT_1:27;
hence a*v in W by A11;
end;
hence thesis by A1;
end;
theorem
for S,T be RealNormSpace holds RLSStruct (# ContinuousFunctions(S,T),
Zero_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Add_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Mult_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T))
#) is Subspace of RealVectSpace(the carrier of S,T)
by Th11,RSSPACE:11;
registration
let S,T be RealNormSpace;
cluster RLSStruct (# ContinuousFunctions(S,T),
Zero_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Add_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T)),
Mult_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T))
#) -> Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital;
coherence by Th11,RSSPACE:11;
end;
definition
let S,T be RealNormSpace;
func R_VectorSpace_of_ContinuousFunctions(S,T) ->
strict RealLinearSpace equals
RLSStruct (# ContinuousFunctions(S,T),
Zero_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Add_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T)),
Mult_(ContinuousFunctions(S,T), RealVectSpace(the carrier of S,T))
#);
coherence;
end;
registration
let S,T be RealNormSpace;
cluster R_VectorSpace_of_ContinuousFunctions(S,T) -> constituted-Functions;
coherence by MONOID_0:80;
end;
definition
let S,T be RealNormSpace,
f be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T);
let v be Element of S;
redefine func f .v -> VECTOR of T; :: redefines . (FUNCT_1, definition)
correctness
proof
f in ContinuousFunctions(S,T); then
ex x be Function of the carrier of S,
the carrier of T st f=x & x is_continuous_on the carrier of S;
then reconsider f as Function of S,T;
f.v is VECTOR of T;
hence thesis;
end;
end;
theorem
for S,T be RealNormSpace
for f,g,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T)
holds h = f+g iff for x be Element of S holds h.x = f.x + g.x
proof
let S,T be RealNormSpace;
let f,g,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T);
set G = { f where f is Function of the carrier of S,
the carrier of T :f is_continuous_on the carrier of S };
A1: f in G & g in G & h in G; then
ex x be Function of the carrier of S,
the carrier of T st f=x & x is_continuous_on the carrier of S; then
reconsider f9=f as Function of S,T;
ex x be Function of the carrier of S,
the carrier of T st g=x & x is_continuous_on the carrier of S by A1; then
reconsider g9=g as Function of S,T;
ex x be Function of the carrier of S,
the carrier of T st h=x & x is_continuous_on the carrier of S by A1;
then reconsider h9=h as Function of S,T;
A2: R_VectorSpace_of_ContinuousFunctions(S,T)
is Subspace of RealVectSpace(the carrier of S,T) by Th11,RSSPACE:11;
then reconsider f1=f as VECTOR of RealVectSpace(the carrier of S,T)
by RLSUB_1:10;
reconsider h1=h as VECTOR of RealVectSpace(the carrier of S,T)
by A2,RLSUB_1:10;
reconsider g1=g as VECTOR of RealVectSpace(the carrier of S,T)
by A2,RLSUB_1:10;
A3: now
assume
A4: h = f+g;
let x be Element of S;
h1=f1+g1 by A2,A4,RLSUB_1:13;
hence h9.x=f9.x+g9.x by LOPBAN_1:1;
end;
now
assume for x be Element of S holds h9.x=f9.x+g9.x;
then h1=f1+g1 by LOPBAN_1:1;
hence h =f+g by A2,RLSUB_1:13;
end;
hence thesis by A3;
end;
theorem
for S,T be RealNormSpace
for f,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T)
for a be Real holds h = a*f iff for x be Element of S holds h.x = a * f.x
proof
let S,T be RealNormSpace;
let f,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T);
set G = { f where f is Function of the carrier of S,
the carrier of T :f is_continuous_on the carrier of S };
A1: f in G & h in G;
then
ex x be Function of the carrier of S,
the carrier of T st f=x & x is_continuous_on the carrier of S; then
reconsider f9=f as Function of S,T;
ex x be Function of the carrier of S,
the carrier of T st h=x & x is_continuous_on the carrier of S by A1; then
reconsider h9=h as Function of S,T;
let a be Real;
A2: R_VectorSpace_of_ContinuousFunctions(S,T)
is Subspace of RealVectSpace(the carrier of S,T) by Th11,RSSPACE:11;
then reconsider f1=f as VECTOR of RealVectSpace(the carrier of S,T)
by RLSUB_1:10;
reconsider h1=h as VECTOR of RealVectSpace(the carrier of S,T)
by A2,RLSUB_1:10;
A3: now
assume
A4: h = a*f;
let x be Element of S;
h1=a*f1 by A2,A4,RLSUB_1:14;
hence h9.x=a*f9.x by LOPBAN_1:2;
end;
now
assume for x be Element of S holds h9.x=a*f9.x;
then h1=a*f1 by LOPBAN_1:2;
hence h =a*f by A2,RLSUB_1:14;
end;
hence thesis by A3;
end;
theorem
for S,T be RealNormSpace holds
R_VectorSpace_of_ContinuousFunctions(S,T)
is Subspace of RealVectSpace(the carrier of S,T) by Th11,RSSPACE:11;
theorem
for S,T be RealNormSpace
holds 0. R_VectorSpace_of_ContinuousFunctions(S,T)
= (the carrier of S) --> 0.T
proof
let S,T be RealNormSpace;
A1: 0.RealVectSpace(the carrier of S,T) = (the carrier of S) -->0.T;
R_VectorSpace_of_ContinuousFunctions(S,T)
is Subspace of RealVectSpace(the carrier of S,T) by Th11,RSSPACE:11;
hence thesis by A1,RLSUB_1:11;
end;
definition
let S,T be RealNormSpace;
let f be object such that
A1: f in ContinuousFunctions(S,T);
func modetrans(f,S,T) -> Function of S,T means
it = f & it is_continuous_on the carrier of S;
existence by A1;
uniqueness;
end;
begin :: Normed Topological Linear Space
definition
struct(RLTopStruct,NORMSTR) RLNormTopStruct
(# carrier -> set, ZeroF -> Element of the carrier,
addF -> BinOp of the carrier,
Mult -> Function of [:REAL, the carrier:],the carrier,
topology -> Subset-Family of the carrier,
normF -> Function of the carrier,REAL #);
end;
registration
let X be non empty set, O be Element of X,
F be BinOp of X, G be Function of [:REAL,X:],X,
T be Subset-Family of X,
N be Function of X,REAL;
cluster RLNormTopStruct (# X,O,F,G,T,N #) -> non empty;
coherence;
end;
registration
cluster strict non empty for RLNormTopStruct;
existence
proof
set X = {0};
reconsider O = 0 as Element of X by TARSKI:def 1;
set F = the BinOp of X;
set G = the Function of [:REAL,X:],X;
set N = the Function of X,REAL;
take RT = RLNormTopStruct (# X,O,F,G,{}bool X,N #);
thus RT is strict;
thus the carrier of RT is non empty;
end;
end;
definition
let X be non empty RLNormTopStruct;
attr X is norm-generated means :Def7:
ex RNS be RealNormSpace
st RNS = the NORMSTR of X
& the topology of X = the topology of TopSpaceNorm RNS;
end;
registration
cluster strict add-continuous Mult-continuous TopSpace-like Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital
discerning reflexive RealNormSpace-like
norm-generated T_2 for non empty RLNormTopStruct;
existence
proof
set RNS = the strict RealNormSpace;
set LRNS = LinearTopSpaceNorm RNS;
reconsider LRNS as strict LinearTopSpace;
A1: the carrier of LRNS = the carrier of RNS
& 0. LRNS = 0. RNS
& the addF of LRNS = the addF of RNS
& the Mult of LRNS = the Mult of RNS
& the topology of LRNS
= the topology of (TopSpaceNorm RNS) by NORMSP_2:def 4;
reconsider N = the normF of RNS
as Function of the carrier of LRNS,REAL by A1;
set W = RLNormTopStruct
(# the carrier of LRNS,
the ZeroF of LRNS,
the addF of LRNS,
the Mult of LRNS,
the topology of LRNS, N #);
A2: now
let x, y be Point of W;
let a be Real;
reconsider u = x, w = y as VECTOR of RNS by NORMSP_2:def 4;
||.u.|| = 0 iff u = 0.RNS by NORMSP_0:def 5;
hence ||.x.|| = 0 iff x = 0.W by A1;
thus ||.(a * x).|| = ||.(a * u).|| by NORMSP_2:def 4
.= |.a.| * ||.u.|| by NORMSP_1:def 1
.= |.a.| * ||.x.||;
||.(u + w).|| <= ||.u.|| + ||.w.|| by NORMSP_1:def 1;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by NORMSP_2:def 4;
end;
take W;
A3: W is TopSpace-like right_complementable Abelian add-associative
right_zeroed vector-distributive scalar-distributive
scalar-associative scalar-unital add-continuous Mult-continuous
proof
A4: for x1, x2 being Point of W
for V being Subset of W st V is open & x1 + x2 in V holds
ex V1, V2 being Subset of W st
V1 is open & V2 is open & x1 in V1 & x2 in V2 & V1 + V2 c= V
proof
let x1, x2 be Point of W;
let V be Subset of W;
assume A5: V is open & x1 + x2 in V;
reconsider V0 = V as Subset of LRNS;
reconsider xx1=x1,xx2=x2 as Point of LRNS;
V0 is open & xx1+xx2 in V0 by A5; then
consider V10, V20 being Subset of LRNS such that
A6: V10 is open & V20 is open
& xx1 in V10 & xx2 in V20 & V10 + V20 c= V0 by RLTOPSP1:def 8;
reconsider V1=V10, V2=V20 as Subset of W;
A7: for z be object holds z in V10 + V20 iff z in V1 + V2
proof
let z be object;
hereby assume z in V10 + V20; then
consider u0, v0 be Element of LRNS such that
A8:z=u0+v0 & u0 in V10 & v0 in V20;
reconsider u =u0,v=v0 as Element of W;
u+v =u0+v0;
hence z in V1 + V2 by A8;
end;
assume z in V1 + V2; then
consider u0, v0 be Element of W such that
A9:z=u0+v0 & u0 in V10 & v0 in V20;
reconsider u =u0,v=v0 as Element of LRNS;
u+v =u0+v0;
hence z in V10 + V20 by A9;
end;
take V1,V2;
thus thesis by A6,A7;
end;
A10: now
let a, b be Real;
let v be VECTOR of W;
reconsider v1 = v as VECTOR of LRNS;
A11: (a * v1) + (b * v1) = (a * v) + (b * v);
(a + b) * v = (a + b) * v1;
hence (a + b) * v = (a * v) + (b * v) by A11, RLVECT_1:def 6;
end;
A12:
for a being Real
for x being Point of W
for V being Subset of W st V is open
& a * x in V holds
ex r being positive Real,
Z being Subset of W st
Z is open & x in Z &
for s being Real st |.(s - a).| < r holds
s * Z c= V
proof
let a be Real;
let x be Point of W,
V be Subset of W;
assume A13: V is open & a * x in V;
reconsider V0 = V as Subset of LRNS;
reconsider xx=x as Point of LRNS;
V0 is open & a*xx in V0 by A13;
then consider r being positive Real,
Z0 being Subset of LRNS such that
A14: Z0 is open & xx in Z0 &
for s being Real st |.(s - a).| < r holds
s * Z0 c= V0 by RLTOPSP1:def 9;
reconsider Z= Z0 as Subset of W;
take r,Z;
for s being Real st |.(s - a).| < r holds s * Z c= V
proof
let s be Real;
assume |.(s - a).| < r; then
A15: s * Z0 c= V0 by A14;
for z be object holds z in s * Z0 iff z in s * Z
proof
let z be object;
hereby assume z in s * Z0; then
consider u0 be Element of LRNS such that
A16:z=s*u0 & u0 in Z0;
reconsider u =u0 as Element of W;
s*u =s*u0;
hence z in s * Z by A16;
end;
assume z in s * Z; then
consider u0 be Element of W such that
A17:z=s*u0 & u0 in Z0;
reconsider u =u0 as Element of LRNS;
s*u =s*u0;
hence z in s * Z0 by A17;
end;
hence thesis by A15;
end;
hence thesis by A14;
end;
A18: W is Abelian
proof
let v, w be VECTOR of W;
reconsider v1 = v, w1 = w as VECTOR of LRNS;
thus v + w = v1 + w1
.= w1 + v1
.= w + v;
end;
A19: W is add-associative
proof
let v, w, x be VECTOR of W;
reconsider v1 = v, w1 = w, x1 = x as VECTOR of LRNS;
thus (v + w) + x = (v1 + w1) + x1
.= v1 + (w1 + x1) by RLVECT_1:def 3
.= v + (w + x);
end;
A20: W is right_zeroed
proof
let v be VECTOR of W;
reconsider v1 = v as VECTOR of LRNS;
thus v + (0. W) = v1 + (0.LRNS)
.= v;
end;
A21: W is right_complementable
proof
let v be VECTOR of W;
reconsider v1 = v as VECTOR of LRNS;
reconsider w = - v1 as VECTOR of W;
take w;
thus v + w = v1 - v1
.= 0.LRNS by RLVECT_1:15
.= 0. W;
end;
A22: now
let a, b be Real;
let v be VECTOR of W;
reconsider v1 = v as VECTOR of LRNS;
a * (b * v1) = a * (b * v);
then (a * b) * v1 = a * (b * v) by RLVECT_1:def 7;
hence (a * b) * v = a * (b * v);
end;
A23: now
let a be Real;
let v, w be VECTOR of W;
reconsider v1 = v, w1 = w as VECTOR of LRNS;
A24: (a * v1) + (a * w1) = (a * v) + (a * w);
a * (v + w) = a * (v1 + w1);
hence a * (v + w) = (a * v) + (a * w) by A24, RLVECT_1:def 5;
end;
now
let v be VECTOR of W;
reconsider v1 = v as VECTOR of LRNS;
thus 1 * v = 1 * v1
.= v by RLVECT_1:def 8;
end;
hence thesis by A18,A12,A4,PRE_TOPC:def 1,A19,A20,A21,A23,A10,A22;
end;
now
let p, q be Point of W;
reconsider p1 = p, q1 = q as Point of LRNS;
assume p <> q;
then consider W1, V1 being Subset of LRNS such that
A25: W1 is open and
A26: V1 is open and
A27: p1 in W1 & q1 in V1 & W1 misses V1 by PRE_TOPC:def 10;
reconsider WW = W1, V = V1 as Subset of W;
A28: V is open by A26;
WW is open by A25;
hence ex b1, b2 being Element of bool the carrier of W st
b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 by A27, A28;
end;
hence thesis by A2,A1,A3;
end;
end;
definition
mode NormedLinearTopSpace is strict add-continuous
Mult-continuous TopSpace-like Abelian add-associative right_zeroed
right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital
discerning reflexive RealNormSpace-like norm-generated
T_2 non empty RLNormTopStruct;
end;
theorem
for X be NormedLinearTopSpace holds X is LinearTopSpace;
theorem
for X be NormedLinearTopSpace holds X is RealNormSpace;
theorem Th19:
for X being NormedLinearTopSpace,
RNS being RealNormSpace
st RNS = the NORMSTR of X
for x,y be Point of X,
x1,y1 be Point of RNS,
a be Real
st x1=x & y1=y
holds
x+y = x1+y1
&
a*x = a*x1
&
x-y = x1-y1
&
||.x.|| = ||.x1.||
proof
let X be NormedLinearTopSpace;
let RNS be RealNormSpace;
assume A1: RNS = the NORMSTR of X;
let x,y be Point of X,
x1,y1 be Point of RNS,
a be Real;
assume A2:x1=x & y1=y;
hence x+y =x1+y1 by A1;
thus a*x =a*x1 by A1,A2;
thus x-y = x + (-1)*y by RLVECT_1:16
.= x1 + (-1)*y1 by A1,A2
.= x1-y1 by RLVECT_1:16;
thus ||.x.|| = ||.x1.|| by A1,A2;
end;
theorem Th20:
for X being NormedLinearTopSpace,
S being sequence of X,
x being Point of X holds
S is_convergent_to x
iff for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r
proof
let X be NormedLinearTopSpace,
S be sequence of X,
x be Point of X;
consider RNS be RealNormSpace such that
A1: RNS = the NORMSTR of X
& the topology of X = the topology of (TopSpaceNorm RNS) by Def7;
reconsider N = S as sequence of RNS by A1;
reconsider xn = x as Point of RNS by A1;
reconsider T = S as sequence of TopSpaceNorm RNS by A1;
reconsider xt = x as Point of TopSpaceNorm RNS by A1;
A2: S is_convergent_to x
iff
T is_convergent_to xt
proof
hereby assume A3: S is_convergent_to x;
now
let U1 be Subset of TopSpaceNorm RNS;
assume A4: U1 is open & xt in U1;
reconsider U0 = U1 as Subset of X by A1;
U0 is open & x in U0 by A1,A4;
then consider n being Nat such that
A5: for m being Nat st n <= m holds S . m in U0 by A3;
take n;
let m be Nat;
assume n <= m;
hence S . m in U1 by A5;
end;
hence T is_convergent_to xt;
end;
assume
A6:T is_convergent_to xt;
now
let U1 be Subset of X;
assume A7:U1 is open & x in U1;
reconsider U0 = U1 as Subset of TopSpaceNorm RNS by A1;
U0 is open & xt in U0 by A1,A7; then
consider n being Nat such that
A8: for m being Nat st n <= m holds T . m in U0 by A6;
take n;
let m be Nat;
assume n <= m;
hence S . m in U1 by A8;
end;
hence S is_convergent_to x;
end;
(for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((N . n) - xn).|| < r )
iff
(for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r )
proof
hereby assume
A9: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds ||.((N . n) - xn).|| < r;
let r be Real;
assume 0 < r; then
consider m being Nat such that
A10: for n being Nat st m <= n holds ||.((N . n) - xn).|| < r by A9;
take m;
let n be Nat;
assume m <= n; then
||.((N . n) - xn).|| < r by A10;
hence ||.((S . n) - x).|| < r by Th19,A1;
end;
assume
A12: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r;
let r be Real;
assume 0 < r; then
consider m being Nat such that
A13: for n being Nat st m <= n holds ||.((S . n) - x).|| < r by A12;
take m;
let n be Nat;
assume m <= n; then
||.((S . n) - x).|| < r by A13;
hence ||.((N . n) - xn).|| < r by Th19,A1;
end;
hence thesis by A2,NORMSP_2:12;
end;
theorem Th21:
for X being NormedLinearTopSpace,
S being sequence of X,
x being Point of X holds
S is convergent & x=lim S
iff
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r
proof
let X be NormedLinearTopSpace,
S be sequence of X,
x be Point of X;
hereby assume
S is convergent & lim S = x; then
S is_convergent_to x by FRECHET2:25;
hence for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r by Th20;
end;
assume for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r;
then S is_convergent_to x by Th20;
hence S is convergent & x=lim S by FRECHET2:25;
end;
theorem Th22:
for X being NormedLinearTopSpace,
S being sequence of X
st S is convergent
holds
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.(S . n) - (lim S) .|| < r
proof
let X be NormedLinearTopSpace,
S be sequence of X;
assume S is convergent;
then consider x being Point of X such that
A1: S is_convergent_to x;
S is convergent & x = lim S by FRECHET2:25,A1;
hence thesis by A1,Th20;
end;
theorem Th23:
for X being NormedLinearTopSpace,
V being Subset of X holds
V is open iff for x being Point of X st x in V holds
ex r being Real st
r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V
proof
let X be NormedLinearTopSpace,
V be Subset of X;
consider RNS be RealNormSpace such that
A1: RNS = the NORMSTR of X
& the topology of X = the topology of TopSpaceNorm RNS by Def7;
reconsider V1 = V as Subset of TopSpaceNorm RNS by A1;
hereby
assume V is open; then
A2:V1 is open by A1;
let x be Point of X;
reconsider x1=x as Point of RNS by A1;
assume x in V; then
consider r be Real such that
A3: r > 0 & { y where y is Point of RNS
: ||.(x1 - y).|| < r } c= V1 by NORMSP_2:7,A2;
take r;
thus r > 0 by A3;
thus { y where y is Point of X : ||.(x - y).|| < r } c= V
proof
let z be object;
assume z in { y where y is Point of X
: ||.(x - y).|| < r }; then
consider y be Point of X such that
A4:y=z & ||.(x - y).|| < r;
reconsider y1=y as Point of RNS by A1;
||.(x1 - y1).|| < r by Th19,A1,A4; then
y1 in { y where y is Point of RNS : ||.(x1 - y).|| < r };
hence z in V by A4,A3;
end;
end;
assume A5:for x being Point of X st x in V holds
ex r being Real st
r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V;
now
let x be Point of RNS;
reconsider x1=x as Point of X by A1;
assume x in V1; then
consider r be Real such that
A6: r > 0 & { y where y is Point of X
: ||.(x1 - y).|| < r } c= V by A5;
take r;
thus r > 0 by A6;
{ y where y is Point of RNS : ||.(x - y).|| < r } c= V1
proof
let z be object;
assume z in { y where y is Point of RNS : ||.(x - y).|| < r }; then
consider y be Point of RNS such that
A7:y=z & ||.(x - y).|| < r;
reconsider y1=y as Point of X by A1;
||.(x1 - y1).|| < r by Th19,A1,A7;
then y1 in { y where y is Point of X : ||.(x1 - y).|| < r };
hence z in V1 by A7,A6;
end;
hence { y where y is Point of RNS : ||.(x - y).|| < r } c= V1;
end;
then V1 is open by NORMSP_2:7;
hence V is open by A1;
end;
theorem Th24:
for X being NormedLinearTopSpace
for x being Point of X
for r being Real
for V being Subset of X
st V = { y where y is Point of X : ||.(x - y).|| < r } holds V is open
proof
let X be NormedLinearTopSpace;
let x be Point of X;
let r be Real;
let V be Subset of X;
consider RNS be RealNormSpace such that
A1: RNS = the NORMSTR of X
& the topology of X = the topology of (TopSpaceNorm RNS) by Def7;
reconsider V0 = V as Subset of (TopSpaceNorm RNS) by A1;
reconsider x1=x as Point of RNS by A1;
assume A2:V = { y where y is Point of X : ||.(x - y).|| < r };
for z be object holds
z in { y where y is Point of X : ||.(x - y).|| < r }
iff z in { y where y is Point of RNS : ||.(x1 - y).|| < r }
proof
let z be object;
hereby assume z in { y where y is Point of X : ||.(x - y).|| < r }; then
consider y be Point of X such that
A3:y=z & ||.(x - y).|| < r;
reconsider y1=y as Point of RNS by A1;
||.(x1 - y1).|| < r by Th19,A1,A3;
hence z in { y where y is Point of RNS : ||.(x1 - y).|| < r } by A3;
end;
assume z in { y where y is Point of RNS : ||.(x1 - y).|| < r }; then
consider y1 be Point of RNS such that
A4:y1=z & ||.(x1 - y1).|| < r;
reconsider y=y1 as Point of X by A1;
||.(x - y).|| < r by Th19,A1,A4;
hence z in { y where y is Point of X : ||.(x - y).|| < r } by A4;
end;
then
{ y where y is Point of X : ||.(x - y).|| < r }
= { y where y is Point of RNS : ||.(x1 - y).|| < r } by TARSKI:2;
then V0 is open by NORMSP_2:8,A2;
hence V is open by A1;
end;
theorem
for X being NormedLinearTopSpace
for x being Point of X
for r being Real
for V being Subset of X
st V = { y where y is Point of X : ||.(x - y).|| <= r } holds
V is closed
proof
let X be NormedLinearTopSpace;
let x be Point of X;
let r be Real;
let V be Subset of X;
assume
A1: V = { y where y is Point of X : ||.(x - y).|| <= r };
consider RNS be RealNormSpace such that
A2: RNS = the NORMSTR of X
& the topology of X = the topology of (TopSpaceNorm RNS) by Def7;
reconsider V0 = V as Subset of (TopSpaceNorm RNS) by A2;
reconsider x1=x as Point of RNS by A2;
reconsider V1 = V as Subset of (LinearTopSpaceNorm RNS)
by A2,NORMSP_2:def 4;
for z be object holds
z in { y where y is Point of X : ||.(x - y).|| <= r }
iff z in { y where y is Point of RNS : ||.(x1 - y).|| <= r }
proof
let z be object;
hereby assume z in { y where y is Point of X
: ||.(x - y).|| <= r }; then
consider y be Point of X such that
A3:y=z & ||.(x - y).|| <= r;
reconsider y1=y as Point of RNS by A2;
||.(x1 - y1).|| <= r by Th19,A2,A3;
hence z in { y where y is Point of RNS
: ||.(x1 - y).|| <= r } by A3;
end;
assume z in { y where y is Point of RNS : ||.(x1 - y).|| <= r }; then
consider y1 be Point of RNS such that
A4:y1=z & ||.(x1 - y1).|| <= r;
reconsider y=y1 as Point of X by A2;
||.(x - y).|| <= r by Th19,A2,A4;
hence z in { y where y is Point of X : ||.(x - y).|| <= r } by A4;
end; then
V0 is closed by NORMSP_2:24,A1,TARSKI:2; then
([#] (TopSpaceNorm RNS)) \ V0 is open; then
([#] X) \ V is open by A2;
hence V is closed;
end;
theorem Th26:
for X being NormedLinearTopSpace,
RNS being RealNormSpace,
t being sequence of X,
s being sequence of RNS
st RNS = the NORMSTR of X & t=s
& t is convergent
holds s is convergent & lim s = lim t
proof
let X be NormedLinearTopSpace,
RNS be RealNormSpace,
t2 be sequence of X,
s2 be sequence of RNS;
assume A1: RNS = the NORMSTR of X
& t2=s2
& t2 is convergent;
reconsider y = lim t2 as Point of RNS by A1;
A2:for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.s2.n - y .|| < r
proof
let r be Real;
assume 0 < r; then
consider m being Nat such that
A3: for n being Nat st m <= n holds
||.t2 . n - lim t2 .|| < r by A1,Th22;
take m;
let n be Nat;
assume m <= n; then
||.t2 . n - lim t2 .|| < r by A3;
hence ||.s2.n - y .|| < r by Th19,A1;
end;
hence s2 is convergent;
hence thesis by A2,NORMSP_1:def 7;
end;
theorem Th27:
for X being NormedLinearTopSpace,
RNS being RealNormSpace,
s being sequence of X,
t being sequence of RNS
st RNS = the NORMSTR of X & s=t
holds
s is convergent
iff
t is convergent
proof
let X be NormedLinearTopSpace,
RNS be RealNormSpace,
s2 be sequence of X,
t2 be sequence of RNS;
assume A1: RNS = the NORMSTR of X & s2=t2;
thus s2 is convergent implies t2 is convergent by A1,Th26;
assume
A2: t2 is convergent;
reconsider y = lim t2 as Point of X by A1;
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.s2.n - y .|| < r
proof
let r be Real;
assume 0 < r; then
consider m being Nat such that
A3: for n being Nat st m <= n holds
||.t2 . n - lim t2 .|| < r by A2,NORMSP_1:def 7;
take m;
let n be Nat;
assume m <= n; then
||.t2 . n - lim t2 .|| < r by A3;
hence ||.s2.n - y .|| < r by Th19,A1;
end;
hence s2 is convergent by Th21;
end;
theorem Th28:
for X being NormedLinearTopSpace,
V being Subset of X
holds
V is closed iff
for s1 being sequence of X st rng s1 c= V & s1 is convergent holds
lim s1 in V
proof
let X be NormedLinearTopSpace;
let V be Subset of X;
consider RNS be RealNormSpace such that
A1: RNS = the NORMSTR of X
& the topology of X = the topology of TopSpaceNorm RNS by Def7;
reconsider V0 = V as Subset of TopSpaceNorm RNS by A1;
reconsider V1 = V as Subset of RNS by A1;
hereby assume V is closed; then
([#] X) \ V is open; then
([#] (TopSpaceNorm RNS)) \ V0 is open by A1; then
V0 is closed; then
A2: V1 is closed by NORMSP_2:15;
thus for s1 being sequence of X st rng s1 c= V & s1 is convergent holds
lim s1 in V
proof
let s1 be sequence of X;
assume A3: rng s1 c= V & s1 is convergent;
reconsider s2=s1 as sequence of RNS by A1;
s2 is convergent & lim s1=lim s2 by A1,A3,Th26;
hence lim s1 in V by A2,A3;
end;
end;
assume
A4: for s1 being sequence of X st rng s1 c= V & s1 is convergent holds
lim s1 in V;
for s1 being sequence of RNS st rng s1 c= V1 & s1 is convergent holds
lim s1 in V1
proof
let s2 be sequence of RNS;
assume A5: rng s2 c= V1 & s2 is convergent;
reconsider s1=s2 as sequence of X by A1;
A6: s1 is convergent by A5,A1,Th27; then
lim s1=lim s2 by A1,Th26;
hence lim s2 in V1 by A4,A6,A5;
end; then
V1 is closed; then
V0 is closed by NORMSP_2:15; then
([#] (TopSpaceNorm RNS)) \ V0 is open; then
([#] X) \ V is open by A1;
hence V is closed;
end;
Lm1: for X being RealNormSpace
for r being Real
for x being Point of X holds
{ y where y is Point of X : ||.(x - y).|| < r }
= { y where y is Point of X : ||.(y - x).|| < r }
proof
let X be RealNormSpace;
let r be Real;
let x be Point of X;
now
let s be object;
assume s in { y where y is Point of X : ||.(y - x).|| < r };
then consider z being Point of X such that
A1: s = z and
A2: ||.(z - x).|| < r;
||.(x - z).|| < r by A2, NORMSP_1:7;
hence s in { y where y is Point of X : ||.(x - y).|| < r } by A1;
end;
then A3: { y where y is Point of X : ||.(y - x).|| < r }
c= { y where y is Point of X : ||.(x - y).|| < r };
now
let s be object;
assume s in { y where y is Point of X : ||.(x - y).|| < r };
then consider z being Point of X such that
A4: s = z and
A5: ||.(x - z).|| < r;
||.(z - x).|| < r by A5, NORMSP_1:7;
hence s in { y where y is Point of X : ||.(y - x).|| < r } by A4;
end;
then { y where y is Point of X : ||.(x - y).|| < r }
c= { y where y is Point of X : ||.(y - x).|| < r };
hence { y where y is Point of X : ||.(x - y).|| < r }
= { y where y is Point of X : ||.(y - x).|| < r } by A3, XBOOLE_0:def 10;
end;
theorem
for X being NormedLinearTopSpace,
RNS be RealNormSpace,
V being Subset of X,
W being Subset of RNS st
RNS = the NORMSTR of X
& the topology of X = the topology of (TopSpaceNorm RNS)
& V = W
holds
V is closed iff W is closed
proof
let X be NormedLinearTopSpace,
RNS be RealNormSpace,
V be Subset of X,
V0 be Subset of RNS;
assume A1:
RNS = the NORMSTR of X
& the topology of X = the topology of (TopSpaceNorm RNS)
& V = V0;
hereby assume
A2: V is closed;
for s2 being sequence of RNS st rng s2 c= V0 & s2 is convergent holds
lim s2 in V0
proof
let s2 be sequence of RNS;
reconsider s1=s2 as sequence of X by A1;
assume A3: rng s2 c= V0 & s2 is convergent; then
A4: s1 is convergent by Th27,A1;
then lim s1 = lim s2 by Th26,A1;
hence lim s2 in V0 by A1,A2,Th28,A3,A4;
end;
hence V0 is closed;
end;
assume A5:V0 is closed;
for s2 being sequence of X st rng s2 c= V & s2 is convergent holds
lim s2 in V
proof
let s2 be sequence of X;
assume A6: rng s2 c= V & s2 is convergent;
reconsider s1=s2 as sequence of RNS by A1;
A7: s1 is convergent by Th27,A1,A6;
lim s1 = lim s2 by Th26,A1,A6;
hence lim s2 in V by A1,A5,A6,A7;
end;
hence V is closed by Th28;
end;
theorem Th30:
for X being NormedLinearTopSpace,
V be Subset of X,
x being Point of X
holds
( V is a_neighborhood of x
iff
( ex r being Real st
r > 0 & { y where y is Point of X : ||.y-x.|| < r } c= V ))
proof
let X be NormedLinearTopSpace,
V be Subset of X,
x be Point of X;
hereby
assume V is a_neighborhood of x;
then consider U being Subset of X such that
A1: U is open and
A2: U c= V and
A3: x in U by CONNSP_2:6;
consider r being Real such that
A4:
r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= U
by Th23,A1,A3;
{ y where y is Point of X : ||.(x - y).|| < r }
=
{ y where y is Point of X : ||. y - x.|| < r } by Lm1;
hence ex r being Real st
r > 0
& { y where y is Point of X : ||.y - x.|| < r } c= V
by A4,A2,XBOOLE_1:1;
end;
given r being Real such that
A5: r > 0
& { y where y is Point of X : ||.(y - x).|| < r } c= V;
reconsider U = { y where y is Point of X : ||.(y - x).|| < r }
as Subset of X by A5,XBOOLE_1:1;
A6:
{ y where y is Point of X : ||.(y - x).|| < r } =
{ y where y is Point of X : ||.x - y.|| < r } by Lm1;
||.(x - x).|| = 0 by NORMSP_1:6; then
x in U by A5;
hence V is a_neighborhood of x by A5,A6,Th24,CONNSP_2:6;
end;
theorem Th31:
for X being NormedLinearTopSpace,
V being Subset of X holds
V is compact iff
for s1 being sequence of X st rng s1 c= V holds
ex s2 being sequence of X st
s2 is subsequence of s1
& s2 is convergent & lim s2 in V
proof
let X be NormedLinearTopSpace;
let V be Subset of X;
consider RNS be RealNormSpace such that
A1: RNS = the NORMSTR of X
& the topology of X = the topology of (TopSpaceNorm RNS) by Def7;
reconsider V0 = V as Subset of (TopSpaceNorm RNS) by A1;
reconsider V1 = V as Subset of RNS by A1;
hereby assume A2:V is compact;
for F being Subset-Family of (TopSpaceNorm RNS)
st F is Cover of V0 & F is open holds
ex G being Subset-Family of (TopSpaceNorm RNS) st
( G c= F & G is Cover of V0 & G is finite )
proof
let F0 being Subset-Family of (TopSpaceNorm RNS);
assume A3: F0 is Cover of V0 & F0 is open;
reconsider F=F0 as Subset-Family of X by A1;
A4:
for P being Subset of X st P in F holds
P is open
proof
let P being Subset of X;
assume A5:P in F;
reconsider P0=P as Subset of (TopSpaceNorm RNS) by A1;
P0 is open by A3,TOPS_2:def 1,A5;
hence P is open by A1;
end;
consider G being Subset-Family of X such that
A6: G c= F & G is Cover of V & G is finite
by A2,COMPTS_1:def 4,A3,A4,TOPS_2:def 1;
reconsider G0=G as Subset-Family of (TopSpaceNorm RNS) by A1;
take G0;
thus G0 c= F0 by A6;
thus G0 is Cover of V0 by A6;
thus G0 is finite by A6;
end; then
V0 is compact by COMPTS_1:def 4; then
A7: V1 is compact by TOPMETR4:19;
thus for s1 being sequence of X st rng s1 c= V holds
ex s2 being sequence of X st
s2 is subsequence of s1 & s2 is convergent & lim s2 in V
proof
let s1 be sequence of X;
reconsider t1 =s1 as sequence of RNS by A1;
assume rng s1 c= V; then
consider t2 being sequence of RNS such that
A9: t2 is subsequence of t1
& t2 is convergent & lim t2 in V1 by A7;
reconsider s2=t2 as sequence of X by A1;
take s2;
thus s2 is subsequence of s1 by A9;
s2 is convergent by A9,Th27,A1;
hence s2 is convergent & lim s2 in V by A9,A1,Th26;
end;
end;
assume
A11:for s1 being sequence of X st rng s1 c= V holds
ex s2 being sequence of X st
s2 is subsequence of s1 & s2 is convergent & lim s2 in V;
for s1 being sequence of RNS st rng s1 c= V1 holds
ex s2 being sequence of RNS st
s2 is subsequence of s1 & s2 is convergent & lim s2 in V1
proof
let s1 be sequence of RNS;
assume A12: rng s1 c= V1;
reconsider t1 =s1 as sequence of X by A1;
consider t2 being sequence of X such that
A13: t2 is subsequence of t1
& t2 is convergent & lim t2 in V by A11,A12;
reconsider s2=t2 as sequence of RNS by A1;
take s2;
thus s2 is subsequence of s1 by A13;
thus
s2 is convergent & lim s2 in V1 by A13,Th26,A1;
end; then
V1 is compact; then
A14:V0 is compact by TOPMETR4:19;
for F being Subset-Family of X
st F is Cover of V & F is open holds
ex G being Subset-Family of X st
G c= F & G is Cover of V & G is finite
proof
let F be Subset-Family of X;
assume A15: F is Cover of V & F is open;
reconsider F0=F as Subset-Family of (TopSpaceNorm RNS) by A1;
A16: for P0 being Subset of (TopSpaceNorm RNS) st P0 in F0 holds
P0 is open
proof
let P0 be Subset of TopSpaceNorm RNS;
assume A17:P0 in F0;
reconsider P=P0 as Subset of X by A1;
P is open by A15,TOPS_2:def 1,A17;
hence P0 is open by A1;
end;
consider G0 being Subset-Family of (TopSpaceNorm RNS) such that
A18: G0 c= F0 & G0 is Cover of V0 & G0 is finite
by A14,COMPTS_1:def 4,A15, A16,TOPS_2:def 1;
reconsider G=G0 as Subset-Family of X by A1;
take G;
thus G c= F by A18;
thus G is Cover of V by A18;
thus G is finite by A18;
end;
hence V is compact by COMPTS_1:def 4;
end;
theorem Th32:
for X being NormedLinearTopSpace,
RNS be RealNormSpace,
V being Subset of X,
W being Subset of RNS st
RNS = the NORMSTR of X
& the topology of X = the topology of TopSpaceNorm RNS
& V = W
holds
V is compact iff W is compact
proof
let X be NormedLinearTopSpace,
RNS be RealNormSpace,
V be Subset of X,
V0 be Subset of RNS;
assume A1:
RNS = the NORMSTR of X
& the topology of X = the topology of TopSpaceNorm RNS
& V = V0;
hereby assume
A2: V is compact;
for t1 being sequence of RNS st rng t1 c= V0 holds
ex t2 being sequence of RNS st
t2 is subsequence of t1
& t2 is convergent & lim t2 in V0
proof
let t1 be sequence of RNS;
assume A3: rng t1 c= V0;
reconsider s1=t1 as sequence of X by A1;
consider s2 being sequence of X such that
A4: s2 is subsequence of s1
& s2 is convergent & lim s2 in V by A2,Th31,A3,A1;
reconsider t2=s2 as sequence of RNS by A1;
take t2;
thus thesis by A4,A1,Th26;
end;
hence V0 is compact;
end;
assume
A5: V0 is compact;
for t1 being sequence of X st rng t1 c= V holds
ex t2 being sequence of X st
t2 is subsequence of t1
& t2 is convergent & lim t2 in V
proof
let t1 be sequence of X;
assume A6: rng t1 c= V;
reconsider s1=t1 as sequence of RNS by A1;
consider s2 being sequence of RNS such that
A7: s2 is subsequence of s1
& s2 is convergent & lim s2 in V0 by A5,A6,A1;
reconsider t2=s2 as sequence of X by A1;
take t2;
t2 is convergent by A7,A1,Th27;
hence thesis by A7,A1,Th26;
end;
hence V is compact by Th31;
end;
begin :: Real Norm Space of Continuous Functions
theorem Th33:
for X, X1 being set
for S being RealNormSpace
for f being PartFunc of S,REAL
st f is_continuous_on X & X1 c= X holds
f is_continuous_on X1
proof
let X, X1 be set;
let S be RealNormSpace;
let f be PartFunc of S,REAL;
assume that
A1: f is_continuous_on X and
A2: X1 c= X;
X c= dom f by A1;
hence A3: X1 c= dom f by A2;
let r be Point of S;
assume A4: r in X1; then
A5: f | X is_continuous_in r by A1, A2;
thus f | X1 is_continuous_in r
proof
(dom f) /\ X1 c= (dom f) /\ X by A2, XBOOLE_1:26;
then dom (f | X1) c= (dom f) /\ X by RELAT_1:61; then
A6: dom (f | X1) c= dom (f | X) by RELAT_1:61;
r in (dom f) /\ X1 by A3, A4, XBOOLE_0:def 4;
hence A7: r in dom (f | X1) by RELAT_1:61; then
A8: (f | X) /. r = f /. r by A6, PARTFUN2:15
.= (f | X1) /. r by A7, PARTFUN2:15;
let s1 be sequence of S;
assume that
A9: rng s1 c= dom (f | X1) and
A10:s1 is convergent & lim s1 = r;
A11:rng s1 c= dom (f | X) by A9, A6;
A12:now
let n be Element of NAT;
dom s1 = NAT by FUNCT_2:def 1; then
A13: s1 . n in rng s1 by FUNCT_1:3;
thus ((f | X) /* s1) . n
= (f | X) /. (s1 . n) by A9, A6, FUNCT_2:109, XBOOLE_1:1
.= f /. (s1 . n) by A9, A6,A13, PARTFUN2:15
.= (f | X1) /. (s1 . n) by A9, A13, PARTFUN2:15
.= ((f | X1) /* s1) . n by A9, FUNCT_2:109;
end;
( (f | X) /* s1 is convergent
& (f | X) /. r = lim ((f | X) /* s1) ) by A5, A10, A11;
hence ( (f | X1) /* s1 is convergent
& (f | X1) /. r = lim ((f | X1) /* s1) ) by A8, A12, FUNCT_2:63;
end;
end;
Lm2:
for S be non empty TopSpace, T being NormedLinearTopSpace
for f being Function of S,T
for Y being Subset of S
st Y <> {}
& Y c= dom f
& Y is compact
& f is continuous
holds
ex K be Real
st
0 <= K
&
for x be Point of S
st x in Y
holds ||.f.x.|| <= K
proof
let S be non empty TopSpace, T be NormedLinearTopSpace;
let f be Function of S,T;
let Y be Subset of S;
assume that
A1: Y <> {} and
A2: Y c= dom f and
A3: Y is compact and
A4: f is continuous;
consider RNS be RealNormSpace such that
A5: RNS = the NORMSTR of T &
the topology of T = the topology of (TopSpaceNorm RNS) by Def7;
reconsider g = the normF of RNS
as Function of the carrier of RNS,REAL;
A6:for x be Point of RNS st x in the carrier of RNS holds g/.x = ||.x.||;
A7: the carrier of RNS = dom g by FUNCT_2:def 1;
reconsider g as PartFunc of RNS,REAL;
reconsider FY = f.:Y as Subset of RNS by A5;
A8: g is_continuous_on FY by A7,NFCONT_1:54,A6,Th33;
A9: f.:Y is compact by A3,A4,WEIERSTR:8;
A10: dom (g | FY) = (dom g) /\ FY by RELAT_1:61
.= FY by A7, XBOOLE_1:28;
A11: (g | FY) is_continuous_on FY
proof
thus FY c= dom (g | FY) by A10;
let r be Point of RNS;
assume r in FY;
then g | FY is_continuous_in r by A8;
hence (g | FY) | FY is_continuous_in r by RELAT_1:72;
end;
A12:dom (g | FY) is compact by A9,A5,Th32,A10;
A13: g.: FY = rng (g | FY) by RELAT_1:115; then
A14: g.: FY is real-bounded by RCOMP_1:10,A12,A10,A11,NFCONT_1:31;
consider x1, x2 being Point of RNS such that
A15: x1 in dom (g | FY) & x2 in dom (g | FY) and
A16: (g | FY) /. x1 = upper_bound (rng (g | FY))
& (g | FY) /. x2 = lower_bound (rng (g | FY))
by A10,A11,A12,NFCONT_1:33,A1;
set K = (g | FY) /. x1;
set L = (g | FY) /. x2;
A17: K = (g | FY) . x1 by A15,PARTFUN1:def 6;
take K;
K = ||.x1.|| by FUNCT_1:47,A15,A17;
hence 0 <= K;
thus for x be Point of S st x in Y holds ||. f.x .|| <= K
proof
let z be Point of S;
assume A18: z in Y;
A19:f.z in dom (g|FY) by A10,A18,FUNCT_1:def 6,A2; then
A20: (g|FY).(f.z) in rng (g|FY) by FUNCT_1:3;
A21: (g|FY).(f.z) = g.(f.z) by A19,FUNCT_1:47
.= g/.(f.z) by A5,PARTFUN1:def 6,A7;
reconsider fz = f.z as Point of RNS by A5;
g/.fz = ||.fz.|| by A6
.=||.f.z.|| by A5;
hence thesis by A21,A20,A16,A14,A13,SEQ_4:def 1;
end;
end;
theorem Th34:
for S be non empty compact TopSpace,T be NormedLinearTopSpace holds
for x being set st x in ContinuousFunctions(S,T) holds
x in BoundedFunctions (the carrier of S,T)
proof
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
let x be set;
assume x in ContinuousFunctions(S,T); then
consider f be Function of the carrier of S,the carrier of T such that
A1:x=f & f is continuous;
A2:dom f = the carrier of S by FUNCT_2:def 1;
consider K be Real such that
A3: 0 <= K &
for x being Element of S st x in [#]S
holds ||.f. x.|| <= K by A1,A2,Lm2,COMPTS_1:1;
for x being Element of S holds ||.f. x.|| <= K by A3; then
f is bounded by RSSPACE4:def 4,A3;
hence x in BoundedFunctions (the carrier of S,T) by RSSPACE4:def 5,A1;
end;
theorem
for S be non empty compact TopSpace,T be NormedLinearTopSpace holds
(R_VectorSpace_of_ContinuousFunctions(S,T) is
Subspace of R_VectorSpace_of_BoundedFunctions(the carrier of S,T))
proof
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
A1:the carrier of R_VectorSpace_of_ContinuousFunctions(S,T)
c= the carrier of R_VectorSpace_of_BoundedFunctions(the carrier of S,T)
by Th34;
A2:R_VectorSpace_of_ContinuousFunctions(S,T) is
Subspace of RealVectSpace(the carrier of S,T) by Th5,RSSPACE:11;
R_VectorSpace_of_BoundedFunctions(the carrier of S,T) is
Subspace of RealVectSpace(the carrier of S,T) by RSSPACE4:7;
hence thesis by A1,A2,RLSUB_1:28;
end;
definition
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
func ContinuousFunctionsNorm(S,T) ->
Function of (ContinuousFunctions(S,T)),REAL
equals
(BoundedFunctionsNorm(the carrier of S,T)) | (ContinuousFunctions(S,T));
correctness
proof
ContinuousFunctions(S,T) c= BoundedFunctions(the carrier of S,T) by Th34;
hence thesis by FUNCT_2:32;
end;
end;
definition
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
func R_NormSpace_of_ContinuousFunctions(S,T) -> strict NORMSTR equals
NORMSTR (# ContinuousFunctions(S,T),
Zero_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Add_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
Mult_(ContinuousFunctions(S,T),RealVectSpace(the carrier of S,T)),
ContinuousFunctionsNorm(S,T) #);
correctness;
end;
registration
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
cluster R_NormSpace_of_ContinuousFunctions(S,T) -> non empty;
correctness;
end;
theorem Th36:
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for x be Point of R_NormSpace_of_ContinuousFunctions(S,T),
y be Point of R_NormSpace_of_BoundedFunctions(the carrier of S,T)
st x=y holds ||.x.||= ||.y.|| by FUNCT_1:49;
theorem
for S be non empty compact TopSpace,
T be NormedLinearTopSpace,
f be Point of R_NormSpace_of_ContinuousFunctions(S,T),
g be Function of S,T
st f=g holds
for t be Point of S holds ||.g.t.|| <= ||.f.||
proof
let S be non empty compact TopSpace,
T be NormedLinearTopSpace;
let f be Point of R_NormSpace_of_ContinuousFunctions(S,T),
g be Function of S,T;
assume A1: f=g; then
g in BoundedFunctions (the carrier of S,T) by Th34; then
reconsider h =g as bounded Function of the carrier of S,T
by RSSPACE4:def 5;
reconsider k =h as Point of
R_NormSpace_of_BoundedFunctions(the carrier of S,T) by Th34,A1;
||.k.|| = ||.f.|| by A1,FUNCT_1:49;
hence thesis by RSSPACE4:16;
end;
theorem Th38:
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for x1,x2 be Point of R_NormSpace_of_ContinuousFunctions(S,T),
y1,y2 be Point of R_NormSpace_of_BoundedFunctions(the carrier of S,T)
st x1=y1 & x2=y2 holds x1+x2=y1+y2
proof
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
let x1,x2 be Point of R_NormSpace_of_ContinuousFunctions(S,T),
y1,y2 be Point of R_NormSpace_of_BoundedFunctions(the carrier of S,T);
assume A1: x1=y1 & x2=y2;
thus x1+x2 = ((the addF of RealVectSpace(the carrier of S,T))
||(ContinuousFunctions(S,T))).([x1,x2]) by RSSPACE:def 8,Th5
.= (the addF of RealVectSpace(the carrier of S,T)).([x1,x2]) by FUNCT_1:49
.= ((the addF of RealVectSpace(the carrier of S,T))
||(BoundedFunctions(the carrier of S,T))).([y1,y2]) by A1,FUNCT_1:49
.=y1+y2 by RSSPACE:def 8,RSSPACE4:6;
end;
theorem Th39:
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for a be Real,
x be Point of R_NormSpace_of_ContinuousFunctions(S,T),
y be Point of R_NormSpace_of_BoundedFunctions(the carrier of S,T)
st x=y holds a*x=a*y
proof
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
let a be Real,
x be Point of R_NormSpace_of_ContinuousFunctions(S,T),
y be Point of R_NormSpace_of_BoundedFunctions(the carrier of S,T);
assume
A1: x=y;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
thus a*x = ((the Mult of RealVectSpace(the carrier of S,T)) |
[:REAL,(ContinuousFunctions(S,T)):]).([a,x])
by RSSPACE:def 9,Th5
.= (the Mult of RealVectSpace(the carrier of S,T)).([aa,x]) by FUNCT_1:49
.= ((the Mult of RealVectSpace(the carrier of S,T))
|[:REAL,(BoundedFunctions(the carrier of S,T)):]).[aa,y]
by A1,FUNCT_1:49
.=a*y by RSSPACE:def 9,RSSPACE4:6;
end;
registration
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
cluster R_NormSpace_of_ContinuousFunctions(S,T) -> non empty
right_complementable Abelian add-associative right_zeroed
vector-distributive scalar-distributive scalar-associative scalar-unital;
coherence
proof
set l = R_NormSpace_of_ContinuousFunctions(S,T);
RLSStruct(# the carrier of l, the ZeroF of l, the addF of l,
the Mult of l #) = R_VectorSpace_of_ContinuousFunctions(S,T);
hence thesis by RSSPACE3:2;
end;
end;
theorem Th40:
for S be non empty compact TopSpace,T be NormedLinearTopSpace holds
(the carrier of S) --> 0.T = 0.R_NormSpace_of_ContinuousFunctions(S,T)
proof
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
(the carrier of S)-->0.T = 0.R_VectorSpace_of_ContinuousFunctions(S,T)
by Th9;
hence thesis;
end;
theorem Th41:
for S be non empty compact TopSpace,T be NormedLinearTopSpace holds
0.R_NormSpace_of_ContinuousFunctions(S,T)
= 0.R_NormSpace_of_BoundedFunctions(the carrier of S,T)
proof
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
thus 0.R_NormSpace_of_ContinuousFunctions(S,T)
= (the carrier of S)-->0.T by Th40
.= 0.R_NormSpace_of_BoundedFunctions(the carrier of S,T) by RSSPACE4:15;
end;
theorem
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for F be Point of R_NormSpace_of_ContinuousFunctions(S,T)
holds 0 <= ||.F.||
proof
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
let F be Point of R_NormSpace_of_ContinuousFunctions(S,T);
reconsider F1=F as Point of
R_NormSpace_of_BoundedFunctions(the carrier of S,T) by Th34;
||.F.|| =||.F1.|| by FUNCT_1:49;
hence thesis;
end;
theorem
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for F be Point of R_NormSpace_of_ContinuousFunctions(S,T) holds
F = 0.R_NormSpace_of_ContinuousFunctions(S,T) implies 0 = ||.F.||
proof
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
let F be Point of R_NormSpace_of_ContinuousFunctions(S,T);
assume
A1: F = 0.R_NormSpace_of_ContinuousFunctions(S,T);
reconsider F1=F as Point of
R_NormSpace_of_BoundedFunctions(the carrier of S,T) by Th34;
A2:||.F.|| =||.F1.|| by FUNCT_1:49;
F= (the carrier of S)--> 0.T by A1,Th40; then
F1 = 0.R_NormSpace_of_BoundedFunctions(the carrier of S,T) by RSSPACE4:15;
hence thesis by A2;
end;
theorem Th44:
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for F,G,H being Point of R_NormSpace_of_ContinuousFunctions(S,T)
for f,g,h be Function of S,T holds
(f=F & g=G & h=H implies
(H = F+G iff for x be Element of S holds h.x = f.x + g.x))
proof
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
let F,G,H be Point of R_NormSpace_of_ContinuousFunctions(S,T);
let f,g,h be Function of S,T;
reconsider f1=F, g1=G, h1=H as VECTOR of
R_VectorSpace_of_ContinuousFunctions(S,T);
H=F+G iff h1=f1+g1;
hence thesis by Th7;
end;
theorem
for a be Real
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for F,G being Point of R_NormSpace_of_ContinuousFunctions(S,T)
for f,g being Function of S,T holds
(f=F & g=G implies ( G = a*F iff for x be Element of S holds g.x = a*f.x ))
proof
let a be Real;
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
let F,G be Point of R_NormSpace_of_ContinuousFunctions(S,T);
let f,g be Function of S,T;
reconsider f1=F, g1=G as VECTOR of R_VectorSpace_of_ContinuousFunctions(S,T);
G=a*F iff g1=a*f1;
hence thesis by Th8;
end;
theorem Th46:
for a being Real
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for F,G being Point of R_NormSpace_of_ContinuousFunctions(S,T) holds
( ||.F.|| = 0 iff F = 0.R_NormSpace_of_ContinuousFunctions(S,T)) &
(||.a*F.|| = |.a.| * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||)
proof
let a be Real;
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
let F,G be Point of R_NormSpace_of_ContinuousFunctions(S,T);
reconsider F1=F, G1=G as Point of
R_NormSpace_of_BoundedFunctions(the carrier of S,T) by Th34;
A1:||.F.|| = ||.F1.|| by FUNCT_1:49;
A2:||.G.|| = ||.G1.|| by FUNCT_1:49;
A3:||.F+G.|| = ||.F1+G1.|| by Th38,Th36;
||.F1.|| = 0 iff
F1=0.R_NormSpace_of_BoundedFunctions(the carrier of S,T)
by NORMSP_0:def 5;
hence ||.F.|| = 0 iff F = 0.R_NormSpace_of_ContinuousFunctions(S,T)
by FUNCT_1:49,Th41;
thus ||.a*F.|| = ||.a*F1.|| by Th39,Th36
.=|.a.| * ||.F1.|| by NORMSP_1:def 1
.=|.a.| * ||.F.|| by FUNCT_1:49;
thus ||.F+G.|| <= ||.F.|| + ||.G.|| by A1,A2,A3,NORMSP_1:def 1;
end;
registration
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
cluster R_NormSpace_of_ContinuousFunctions(S,T)
-> reflexive discerning RealNormSpace-like;
correctness by Th46;
end;
theorem Th47:
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for x1,x2 be Point of R_NormSpace_of_ContinuousFunctions(S,T),
y1,y2 be Point of R_NormSpace_of_BoundedFunctions(the carrier of S,T)
st x1=y1 & x2=y2 holds x1-x2=y1-y2
proof
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
let x1,x2 be Point of R_NormSpace_of_ContinuousFunctions(S,T),
y1,y2 be Point of R_NormSpace_of_BoundedFunctions(the carrier of S,T);
assume
A1: x1=y1 & x2=y2;
-x2=(-1)*x2 by RLVECT_1:16
.=(-1)*y2 by A1,Th39
.= -y2 by RLVECT_1:16;
hence x1-x2 =y1-y2 by A1,Th38;
end;
theorem
for S be non empty compact TopSpace,T be NormedLinearTopSpace
for F,G,H be Point of R_NormSpace_of_ContinuousFunctions(S,T)
for f,g,h be Function of S,T holds
f=F & g=G & h=H implies
(H = F-G iff (for x be Element of S holds h.x = f.x - g.x))
proof
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
let F,G,H be Point of R_NormSpace_of_ContinuousFunctions(S,T);
let f,g,h be Function of S,T;
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
A3: H+G=F-0.R_NormSpace_of_ContinuousFunctions(S,T) by RLVECT_1:15;
now let x be Element of S;
f.x -g.x = h.x + g.x -g.x by A1,A3,Th44;
hence f.x-g.x=h.x by RLVECT_4:1;
end;
hence for x be Element of S holds h.x = f.x - g.x;
end;
now assume
A4: for x be Element of S holds h.x = f.x - g.x;
now let x be Element of S;
h.x = f.x - g.x by A4;
hence h.x + g.x= f.x by RLVECT_4:1;
end; then
F=H+G by A1,Th44; then
F-G=H+(G-G) by RLVECT_1:def 3; then
F-G=H+0.R_NormSpace_of_ContinuousFunctions(S,T) by RLVECT_1:15;
hence F-G=H;
end;
hence thesis by A2;
end;
theorem Th49:
for S be non empty TopSpace,T be NormedLinearTopSpace,
H be Functional_Sequence of the carrier of S,the carrier of T,
LimH be Function of S,T
st H is_unif_conv_on (the carrier of S)
&
( for n be Nat holds
ex Hn be Function of S,T st Hn = H.n & Hn is continuous )
& LimH = lim(H,the carrier of S)
holds LimH is continuous
proof
let S be non empty TopSpace,
T be NormedLinearTopSpace,
H be Functional_Sequence of the carrier of S,the carrier of T,
LimH be Function of S,T;
assume that
A1: H is_unif_conv_on the carrier of S and
A2: for n be Nat holds
ex Hn be Function of S,T st Hn = H.n & Hn is continuous and
A3: LimH = lim(H,the carrier of S);
set X = the carrier of S;
A4: H is_point_conv_on X by A1,SEQFUNC2:33;
for x being Point of S holds LimH is_continuous_at x
proof
let x be Point of S;
for G being a_neighborhood of LimH . x
ex H being a_neighborhood of x st LimH .: H c= G
proof
let G be a_neighborhood of LimH . x;
consider r being Real such that
A5: r > 0
& { y where y is Point of T : ||.y-LimH.x .|| < r } c= G by Th30;
A6: 0 < r/3 by XREAL_1:222,A5;
reconsider r as Element of REAL by XREAL_0:def 1;
consider k be Nat such that
A7: for n be Nat for x1 being Element of S st n>=k & x1 in X holds
||.(H.n)/.x1-LimH/.x1.||<r/3 by A1,XREAL_1:222,A5,A3,SEQFUNC2:33;
consider k1 be Nat such that
A8: for n be Nat st n>=k1 holds ||.(H.n)/.x - LimH/.x.|| < r/3
by A4,A6,A3,SEQFUNC2:11;
reconsider m = max(k,k1) as Nat by XXREAL_0:def 10;
consider h be Function of S,T such that
A9: h = H.m & h is continuous by A2;
set W = { y where y is Point of T : ||.y-h.x .|| < r/3 };
now let z be object;
assume z in W; then
ex y be Point of T st z=y & ||.y-h.x .|| < r/3;
hence z in the carrier of T;
end; then
reconsider W as Subset of T by TARSKI:def 3;
W is a_neighborhood of h.x by XREAL_1:222,A5,Th30; then
consider H being a_neighborhood of x such that
A10: h.: H c= W by A9,TMAP_1:44,TMAP_1:def 2;
take H;
now let z be object;
assume z in LimH .: H; then
consider s be object such that
A11: s in the carrier of S & s in H & z=LimH .s by FUNCT_2:64;
reconsider s as Point of S by A11;
h.s in h.:H by A11,FUNCT_2:35; then
h.s in W by A10; then
A12: ex y be Point of T st y =h.s & ||.y-h.x .|| < r/3;
||.h/.s-LimH/.s .|| < r/3 by A7,A9,XXREAL_0:25; then
A13: ||.LimH/.s -h/.s.|| < r/3 by NORMSP_1:7;
A14: ||.h/.x - LimH/.x.|| < r/3 by A8,A9,XXREAL_0:25;
LimH.s-LimH.x = LimH.s - h/.s + h/.s -LimH.x by RLVECT_4:1
.= LimH.s - h/.s + (h/.s -LimH.x) by RLVECT_1:28
.= LimH.s - h/.s + (h/.s -h/.x + h/.x -LimH.x) by RLVECT_4:1
.= LimH.s - h/.s + (h/.s -h/.x + (h/.x -LimH.x)) by RLVECT_1:28;
then
A15: ||.LimH.s-LimH.x.|| <= ||.LimH.s - h/.s.||
+ ||.h/.s -h/.x + (h/.x -LimH.x).|| by NORMSP_1:def 1;
A16: ||.LimH.s - h/.s.|| + ||.h/.s -h/.x + (h/.x -LimH.x).||
< r/3 + ||.h/.s -h/.x + (h/.x -LimH.x).|| by XREAL_1:8,A13;
A17: ||.h/.s -h/.x + (h/.x -LimH.x).||
<= ||.h/.s -h/.x.|| + ||.(h/.x -LimH.x).|| by NORMSP_1:def 1;
||.h/.s -h/.x.|| + ||.(h/.x -LimH.x).||
< r/3 + r/3 by XREAL_1:8,A12,A14; then
||.h/.s -h/.x + (h/.x -LimH.x).|| < r/3 + r/3 by A17,XXREAL_0:2;
then
r/3 + ||.h/.s -h/.x + (h/.x -LimH.x).|| < r/3 + (r/3 + r/3)
by XREAL_1:8; then
||.LimH.s - h/.s.|| + ||.h/.s -h/.x + (h/.x -LimH.x).||
< r by A16,XXREAL_0:2; then
||.LimH.s-LimH.x .|| < r by A15,XXREAL_0:2;
then LimH.s in { y where y is Point of T : ||.y-LimH.x .|| < r };
hence z in G by A11,A5;
end;
hence LimH .: H c= G;
end;
hence thesis by TMAP_1:def 2;
end;
hence thesis by TMAP_1:44;
end;
theorem Th50:
for S be non empty compact TopSpace,T be NormedLinearTopSpace holds
for Y be Subset of the carrier of
R_NormSpace_of_BoundedFunctions(the carrier of S,T) st
Y = ContinuousFunctions(S,T) holds Y is closed
proof
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
let Y be Subset of the carrier of
R_NormSpace_of_BoundedFunctions(the carrier of S,T);
assume
A1: Y = ContinuousFunctions(S,T);
now let seq be sequence of
R_NormSpace_of_BoundedFunctions(the carrier of S,T);
assume
A2: rng seq c= Y & seq is convergent;
reconsider f = lim seq as bounded
Function of the carrier of S, the carrier of T
by RSSPACE4:def 5;
A3: dom f = the carrier of S by FUNCT_2:def 1;
now let z be object;
assume z in BoundedFunctions (the carrier of S,T); then
z is Function of the carrier of S, the carrier of T
by RSSPACE4:def 5;
hence z in PFuncs(the carrier of S, the carrier of T) by PARTFUN1:45;
end; then
BoundedFunctions (the carrier of S, T)
c= PFuncs(the carrier of S, the carrier of T); then
reconsider H = seq as Functional_Sequence of the carrier of S,
the carrier of T by FUNCT_2:7;
A4: for n being Nat holds the carrier of S c= dom (H . n)
proof
let n be Nat;
H.n in rng seq by ORDINAL1:def 12,FUNCT_2:4; then
H.n in Y by A2; then
consider f be Function of the carrier of S, the carrier of T such that
A5: H.n = f & f is continuous by A1;
thus thesis by A5,FUNCT_2:def 1;
end;
A6: for p being Real st p > 0 holds ex k being Nat st
for n being Nat for x be Element of the carrier of S
st n >= k & x in the carrier of S holds
||.(((H . n) /. x) - (f /. x)).|| < p
proof
let p be Real;
assume p > 0;
then consider k being Nat such that
A7: for n being 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 Nat;
let x be Element of S;
assume n >= k & x in the carrier of S; then
A8: ||.((seq . n) - (lim seq)).|| < p by A7;
reconsider g = (seq . n) - (lim seq) as bounded Function of
the carrier of S, the carrier of T by RSSPACE4:def 5;
reconsider s = seq . n as bounded Function of
the carrier of S, the carrier of T by RSSPACE4:def 5;
reconsider x0 = x as Element of the carrier of S;
A9: g . x0 = (s . x0) - (f . x0) by RSSPACE4:24;
A10: ||.(g . x0).|| <= ||.((seq . n) - (lim seq)).|| by RSSPACE4:16;
H.n in rng seq by ORDINAL1:def 12,FUNCT_2:4; then
H.n in Y by A2; then
ex f be Function of the carrier of S, the carrier of T
st H.n = f & f is continuous by A1; then
dom (H.n) = the carrier of S by FUNCT_2:def 1; then
(H.n).x = (H.n)/.x by PARTFUN1:def 6;
hence ||.(((H . n) /. x) - (f /. x)).|| < p by A9,A10,A8,XXREAL_0:2;
end;
end;
A12:for x be Element of the carrier of S
st x in the carrier of S holds
for p be Real st p > 0 ex k be Nat st for n be Nat st n>=k holds
||.(H.n)/.x - f/.x.|| < p
proof
let x be Element of the carrier of S;
assume x in the carrier of S;
let p be Real;
assume p > 0; then
consider k being Nat such that
A13: for n being Nat
for x be Element of the carrier of S
st n >= k & x in the carrier of S holds
||.(((H . n) /. x) - (f /. x)).|| < p by A6;
take k;
let n be Nat;
assume n>=k;
hence ||.(((H . n) /. x) - (f /. x)).|| < p by A13;
end; then
A14:H is_point_conv_on (the carrier of S) by A4,SEQFUNC:def 9,A3;
A15:H is_unif_conv_on (the carrier of S) by A3,A4,SEQFUNC:def 9,A6;
A16:lim(H,the carrier of S) = f by A3,A12,A14,SEQFUNC2:11;
for n be Nat holds
ex Hn be Function of S,T st Hn = (H.n) & Hn is continuous
proof
let n be Nat;
H.n in rng seq by ORDINAL1:def 12,FUNCT_2:4; then
H.n in Y by A2;then
consider f be Function of the carrier of S, the carrier of T such that
A17: H.n = f & f is continuous by A1;
thus thesis by A17;
end; then
f is continuous by Th49,A15,A16;
hence lim seq in Y by A1;
end;
hence thesis;
end;
theorem Th51:
for S be non empty compact TopSpace,
T be NormedLinearTopSpace st T is complete holds
for seq be sequence of R_NormSpace_of_ContinuousFunctions(S,T)
st seq is Cauchy_sequence_by_Norm holds seq is convergent
proof
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
assume A1: T is complete;
set Z = R_NormSpace_of_ContinuousFunctions(S,T);
let vseq be sequence of Z;
assume
A2: vseq is Cauchy_sequence_by_Norm;
A3:for x being object st x in ContinuousFunctions(S,T) holds
x in BoundedFunctions(the carrier of S,T) by Th34;
rng vseq c= BoundedFunctions(the carrier of S,T) by Th34; then
reconsider vseq1=vseq as sequence of
R_NormSpace_of_BoundedFunctions(the carrier of S,T) by FUNCT_2:6;
A4: now let e be Real;
assume e > 0; then
consider k be Nat such that
A6: for n,m be Nat st n >= k & m >= k holds
||. vseq.n - vseq.m .|| < e by A2,RSSPACE3:8;
take k;
let n,m be Nat;
assume n >= k & m >= k; then
||. vseq.n - vseq.m .|| < e by A6;
hence ||. vseq1.n - vseq1.m .|| < e by Th47,Th36;
end; then
A7:vseq1 is Cauchy_sequence_by_Norm by RSSPACE3:8;
A8: vseq1 is convergent by A1,RSSPACE4:25,A4,RSSPACE3:8;
reconsider Y = ContinuousFunctions(S,T) as Subset of
R_NormSpace_of_BoundedFunctions(the carrier of S,T) by A3,TARSKI:def 3;
A9:rng vseq c= Y;
Y is closed by Th50; then
reconsider tv=lim vseq1 as Point of Z by A1,A9,A7,C0SP2:20;
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
A10:for n be Nat st n >= k holds
||.vseq1.n - lim vseq1.|| < e by A8,NORMSP_1:def 7;
take k;
now
let n be Nat;
assume n >= k; then
||.vseq1.n-lim vseq1.|| < e by A10;
hence ||.vseq.n-tv.|| < e by Th47,Th36;
end;
hence for n be Nat st n >= k holds ||.vseq.n - tv.|| < e;
end;
hence thesis;
end;
theorem
for S be non empty compact TopSpace,
T be NormedLinearTopSpace st T is complete holds
R_NormSpace_of_ContinuousFunctions(S,T) is complete
proof
let S be non empty compact TopSpace,T be NormedLinearTopSpace;
set Z = R_NormSpace_of_ContinuousFunctions(S,T);
assume T is complete; then
for seq be sequence of Z st seq is Cauchy_sequence_by_Norm holds
seq is convergent by Th51;
hence thesis by LOPBAN_1:def 15;
end;
begin :: Some Properties of Support
definition
let X be ZeroStr;
let f be (the carrier of X)-valued Function;
func support f -> set means :Def10:
for x being object holds
x in it iff x in dom f & f /. x <> 0.X;
existence
proof
defpred S1[object] means $1 in dom f & f /. $1 <> 0.X;
consider A being set such that
A1: for x being object holds
x in A iff x in dom f & S1[x] from XBOOLE_0:sch 1;
take A;
let x be object;
thus x in A implies x in dom f & f /. x <> 0.X by A1;
assume x in dom f & f /. x <> 0.X;
hence x in A by A1;
end;
uniqueness
proof
let A, B be set;
assume that
A3: for x being object holds x in A iff x in dom f & f /. x <> 0.X and
A4: for x being object holds x in B iff x in dom f & f /. x <> 0.X;
for x being object holds x in A iff x in B
proof
let x be object;
x in A iff x in dom f & f /. x <> 0.X by A3;
hence x in A iff x in B by A4;
end;
hence A = B by TARSKI:2;
end;
end;
theorem
for X be ZeroStr,
f be (the carrier of X)-valued Function
holds support f c= dom f by Def10;
definition
let X be non empty TopSpace, T be RealLinearSpace;
let f be Function of X,T;
redefine func support f -> Subset of X; :: redefines support (C0SP3, definition)
correctness
proof
support f c= dom f by Def10;
hence thesis by FUNCT_2:def 1;
end;
end;
theorem Th54:
for X be non empty TopSpace, T be RealLinearSpace
for f,g be Function of X,T holds
support(f+g) c= support(f) \/ support(g)
proof
let X be non empty TopSpace,T be RealLinearSpace;
let f,g be Function of X,T;
set CX = the carrier of X;
reconsider h=f+g as Function of X,T;
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: (not x in dom f or f/.x = 0.T) & (not x in dom g or g/.x=0.T) by Def10;
A4: (f+g)/.x= 0.T+ 0.T by A3,A2,A1,VFUNCT_1:def 1;
not x in support(f+g) by A4,Def10;
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 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 XBOOLE_1:28;
hence thesis by XBOOLE_1:28;
end;
theorem Th55:
for X be non empty TopSpace,T be RealLinearSpace,
f be Function of X,T,
a be Real holds
support(a(#)f) c= support(f)
proof
let X be non empty TopSpace,T be RealLinearSpace;
let f be Function of X,T,
a be Real;
set CX = the carrier of X;
reconsider h=a(#)f as Function of X,T;
now let x be object;
assume x in support(a(#)f); then
A1: x in dom (a(#)f) & (a(#)f)/.x <>0.T by Def10; then
a*f/.x <> 0.T by VFUNCT_1:def 4; then
A3: f/.x <> 0.T;
x in dom f by A1,VFUNCT_1:def 4;
hence x in support(f) by A3,Def10;
end;
hence thesis;
end;
begin :: Space of Real-valued Continuous Functionals with Bounded Support
definition
let X be non empty TopSpace, T be NormedLinearTopSpace;
func C_0_Functions(X,T) -> non empty Subset of
RealVectSpace(the carrier of X,T) equals
{ f where f is Function of the carrier of X, the carrier of T :
f is continuous & ex Y be non empty Subset of X st Y is compact
& Cl support f c= Y };
correctness
proof
set CS = { f where f is Function of the carrier of X, the carrier of T :
f is continuous &
ex Y be non empty Subset of X st Y is compact
& Cl support(f) c= Y };
A1:CS c= Funcs(the carrier of X,the carrier of T)
proof
for x being object st x in CS
holds x in Funcs(the carrier of X,the carrier of T)
proof
let x be object;
assume x in CS; then
ex f be Function of the carrier of X,
the carrier of T st x=f & f is continuous
& ex Y be non empty Subset of X st Y is compact
& Cl(support(f)) c= Y;
hence x in Funcs(the carrier of X, the carrier of T) by FUNCT_2:8;
end;
hence thesis;
end;
CS is non empty
proof
set g = X --> 0.T;
reconsider g as Function of the carrier of X, the carrier of T;
ex Y be non empty Subset of X st Y is compact
& Cl(support(g)) c= Y
proof
set PX = the Point of X;
reconsider S = { PX } as non empty Subset of X;
reconsider K = S as Subset of X;
take S;
thus S is compact;
support(g)={}
proof
assume
A4: not thesis;
set p = the Element of support(g);
A5: p in support(g) by A4;
p in dom g & g/.p <> 0.T by A4,Def10; then
g.p <> 0.T by PARTFUN1:def 6;
hence contradiction by A5,FUNCOP_1:7;
end;
hence Cl(support(g)) c= S by PRE_TOPC:22;
end; then
g in CS;
hence thesis;
end;
hence thesis by A1;
end;
end;
theorem Th56:
for X be non empty TopSpace,T be NormedLinearTopSpace
for v,u be Element of RealVectSpace(the carrier of X,T)
st v in C_0_Functions(X,T) & u in C_0_Functions(X,T)
holds v + u in C_0_Functions(X,T)
proof
let X be non empty TopSpace,T be NormedLinearTopSpace;
set W = C_0_Functions(X,T);
set V = RealVectSpace(the carrier of X,T);
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, the carrier of T such that
A2: u1=u & u1 is continuous
& ex Y1 be non empty Subset of X st Y1 is compact
& Cl(support(u1)) c= Y1 by A1;
consider Y1 be non empty Subset of X such that
A3: Y1 is compact & Cl(support(u1)) c= Y1 by A2;
consider v1 be Function of the carrier of X, the carrier of T such that
A4: v1=v & v1 is continuous
& ex Y2 be non empty Subset of X st Y2 is compact
& Cl(support(v1)) c= Y2 by A1;
consider Y2 be non empty Subset of X such that
A5: Y2 is compact & Cl(support(v1)) c= Y2 by A4;
A6: ContinuousFunctions(X,T) is linearly-closed by Th5;
A7: u in ContinuousFunctions(X,T) by A2;
v in ContinuousFunctions(X,T) by A4; then
v + u in ContinuousFunctions(X,T) by A7,A6; then
consider fvu be Function of the carrier of X, the carrier of T such that
A9: v+u = fvu & fvu is continuous;
reconsider Y12 = Y1 \/ Y2 as non empty Subset of X;
A10:Y12 is compact by A3,A5,COMPTS_1:10;
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;
Cl(support(v1+u1)) c= Cl(support(u1) \/ support(v1)) by Th54,PRE_TOPC:19;
then
A12:Cl(support(v1+u1)) c= Cl(support(u1)) \/ Cl(support(v1)) by PRE_TOPC:20;
Cl(support(v1)) \/ Cl(support(u1)) c= Y1 \/ Y2 by A3,A5,XBOOLE_1:13; then
A13:Cl(support(v1+u1)) c= Y12 by A12;
A14:dom fvu = the carrier of X by FUNCT_2:def 1;
for x be Element of X st x in dom fvu
holds fvu/.x = v1/.x + u1/.x by LOPBAN_1:11,A9,A2,A4; then
fvu = v1+u1 by VFUNCT_1:def 1,A14,A11;
hence thesis by A9,A10,A13;
end;
theorem Th57:
for X be non empty TopSpace,T be NormedLinearTopSpace
for a be Real,u be Element of RealVectSpace(the carrier of X,T)
st u in C_0_Functions(X,T) holds a * u in C_0_Functions(X,T)
proof
let X be non empty TopSpace,T be NormedLinearTopSpace;
set W = C_0_Functions(X,T);
set V = RealVectSpace(the carrier of X,T);
let a be Real;
let u be Element of V;
assume u in W; then
consider u1 be Function of the carrier of X, the carrier of T such that
A2: u1=u & u1 is continuous
& ex Y1 be non empty Subset of X st Y1 is compact
& Cl(support(u1)) c= Y1;
consider Y1 be non empty Subset of X such that
A3: Y1 is compact & Cl(support(u1)) c=Y1 by A2;
A4: u in ContinuousFunctions(X,T) by A2;
ContinuousFunctions(X,T) is linearly-closed by Th5; then
a*u in ContinuousFunctions(X,T) by A4; then
consider fau be Function of the carrier of X, the carrier of T such that
A5: a*u = fau & fau is continuous;
A6: dom fau = the carrier of X by FUNCT_2:def 1;
A7: dom u1 = the carrier of X by FUNCT_2:def 1;
Cl(support(a(#)u1)) c= Cl(support(u1)) by Th55,PRE_TOPC:19; then
A8: Cl(support(a(#)u1)) c= Y1 by A3;
for x be Element of X st x in dom fau
holds fau/.x = a*u1/.x by LOPBAN_1:12,A2,A5;
then fau = a(#)u1 by VFUNCT_1:def 4,A7,A6;
hence thesis by A3,A8,A5;
end;
theorem
for X be non empty TopSpace,T be NormedLinearTopSpace holds
C_0_Functions(X,T) is linearly-closed by Th56,Th57;
registration
let X be non empty TopSpace,T be NormedLinearTopSpace;
cluster C_0_Functions(X,T) -> non empty linearly-closed;
correctness by Th56,Th57;
end;
definition
let X be non empty TopSpace,T be NormedLinearTopSpace;
func R_VectorSpace_of_C_0_Functions(X,T) -> RealLinearSpace equals
RLSStruct (# C_0_Functions(X,T),
Zero_(C_0_Functions(X,T), RealVectSpace(the carrier of X,T)),
Add_(C_0_Functions(X,T), RealVectSpace(the carrier of X,T)),
Mult_(C_0_Functions(X,T), RealVectSpace(the carrier of X,T)) #);
correctness by RSSPACE:11;
end;
theorem
for X be non empty TopSpace,T be NormedLinearTopSpace holds
R_VectorSpace_of_C_0_Functions(X,T)
is Subspace of RealVectSpace(the carrier of X,T) by RSSPACE:11;
theorem Th60:
for X be non empty TopSpace,T be NormedLinearTopSpace
for x being set st x in C_0_Functions(X,T) holds
x in BoundedFunctions(the carrier of X,T)
proof
let X be non empty TopSpace,T be NormedLinearTopSpace;
let x be set;
assume x in C_0_Functions(X,T); then
consider f be Function of the carrier of X, the carrier of T such that
A2: f=x & f is continuous
& ex Y be non empty Subset of X st Y is compact
& Cl(support(f)) c= Y;
consider Y be non empty Subset of X such that
A3: Y is compact & Cl(support(f)) c= Y by A2;
A4: dom f = the carrier of X by FUNCT_2:def 1; then
consider K be Real such that
A5: 0 <= K &
for x be Point of X st x in Y holds ||.f.x.|| <= K by A3,A2,Lm2;
for x being Element of X holds ||.f. x.|| <= K
proof
let x be Element of X;
A6: support(f) c= Cl support(f) by PRE_TOPC:18;
per cases;
suppose not x in Y; then
not x in support(f) by A3,A6; then
not x in dom f or f/.x = 0.T by Def10;
hence ||.f. x.|| <= K by A5,A4;
end;
suppose x in Y;
hence ||.f. x.|| <= K by A5;
end;
end; then
f is bounded by RSSPACE4:def 4,A5;
hence x in BoundedFunctions(the carrier of X,T) by RSSPACE4:def 5,A2;
end;
definition
let X be non empty TopSpace, T be NormedLinearTopSpace;
func C_0_FunctionsNorm(X,T) -> Function of (C_0_Functions(X,T)),REAL equals
(BoundedFunctionsNorm(the carrier of X,T)) | (C_0_Functions(X,T));
correctness
proof
C_0_Functions(X,T) c= BoundedFunctions(the carrier of X,T) by Th60;
hence thesis by FUNCT_2:32;
end;
end;
definition
let X be non empty TopSpace,T be NormedLinearTopSpace;
func R_Normed_Space_of_C_0_Functions (X,T) -> NORMSTR equals
NORMSTR (# C_0_Functions(X,T),
Zero_(C_0_Functions(X,T), RealVectSpace(the carrier of X,T)),
Add_(C_0_Functions(X,T), RealVectSpace(the carrier of X,T)),
Mult_(C_0_Functions(X,T), RealVectSpace(the carrier of X,T)),
C_0_FunctionsNorm(X,T) #);
correctness;
end;
registration
let X be non empty TopSpace,T be NormedLinearTopSpace;
cluster R_Normed_Space_of_C_0_Functions (X,T) -> strict non empty;
correctness;
end;
theorem
for X be non empty TopSpace, T be NormedLinearTopSpace
for x being set st x in C_0_Functions(X,T) holds
x in ContinuousFunctions(X,T)
proof
let X be non empty TopSpace,T be NormedLinearTopSpace;
let x be set;
assume x in C_0_Functions(X,T); then
consider f be Function of the carrier of X, the carrier of T such that
A2: f=x & f is continuous
& ex Y be non empty Subset of X st Y is compact
& Cl(support(f)) c= Y;
thus thesis by A2;
end;
theorem Th62:
for X be non empty TopSpace, T be NormedLinearTopSpace holds
0.R_VectorSpace_of_C_0_Functions(X,T) = X -->0.T
proof
let X be non empty TopSpace, T be NormedLinearTopSpace;
A1:R_VectorSpace_of_C_0_Functions(X,T) is
Subspace of RealVectSpace(the carrier of X,T) by RSSPACE:11;
0.RealVectSpace(the carrier of X,T) = X -->0.T;
hence thesis by A1,RLSUB_1:11;
end;
theorem Th63:
for X be non empty TopSpace,T be NormedLinearTopSpace holds
0.R_Normed_Space_of_C_0_Functions (X,T) = X --> 0.T
proof
let X be non empty TopSpace,T be NormedLinearTopSpace;
0.R_Normed_Space_of_C_0_Functions (X,T)
=0.R_VectorSpace_of_C_0_Functions(X,T)
.=X --> 0.T by Th62;
hence thesis;
end;
theorem Th64:
for X be non empty TopSpace,T be NormedLinearTopSpace
for x1,x2 be Point of R_Normed_Space_of_C_0_Functions (X,T),
y1,y2 be Point of R_NormSpace_of_BoundedFunctions(the carrier of X,T)
st x1=y1 & x2=y2 holds x1+x2=y1+y2
proof
let X be non empty TopSpace,T be NormedLinearTopSpace;
let x1,x2 be Point of R_Normed_Space_of_C_0_Functions (X,T),
y1,y2 be Point of R_NormSpace_of_BoundedFunctions(the carrier of X,T);
assume
A1: x1=y1 & x2=y2;
thus x1+x2 = ((the addF of RealVectSpace(the carrier of X,T))
||C_0_Functions(X,T)).([x1,x2]) by RSSPACE:def 8
.= (the addF of RealVectSpace(the carrier of X,T)).([x1,x2])
by FUNCT_1:49
.= ((the addF of RealVectSpace(the carrier of X,T))
|| (BoundedFunctions(the carrier of X,T)).([y1,y2])) by A1,FUNCT_1:49
.=y1+y2 by RSSPACE:def 8,RSSPACE4:6;
end;
theorem Th65:
for X be non empty TopSpace,T be NormedLinearTopSpace
for a be Real,x be Point of R_Normed_Space_of_C_0_Functions (X,T),
y be Point of R_NormSpace_of_BoundedFunctions(the carrier of X,T)
st x=y holds a*x=a*y
proof
let X be non empty TopSpace,T be NormedLinearTopSpace;
let a be Real, x be Point of R_Normed_Space_of_C_0_Functions (X,T),
y be Point of R_NormSpace_of_BoundedFunctions(the carrier of X,T);
assume
A1: x=y;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
thus a*x = ((the Mult of RealVectSpace(the carrier of X,T))
|[:REAL,(C_0_Functions(X,T)):]).([a,x]) by RSSPACE:def 9
.= (the Mult of RealVectSpace(the carrier of X,T)).([aa,x]) by FUNCT_1:49
.= ((the Mult of RealVectSpace(the carrier of X,T))
|[:REAL,(BoundedFunctions(the carrier of X,T)) :]).([aa,y]) by A1,FUNCT_1:49
.= a*y by RSSPACE:def 9,RSSPACE4:6;
end;
theorem Th66:
for a be Real
for X be non empty TopSpace,T be NormedLinearTopSpace
for F,G be Point of R_Normed_Space_of_C_0_Functions (X,T) holds
(||.F.|| = 0 iff F = 0.R_Normed_Space_of_C_0_Functions (X,T) ) &
||.a*F.|| = |.a.| * ||.F.|| & ||.F+G.|| <= ||.F.|| + ||.G.||
proof
let a be Real;
let X be non empty TopSpace,T be NormedLinearTopSpace;
let F,G be Point of R_Normed_Space_of_C_0_Functions (X,T);
A1:||.F.|| = 0 iff F = 0.R_Normed_Space_of_C_0_Functions (X,T)
proof
reconsider FB=F as
Point of R_NormSpace_of_BoundedFunctions(the carrier of X,T) by Th60;
A2: 0.R_Normed_Space_of_C_0_Functions (X,T) =X-->0.T by Th63;
||.FB.|| = 0 iff
FB = 0.R_NormSpace_of_BoundedFunctions(the carrier of X,T)
by RSSPACE4:21;
hence thesis by A2,RSSPACE4:15,FUNCT_1:49;
end;
A3:||.a*F.|| = |.a.| * ||.F.||
proof
reconsider FB=F as
Point of R_NormSpace_of_BoundedFunctions(the carrier of X,T) by Th60;
A4: ||.FB.||=||.F.|| by FUNCT_1:49;
A5: a*FB=a*F by Th65;
reconsider aFB=a*FB as Point of R_NormSpace_of_BoundedFunctions
(the carrier of X,T);
reconsider aF=a*F as Point of R_Normed_Space_of_C_0_Functions (X,T);
||.aFB.||=||.aF.|| by A5,FUNCT_1:49;
hence thesis by A4,RSSPACE4:21;
end;
||.F+G.|| <= ||.F.|| + ||.G.||
proof
reconsider FB=F,GB=G as
Point of R_NormSpace_of_BoundedFunctions(the carrier of X,T) by Th60;
A6: ||.FB.||=||.F.|| & ||.GB.||=||.G.|| by FUNCT_1:49;
FB+GB=F+G by Th64; then
||.FB+GB.||=||.F+G.|| by FUNCT_1:49;
hence thesis by A6,RSSPACE4:21;
end;
hence thesis by A1,A3;
end;
theorem
for X be non empty TopSpace,T be NormedLinearTopSpace holds
R_Normed_Space_of_C_0_Functions (X,T) is RealNormSpace-like by Th66;
registration
let X be non empty TopSpace,T be NormedLinearTopSpace;
cluster R_Normed_Space_of_C_0_Functions (X,T) ->
reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
coherence
proof
R_VectorSpace_of_C_0_Functions(X,T) is RealLinearSpace;
hence thesis by RSSPACE3:2,Th66;
end;
end;
theorem
for X be non empty TopSpace,T be NormedLinearTopSpace holds
R_Normed_Space_of_C_0_Functions (X,T) is RealNormSpace;