:: Ascoli-Arzela's Theorem
:: by Hiroshi Yamazaki , Keiichi Miyajima and Yasunari Shidama
::
:: Received June 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 ASCOLI, STRUCT_0, NUMBERS, PRE_TOPC, ORDINAL2, PCOMPS_1,
NORMSP_0, SUBSET_1, RCOMP_1, RELAT_1, XBOOLE_0, FUNCT_1, TARSKI, CARD_1,
ARYTM_3, ARYTM_1, REAL_1, FUNCT_2, ZFMISC_1, RSSPACE4, XXREAL_2,
XXREAL_0, NORMSP_1, NORMSP_2, REWRITE1, NAT_1, ORDINAL4, RSSPACE3, SEQ_2,
TMAP_1, ORDEQ_01, PARTFUN1, C0SP2, LOPBAN_1, METRIC_1, SETFAM_1,
FINSET_1, METRIC_6, SEQ_4, TBSP_1, TOPMETR4, BHSP_3, C0SP3, UPROOTS,
FINSEQ_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FUNCT_1, CARD_1,
ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSET_1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, XXREAL_2, SEQ_4, STRUCT_0, PCOMPS_1, TBSP_1,
RLVECT_1, NORMSP_0, NORMSP_1, NFCONT_1, PRE_TOPC, COMPTS_1, TOPS_2,
METRIC_1, TMAP_1, TOPMETR, RSSPACE3, LOPBAN_1, NORMSP_2, RSSPACE4,
NORMSP_3, TOPMETR4, C0SP3, METRIC_6, FINSEQ_1;
constructors RSSPACE3, COMPLEX1, PCOMPS_1, TBSP_1, NFCONT_1, TOPMETR, SEQ_4,
NORMSP_2, TMAP_1, TOPS_2, RSSPACE4, NORMSP_3, TOPMETR4, C0SP3, METRIC_6;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, XREAL_0, NUMBERS,
ORDINAL1, MEMBERED, VALUED_0, COMPTS_1, XXREAL_0, FUNCT_2, XXREAL_2,
TOPMETR, RELSET_1, WAYBEL_2, XCMPLX_0, TOPS_1, RSSPACE4, NORMSP_3, C0SP3,
TBSP_1, PCOMPS_1, CARD_1, NAT_1, FINSEQ_1, FINSET_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TBSP_1, TARSKI;
equalities ALGSTR_0, STRUCT_0, NORMSP_0, NORMSP_2, RSSPACE4, PCOMPS_1, C0SP3,
METRIC_1, FINSEQ_1;
expansions TARSKI, STRUCT_0, LOPBAN_1, XBOOLE_0, PRE_TOPC, TBSP_1;
theorems FUNCT_1, NFCONT_1, PARTFUN1, ZFMISC_1, TARSKI, XBOOLE_1, RSSPACE3,
RELAT_1, XREAL_0, XXREAL_0, NORMSP_1, NORMSP_2, FUNCT_2, XREAL_1,
RLVECT_1, TOPS_2, NAT_1, FINSEQ_3, XBOOLE_0, COMPTS_1, PRE_TOPC, SEQ_4,
PARTFUN2, ORDINAL1, TOPMETR4, TMAP_1, TOPMETR, RSSPACE4, RLVECT_4,
NORMSP_3, PCOMPS_1, C0SP3, SETFAM_1, METRIC_1, METRIC_6, FINSEQ_1;
schemes FUNCT_2, NAT_1;
begin :: Equicontinuousness and Equiboundedness of Continuous Functions
reserve S, T for RealNormSpace;
reserve F for Subset of Funcs(the carrier of S,the carrier of T);
definition
let X be non empty MetrSpace, Y be Subset of X;
func Cl Y -> Subset of X means :Def1:
ex Z be Subset of TopSpaceMetr X st Z = Y & it = Cl Z;
correctness
proof
reconsider Z = Y as Subset of TopSpaceMetr X;
Cl Z is Subset of X;
hence thesis;
end;
end;
theorem Th1:
for X be RealNormSpace,
Y be Subset of X,
Z be Subset of MetricSpaceNorm X
st Y = Z
holds Cl(Y) = Cl(Z)
proof
let X be RealNormSpace,
Y be Subset of X,
Z be Subset of MetricSpaceNorm X;
assume A1: Y =Z;
consider S be Subset of LinearTopSpaceNorm X such that
A2: Y = S & Cl Y = Cl S by NORMSP_3:def 1;
A3:the carrier of TopSpaceNorm X = the carrier of LinearTopSpaceNorm X
by NORMSP_2:def 4;
consider D be Subset of TopSpaceMetr MetricSpaceNorm X such that
A4: D = Z & Cl(Z) = Cl D by Def1;
for p being set st p in the carrier of LinearTopSpaceNorm X holds
( p in Cl D iff for G being Subset of LinearTopSpaceNorm X
st G is open & p in G holds S meets G )
proof
let p be set;
assume
A5: p in the carrier of LinearTopSpaceNorm X;
( for G being Subset of TopSpaceMetr MetricSpaceNorm X
st G is open & p in G holds D meets G )
iff
(for G being Subset of LinearTopSpaceNorm X
st G is open & p in G holds S meets G)
proof
hereby assume
A6:( for G being Subset of TopSpaceMetr MetricSpaceNorm X
st G is open & p in G holds D meets G );
let G be Subset of LinearTopSpaceNorm X;
assume A7: G is open & p in G;
reconsider G0 = G as Subset of TopSpaceMetr MetricSpaceNorm X
by NORMSP_2:def 4;
G0 is open & p in G0 by A7,A3,NORMSP_2:def 4;
hence S meets G by A6,A2,A4,A1;
end;
assume
A9: (for G being Subset of LinearTopSpaceNorm X
st G is open & p in G holds S meets G);
let G be Subset of TopSpaceMetr MetricSpaceNorm X;
assume A10: G is open & p in G;
reconsider G0 = G as Subset of LinearTopSpaceNorm X by NORMSP_2:def 4;
G0 is open & p in G0 by A10,A3,NORMSP_2:def 4;
hence D meets G by A9,A2,A4,A1;
end;
hence thesis by A5,PRE_TOPC:def 7,A3;
end;
hence thesis by A2,A4,PRE_TOPC:def 7,A3;
end;
registration
let X be non empty MetrSpace;
let H be non empty Subset of X;
cluster Cl(H) -> non empty;
correctness
proof
consider Z be Subset of TopSpaceMetr X such that
A1: Z = H & Cl(H) = Cl Z by Def1;
Z c= Cl(Z) by PRE_TOPC:18;
hence thesis by A1;
end;
end;
theorem Th2:
for S be TopSpace,
F be FinSequence of bool the carrier of S
st for i be Nat st i in Seg len F
holds F/.i is compact
holds
union rng F is compact
proof
let S be TopSpace;
let F be FinSequence of bool the carrier of S;
assume A1: for i be Nat st i in Seg len F holds F/.i is compact;
defpred P[Nat] means
for F be FinSequence of bool the carrier of S
st len F = $1 &
for i be Nat st i in Seg len F
holds F/.i is compact holds union rng F is compact;
A2:P[0]
proof
let F be FinSequence of bool the carrier of S;
assume A3:len F = 0 &
for i be Nat st i in Seg len F holds F/.i is compact;
dom F = {} by A3,FINSEQ_1:def 3; then
union rng F = {} by ZFMISC_1:2,RELAT_1:42;
hence union rng F is compact;
end;
A4:for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A5: P[i];
let F be FinSequence of bool the carrier of S;
assume A6:len F = i+1 &
for i be Nat st i in Seg len F holds F/.i is compact;
i+1 in Seg (i+1) by FINSEQ_1:4; then
A7: i+1 in dom F by A6,FINSEQ_1:def 3;
A8: F = (F|i) ^ <*F.(i+1)*> by A6,FINSEQ_3:55;
A9:i <= i + 1 by NAT_1:11;
A10: len (F|i) = i by A6,FINSEQ_1:59,NAT_1:11; then
A11:dom (F|i) = Seg i by FINSEQ_1:def 3;
for k be Nat st k in Seg len (F|i) holds (F|i)/.k is compact
proof
let k be Nat;
assume
A12: k in Seg len (F|i); then
A13: k in Seg (i+1) by A10,A9,FINSEQ_1:5,TARSKI:def 3; then
A14: k in dom F by A6,FINSEQ_1:def 3;
(F|i)/.k = (F|i).k by A11,A12,A10,PARTFUN1:def 6
.=F.k by A12,A10,FUNCT_1:49
.=F/.k by PARTFUN1:def 6,A14;
hence (F|i)/.k is compact by A6,A13;
end; then
A15: union rng (F|i) is compact by A5,A10;
rng F = rng (F|i) \/ rng <*F.(i+1)*> by FINSEQ_1:31,A8
.= rng (F|i) \/ {F.(i+1) } by FINSEQ_1:39
.= rng (F|i) \/ {F/.(i+1) } by PARTFUN1:def 6,A7; then
A16:union rng F = (union rng (F|i)) \/ union {F/.(i+1) } by ZFMISC_1:78
.= (union rng ( F|i )) \/ (F/.(i+1)) by ZFMISC_1:25;
F/.(i+1) is compact by A6,FINSEQ_1:4;
hence thesis by A16,A15,COMPTS_1:10;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A2,A4);
hence thesis by A1;
end;
theorem Th3:
for S be non empty TopSpace,T be NormedLinearTopSpace,
f be Function of S,T,
x be Point of S holds
( f is_continuous_at x
iff
for e be Real
st 0 < e
holds ex H being Subset of S st
( H is open & x in H
&
for y be Point of S
st y in H holds ||.f.x-f.y.|| < e ) )
proof
let S be non empty TopSpace,T be NormedLinearTopSpace,
f be Function of S,T,
x be Point of S;
hereby assume
A1:f is_continuous_at x;
let e be Real;
assume A2: 0 < e;
set V = { y where y is Point of T : ||.f.x - y.|| < e };
now let z be object;
assume z in V; then
ex y be Point of T st z=y & ||.f.x - y.|| < e;
hence z in the carrier of T;
end; then
reconsider V as Subset of T by TARSKI:def 3;
||.f.x - f.x.|| < e by NORMSP_1:6,A2; then
f.x in V; then
consider H being Subset of S such that
A3: H is open & x in H & f .: H c= V by A1,TMAP_1:43,C0SP3:24;
take H;
thus H is open by A3;
thus x in H by A3;
let y be Point of S;
assume y in H; then
f.y in f.:H by FUNCT_2:35; then
f.y in V by A3; then
ex z be Point of T st z=f.y & ||.f.x - z.|| < e;
hence ||.f.x - f.y.|| < e;
end;
assume
A4: for e be Real st 0 < e
holds ex H being Subset of S st
( H is open & x in H & for y be Point of S
st y in H holds ||.f.x-f.y.|| < e );
for G being Subset of T st G is open & f . x in G holds
ex H being Subset of S st
H is open & x in H & f .: H c= G
proof
let G be Subset of T;
assume G is open & f . x in G; then
consider r being Real such that
A5: r > 0
& { y where y is Point of T : ||. f.x - y .|| < r } c= G by C0SP3:23;
consider H being Subset of S such that
A6: H is open & x in H &
for y be Point of S
st y in H holds ||.f.x-f.y.|| < r by A4,A5;
take H;
thus H is open by A6;
thus x in H by A6;
now let z be object;
assume z in f .: H; then
consider t being object such that
A7: t in dom f & t in H & z = f . t by FUNCT_1:def 6;
reconsider t as Point of S by A7;
||.f.x-f.t.|| < r by A7,A6; then
z in { y where y is Point of T : ||. f.x - y .|| < r } by A7;
hence z in G by A5;
end;
hence f .: H c= G;
end;
hence f is_continuous_at x by TMAP_1:43;
end;
theorem Th4:
for S be non empty MetrSpace,
V be non empty compact TopSpace,
T be NormedLinearTopSpace,
f be Function of V,T
st V = TopSpaceMetr(S)
holds
f is continuous
iff
for e be Real
st 0 < e
holds ex d be Real
st 0 < d
& for x1,x2 be Point of S
st dist(x1,x2) < d holds ||.f/.x1-f/.x2.|| < e
proof
let S be non empty MetrSpace,
V be non empty compact TopSpace,
T be NormedLinearTopSpace,
f be Function of V,T;
assume A1: V = TopSpaceMetr(S);
hereby assume
A2: f is continuous;
let e be Real;
assume
A3: 0 < e;
A4: [#]TopSpaceMetr(S) is compact by A1,COMPTS_1:1;
defpred P[Element of S,Real] means
0 < $2 &
for x be Point of S st dist(x,$1) < $2
holds ||.f/.x-f/.$1.|| < e/2;
A5: for x0 being Element of the carrier of S
ex d being Element of REAL st P[x0,d]
proof
let x0 be Element of the carrier of S;
reconsider xx0 = x0 as Point of V by A1;
consider H being Subset of V such that
A6: H is open & xx0 in H &
for y be Point of V
st y in H holds ||.f.xx0-f.y.|| < e/2
by A3,Th3,A2,TMAP_1:50;
consider d being Real such that
A7: d > 0 & Ball (x0,d) c= H by A1,PCOMPS_1:def 4,A6;
reconsider d as Element of REAL by XREAL_0:def 1;
take d;
for x be Point of S
st dist(x,x0) < d holds ||.f/.x-f/.x0.|| < e/2
proof
let x be Point of S;
assume dist(x,x0) < d; then
x in { y where y is Point of S : dist(x0,y) < d }; then
A8:x in Ball (x0,d) by METRIC_1:def 14;
reconsider y=x as Point of V by A1;
A9: ||.f.xx0-f.y.|| < e/2 by A6,A8,A7;
f.xx0 = f/.xx0 & f.y = f/.y;
hence ||.f/.x-f/.x0.|| < e/2 by A9,NORMSP_1:7;
end;
hence thesis by A7;
end;
consider D being Function of the carrier of S,REAL such that
A10: for x0 being Element of the carrier of S
holds P[x0,D . x0] from FUNCT_2:sch 3(A5);
set CV = the set of all Ball (x0,(D.x0)/2)
where x0 is Element of S;
CV c= bool the carrier of TopSpaceMetr S
proof
let z be object;
assume z in CV; then
consider x0 be Point of S such that
A11: z = Ball (x0,(D.x0)/2);
thus z in bool the carrier of TopSpaceMetr S by A11;
end; then
reconsider CV as Subset-Family of TopSpaceMetr S;
for P being Subset of TopSpaceMetr S st P in CV holds P is open
proof
let P be Subset of TopSpaceMetr S;
assume P in CV; then
consider x0 be Point of S such that
A12: P = Ball (x0,(D.x0)/2);
thus P is open by A12,PCOMPS_1:29;
end; then
A13: CV is open by TOPS_2:def 1;
the carrier of TopSpaceMetr S c= union CV
proof
let z be object;
assume z in the carrier of TopSpaceMetr S; then
reconsider x0=z as Point of S;
A14:Ball(x0,(D.x0)/2) in CV;
0 < (D.x0)/2 by A10,XREAL_1:215; then
dist(x0,x0) < (D.x0)/2 by METRIC_1:1; then
x0 in { y where y is Element of S : dist (x0,y) < (D.x0)/2 }; then
x0 in Ball(x0,(D.x0)/2) by METRIC_1:def 14;
hence z in union CV by TARSKI:def 4,A14;
end; then
consider G being Subset-Family of TopSpaceMetr S such that
A17: G c= CV & G is Cover of [#] (TopSpaceMetr S) & G is finite
by COMPTS_1:def 4,A4,A13,SETFAM_1:def 11;
defpred P1[object,object] means
ex x0 be Point of S st
$2 = x0 & $1 =Ball(x0,(D.x0)/2);
A18: for Z be object st Z in G
ex x0 be object st x0 in the carrier of S & P1[Z,x0]
proof
let Z be object;
assume Z in G; then
Z in CV by A17; then
consider x0 be Point of S such that
A19: Z = Ball(x0,(D.x0)/2);
take x0;
thus thesis by A19;
end;
consider H being Function of G,the carrier of S such that
A20: for Z being object st Z in G
holds P1[Z,H.Z] from FUNCT_2:sch 1(A18);
A21:for Z being object st Z in G holds Z = Ball(H/.Z,(D.(H.Z))/2)
proof
let Z be object;
assume A22: Z in G; then
A23: ex x0 be Point of S st H.Z = x0 &
Z = Ball(x0,(D.x0)/2) by A20;
dom H = G by FUNCT_2:def 1;
hence Z = Ball(H/.Z,(D.(H.Z))/2) by A23,A22,PARTFUN1:def 6;
end;
A24: dom H = G by FUNCT_2:def 1;
reconsider D0 = D.: (rng H) as finite Subset of REAL by A17;
A25:dom D = the carrier of S by FUNCT_2:def 1;
G <> {}
proof
assume G = {}; then
the carrier of TopSpaceMetr S c= {} by ZFMISC_1:2,A17,SETFAM_1:def 11;
hence contradiction;
end; then
consider xx be object such that
A26: xx in G by XBOOLE_0:def 1;
rng H <> {} by A24,A26,FUNCT_1:3; then
consider xx be object such that
A27: xx in rng H by XBOOLE_0:def 1;
reconsider xx as Point of S by A27;
set d0 = lower_bound D0;
A28: for r be Real st r in D0 holds d0 <= r by SEQ_4:def 2;
d0 in D0 by SEQ_4:133,A27; then
consider xx being object such that
A29: xx in dom D & xx in rng H & d0 = D . xx by FUNCT_1:def 6;
reconsider xx as Point of S by A29;
A30:0 < d0 by A29,A10;
reconsider d=d0/2 as Real;
take d;
thus 0 < d by A30;
thus for x1,x2 be Point of S
st dist(x1,x2) < d holds ||.f/.x1-f/.x2.|| < e
proof
let x1,x2 be Point of S;
assume A31: dist(x1,x2) < d;
x1 in union G by A17,SETFAM_1:def 11,TARSKI:def 3; then
consider X1 be set such that
A32: x1 in X1 & X1 in G by TARSKI:def 4;
A33: X1 = Ball(H/.X1,(D.(H.X1))/2) by A21,A32;
A34: (D.(H/.X1))/2 < D.(H/.X1) by A10,XREAL_1:216;
x1 in { y where y is Point of S : dist(H/.X1,y) < (D.(H.X1))/2 }
by A33,A32,METRIC_1:def 14; then
A35: ex y be Point of S st y=x1 & dist(H/.X1,y) < (D.(H.X1))/2; then
dist(x1,H/.X1) < (D.(H/.X1))/2 by A24,PARTFUN1:def 6,A32; then
dist(x1,H/.X1) < (D.(H/.X1)) by A34,XXREAL_0:2; then
A36: ||.f/.x1-f/.(H/.X1).|| < e/2 by A10;
A37: H.X1 in rng H by A24,A32,FUNCT_1:3;
H/.X1 in dom D by A25; then
H.X1 in dom D by A24,A32,PARTFUN1:def 6; then
(D.(H.X1)) in D0 by FUNCT_1:def 6,A37; then
d0/2 <= (D.(H.X1))/2 by A28,XREAL_1:72; then
A38: dist(x1,x2) < (D.(H.X1))/2 by A31,XXREAL_0:2;
A39: dist(x2,H/.X1) <= dist(x1,x2)+ dist(H/.X1,x1) by METRIC_1:4;
dist(x1,x2)+ dist(H/.X1,x1) < (D.(H.X1))/2 +(D.(H.X1))/2
by A38,A35, XREAL_1:8; then
A40: dist(x2,H/.X1) < D.(H.X1) by A39,XXREAL_0:2;
dist(x2,H/.X1) < (D.(H/.X1)) by PARTFUN1:def 6,A24,A40,A32; then
A41: ||.f/.x2-f/.(H/.X1).|| < e/2 by A10;
f/.x1-f/.x2 = f/.x1-f/.(H/.X1)+f/.(H/.X1)-f/.x2 by RLVECT_4:1
.= f/.x1-f/.(H/.X1)+ (f/.(H/.X1)-f/.x2) by RLVECT_1:28; then
||.f/.x1-f/.x2.|| <= ||.f/.x1-f/.(H/.X1).|| + ||.(f/.(H/.X1)-f/.x2).||
by NORMSP_1:def 1; then
A42:||.f/.x1-f/.x2.|| <= ||.f/.x1-f/.(H/.X1).|| +||.f/.x2-f/.(H/.X1).||
by NORMSP_1:7;
||.f/.x1-f/.(H/.X1).|| +||.f/.x2-f/.(H/.X1).||
< e/2 + e/2 by A41,A36,XREAL_1:8;
hence ||.f/.x1-f/.x2.|| < e by A42,XXREAL_0:2;
end;
end;
assume A43:
for e be Real st 0 < e
holds ex d be Real
st 0 < d
& for x1,x2 be Point of S
st dist(x1,x2) < d holds ||.f/.x1-f/.x2.|| < e;
for x being Point of V holds f is_continuous_at x
proof
let x be Point of V;
now let e be Real;
assume A44: 0 < e;
reconsider x0=x as Point of S by A1;
consider d be Real such that
A45: 0 < d & for x1,x2 be Point of S
st dist(x1,x2) < d holds ||.f/.x1-f/.x2.|| < e by A44,A43;
reconsider H = Ball (x0,d) as Subset of V by A1;
take H;
thus H is open by A1,PCOMPS_1:29;
dist(x0,x0) < d by A45,METRIC_1:1;
hence x in H by METRIC_1:11;
thus for y be Point of V st y in H holds ||.f.x-f.y.|| < e
proof
let y be Point of V;
assume y in H; then
y in { t where t is Point of S : dist(x0,t) < d } by METRIC_1:def 14; then
A46: ex t be Point of S st y=t & dist(x0,t) < d;
reconsider y0 =y as Point of S by A1;
dom f = the carrier of S by A1,FUNCT_2:def 1; then
f/.x0 = f.x0 & f/.y0 = f.y0 by PARTFUN1:def 6;
hence ||.f.x-f.y.|| < e by A45,A46;
end;
end;
hence f is_continuous_at x by Th3;
end;
hence f is continuous by TMAP_1:50;
end;
definition
let S be non empty MetrSpace,T be RealNormSpace;
let F be Subset of Funcs(the carrier of S,the carrier of T);
attr F is equibounded means
ex K be Real
st for f be Function of the carrier of S,the carrier of T
st f in F
holds
for x be Element of S
holds
||.f.x.|| <= K;
end;
definition
let S be non empty MetrSpace, T be RealNormSpace;
let F be Subset of Funcs(the carrier of S,the carrier of T);
let x0 be Point of S;
pred F is_equicontinuous_at x0 means
for e be Real st 0 < e
ex d be Real st 0 < d &
for f be Function of the carrier of S,the carrier of T
st f in F
holds
for x be Point of S
st dist(x,x0) < d holds ||.f.x-f.x0.|| < e;
end;
definition
let S be non empty MetrSpace, T be RealNormSpace;
let F be Subset of Funcs(the carrier of S,the carrier of T);
attr F is equicontinuous means
for e be Real st 0 < e
ex d be Real st 0 < d &
for f be Function of the carrier of S,the carrier of T
st f in F
holds
for x1,x2 be Point of S
st dist(x1,x2) < d holds ||.f.x1-f.x2.|| < e;
end;
theorem Th5:
for S be non empty MetrSpace,
T be RealNormSpace,
F be Subset of Funcs(the carrier of S,the carrier of T)
st TopSpaceMetr(S) is compact
holds
F is equicontinuous
iff
for x be Point of S holds F is_equicontinuous_at x
proof
let S be non empty MetrSpace,
T be RealNormSpace,
F be Subset of Funcs(the carrier of S,the carrier of T);
assume A1: TopSpaceMetr(S) is compact;
hereby assume A2: F is equicontinuous;
thus for x be Point of S holds F is_equicontinuous_at x
proof
let x0 be Point of S;
let e be Real;
assume 0 < e; then
consider d be Real such that
A3: 0 < d &
for f be Function of the carrier of S,the carrier of T st f in F
holds
for x1,x2 be Point of S
st dist(x1,x2) < d holds ||.f.x1-f.x2.|| < e by A2;
take d;
thus 0 < d by A3;
let f be Function of the carrier of S,the carrier of T;
assume A4: f in F;
let x be Point of S;
assume dist(x,x0) < d;
hence ||.f.x-f.x0.|| < e by A3,A4;
end;
end;
assume
A5: for x be Point of S holds F is_equicontinuous_at x;
let e be Real;
assume
A6:0 < e;
A7: [#]TopSpaceMetr(S) is compact by A1,COMPTS_1:1;
defpred P[Element of S,Real] means
0 < $2 &
for f be Function of the carrier of S,the carrier of T st f in F
holds for x be Point of S st dist(x,$1) < $2
holds ||.f.x-f.$1.|| < e/2;
A8: for x0 being Element of the carrier of S
ex d being Element of REAL st P[x0,d]
proof
let x0 be Element of the carrier of S;
F is_equicontinuous_at x0 by A5; then
consider d be Real such that
A9: 0 < d &
for f be Function of the carrier of S,the carrier of T
st f in F holds
for x be Point of S
st dist(x,x0) < d holds ||.f.x-f.x0.|| < e/2 by A6;
reconsider d as Element of REAL by XREAL_0:def 1;
take d;
thus thesis by A9;
end;
consider D being Function of the carrier of S,REAL such that
A10: for x0 being Element of the carrier of S
holds P[x0,D . x0] from FUNCT_2:sch 3(A8);
set CV = the set of all Ball (x0,(D.x0)/2)
where x0 is Element of S;
CV c= bool the carrier of TopSpaceMetr S
proof
let z be object;
assume z in CV; then
consider x0 be Point of S such that
A11: z = Ball (x0,(D.x0)/2);
thus z in bool the carrier of TopSpaceMetr S by A11;
end; then
reconsider CV as Subset-Family of TopSpaceMetr S;
for P being Subset of TopSpaceMetr S st P in CV holds P is open
proof
let P be Subset of TopSpaceMetr S;
assume P in CV; then
consider x0 be Point of S such that
A12: P = Ball (x0,(D.x0)/2);
thus P is open by A12,PCOMPS_1:29;
end; then
A13: CV is open by TOPS_2:def 1;
the carrier of TopSpaceMetr S c= union CV
proof
let z be object;
assume z in the carrier of TopSpaceMetr S; then
reconsider x0=z as Point of S;
A14:Ball(x0,(D.x0)/2) in CV;
A15: 0 < (D.x0)/2 by A10,XREAL_1:215;
dist(x0,x0) < (D.x0)/2 by A15,METRIC_1:1; then
x0 in { y where y is Element of S : dist (x0,y) < (D.x0)/2 }; then
x0 in Ball(x0,(D.x0)/2) by METRIC_1:def 14;
hence z in union CV by TARSKI:def 4,A14;
end; then
consider G being Subset-Family of TopSpaceMetr S such that
A17: G c= CV & G is Cover of [#] (TopSpaceMetr S) & G is finite
by COMPTS_1:def 4,A7,A13,SETFAM_1:def 11;
defpred P1[object,object] means
ex x0 be Point of S st $2 = x0 & $1 =Ball(x0,(D.x0)/2);
A18: for Z be object st Z in G
ex x0 be object st x0 in the carrier of S & P1[Z,x0]
proof
let Z be object;
assume Z in G; then
Z in CV by A17; then
consider x0 be Point of S such that
A19: Z = Ball(x0,(D.x0)/2);
take x0;
thus thesis by A19;
end;
consider H being Function of G,the carrier of S such that
A20: for Z being object st Z in G
holds P1[Z,H.Z] from FUNCT_2:sch 1(A18);
A21:for Z being object st Z in G holds
Z= Ball(H/.Z,(D.(H.Z))/2)
proof
let Z be object;
assume A22: Z in G; then
A23: ex x0 be Point of S st H.Z = x0 & Z =Ball(x0,(D.x0)/2) by A20;
dom H = G by FUNCT_2:def 1;
hence Z = Ball(H/.Z,(D.(H.Z))/2) by A23,A22,PARTFUN1:def 6;
end;
A24: dom H = G by FUNCT_2:def 1;
reconsider D0 = D.: (rng H) as finite Subset of REAL by A17;
A25:dom D = the carrier of S by FUNCT_2:def 1;
G <> {}
proof
assume G = {}; then
the carrier of TopSpaceMetr S c= {} by ZFMISC_1:2,A17,SETFAM_1:def 11;
hence contradiction;
end; then
consider xx be object such that
A26: xx in G by XBOOLE_0:def 1;
rng H <> {} by A24,A26,FUNCT_1:3; then
consider xx be object such that
A27: xx in rng H by XBOOLE_0:def 1;
reconsider xx as Point of S by A27;
A28: D0 is bounded_below & lower_bound D0 in D0 by SEQ_4:133,A27;
set d0 = lower_bound D0;
consider xx being object such that
A29: xx in dom D & xx in rng H & d0 = D . xx by FUNCT_1:def 6,A28;
reconsider xx as Point of S by A29;
A30:0 < d0 by A29,A10;
take d=d0/2;
thus 0 < d by A30;
thus for f be Function of S,T
st f in F
for x1,x2 be Point of S
st dist(x1,x2) < d holds ||.f.x1-f.x2.|| < e
proof
let f be Function of S,T;
assume A31: f in F;
let x1,x2 be Point of S;
assume A32: dist(x1,x2) < d;
x1 in union G by A17,SETFAM_1:def 11,TARSKI:def 3; then
consider X1 be set such that
A33: x1 in X1 & X1 in G by TARSKI:def 4;
A34: X1 = Ball(H/.X1,(D.(H.X1))/2) by A21,A33;
A35: (D.(H/.X1))/2 < D.(H/.X1) by A10,XREAL_1:216;
x1 in { y where y is Point of S : dist(H/.X1,y) < (D.(H.X1))/2 }
by A34,A33,METRIC_1:def 14; then
A36:ex y be Point of S st y=x1 & dist(H/.X1,y) < (D.(H.X1))/2; then
dist(x1,H/.X1) < (D.(H/.X1))/2 by A24,PARTFUN1:def 6,A33; then
dist(x1,H/.X1) < (D.(H/.X1)) by A35,XXREAL_0:2; then
A37: ||.f.x1-f.(H/.X1).|| < e/2 by A10,A31;
A38: H.X1 in rng H by A24,A33,FUNCT_1:3;
H/.X1 in dom D by A25; then
H.X1 in dom D by A24,A33,PARTFUN1:def 6; then
(D.(H.X1)) in D0 by FUNCT_1:def 6,A38; then
d0 <= (D.(H.X1)) by SEQ_4:def 2; then
d0/2 <= (D.(H.X1))/2 by XREAL_1:72; then
A39: dist(x1,x2) < (D.(H.X1))/2 by A32,XXREAL_0:2;
A40: dist(x2,H/.X1) <= dist(x1,x2)+ dist(H/.X1,x1) by METRIC_1:4;
dist(x1,x2)+ dist(H/.X1,x1) < (D.(H.X1))/2 +(D.(H.X1))/2
by A39,A36,XREAL_1:8; then
dist(x2,H/.X1) < D.(H.X1) by A40,XXREAL_0:2; then
dist(x2,H/.X1) < (D.(H/.X1)) by PARTFUN1:def 6,A24,A33; then
A42: ||.f.x2-f.(H/.X1).|| < e/2 by A10,A31;
f.x1-f.x2 = f.x1-f.(H/.X1)+f.(H/.X1)-f.x2 by RLVECT_4:1
.= f.x1-f.(H/.X1)+ (f.(H/.X1)-f.x2) by RLVECT_1:28; then
||.f.x1-f.x2.|| <= ||.f.x1-f.(H/.X1).|| + ||.(f.(H/.X1)-f.x2).||
by NORMSP_1:def 1; then
A43:||.f.x1-f.x2.|| <= ||.f.x1-f.(H/.X1).|| +||.f.x2-f.(H/.X1).||
by NORMSP_1:7;
||.f.x1-f.(H/.X1).|| +||.f.x2-f.(H/.X1).||
< e/2 + e/2 by A42,A37,XREAL_1:8;
hence ||.f.x1-f.x2.|| < e by A43,XXREAL_0:2;
end;
end;
begin :: Ascoli-Arzela's Theorem
reserve S,Z for RealNormSpace;
reserve T for RealBanachSpace;
reserve F for Subset of Funcs(the carrier of S,the carrier of T);
theorem Th6:
for Z be RealNormSpace
holds
Z is complete iff MetricSpaceNorm Z is complete
proof
let Z be RealNormSpace;
set N = MetricSpaceNorm Z;
hereby assume A1:Z is complete;
for S2 being sequence of N st S2 is Cauchy holds
S2 is convergent
proof
let S2 be sequence of N;
assume A2: S2 is Cauchy;
reconsider seq2 = S2 as sequence of Z;
for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq2 . n) - (seq2 . m)).|| < r
proof
let r be Real;
assume r > 0; then
consider p being Nat such that
A3:for n, m being Nat st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r by A2;
take p;
let n, m be Nat;
assume p <= n & p <= m; then
dist ((S2 . n),(S2 . m)) < r by A3;
hence ||.((seq2 . n) - (seq2 . m)).|| < r by NORMSP_2:def 1;
end; then
A4: seq2 is convergent by A1,RSSPACE3:8;
reconsider L = lim seq2 as Point of N;
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((seq2 . n) - lim seq2).|| < r by A4,NORMSP_1:def 7;
then
S2 is_convergent_in_metrspace_to L by NORMSP_2:4;
hence S2 is convergent by METRIC_6:9;
end;
hence MetricSpaceNorm Z is complete;
end;
assume A5: MetricSpaceNorm Z is complete;
for seq2 be sequence of Z st seq2 is Cauchy_sequence_by_Norm
holds seq2 is convergent
proof
let seq2 be sequence of Z;
assume A6:seq2 is Cauchy_sequence_by_Norm;
reconsider S2= seq2 as sequence of N;
now let r be Real;
assume r > 0; then
consider p being Nat such that
A7: for n, m being Nat st p <= n & p <= m holds
||.((seq2 . n) - (seq2 . m)).|| < r by A6,RSSPACE3:8;
take p;
let n, m be Nat;
assume p <= n & p <= m; then
||.((seq2 . n) - (seq2 . m)).|| < r by A7;
hence dist ((S2 . n),(S2 . m)) < r by NORMSP_2:def 1;
end; then
S2 is Cauchy; then
S2 is convergent by A5;
hence seq2 is convergent by NORMSP_2:5;
end;
hence Z is complete;
end;
theorem Th7:
for Z be RealNormSpace,
H be non empty Subset of MetricSpaceNorm Z
st Z is complete
holds
(MetricSpaceNorm Z) | Cl(H) is complete
proof
let Z be RealNormSpace,
H be non empty Subset of MetricSpaceNorm Z;
assume A1: Z is complete;
reconsider F=H as non empty Subset of Z;
A2: Cl(F) = Cl(H) by Th1;
set N = (MetricSpaceNorm Z) | Cl(H);
A3: the carrier of N = Cl(H) by TOPMETR:def 2;
for S2 being sequence of N st S2 is Cauchy holds
S2 is convergent
proof
let S2 be sequence of N;
assume A4: S2 is Cauchy;
A5:rng S2 c= Cl(H) by A3;
rng S2 c= the carrier of MetricSpaceNorm Z by A3,XBOOLE_1:1; then
reconsider S1 = S2 as sequence of MetricSpaceNorm Z by FUNCT_2:6;
reconsider seq2 = S1 as sequence of Z;
A6: rng seq2 c= Cl(F) by Th1,A5;
for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq2 . n) - (seq2 . m)).|| < r
proof
let r be Real;
assume r > 0; then
consider p being Nat such that
A7:for n, m being Nat st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r by A4;
take p;
let n, m be Nat;
assume p <= n & p <= m; then
dist ((S2 . n),(S2 . m)) < r by A7; then
dist ((S1 . n),(S1 . m)) < r by TOPMETR:def 1;
hence ||.((seq2 . n) - (seq2 . m)).|| < r by NORMSP_2:def 1;
end; then
A8: seq2 is convergent by A1,RSSPACE3:8; then
lim seq2 in Cl(F) by NFCONT_1:def 3,A6; then
reconsider L = lim seq2 as Point of N by TOPMETR:def 2,A2;
reconsider L0 = L as Point of MetricSpaceNorm Z;
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((seq2 . n) - lim seq2).|| < r by A8,NORMSP_1:def 7; then
A9:S1 is_convergent_in_metrspace_to L0 by NORMSP_2:4;
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
dist ((S2 . n),L) < r
proof
let r be Real;
assume 0 < r; then
consider m being Nat such that
A10:for n being Nat st m <= n holds
dist ((S1 . n),L0) < r by METRIC_6:def 2,A9;
take m;
let n be Nat;
assume m <= n; then
dist ((S1 . n),L0) < r by A10;
hence dist ((S2 . n),L) < r by TOPMETR:def 1;
end;
hence S2 is convergent;
end;
hence thesis;
end;
theorem Th8:
for Z be RealNormSpace,
H be non empty Subset of MetricSpaceNorm Z
holds
(MetricSpaceNorm Z) | H is totally_bounded
iff (MetricSpaceNorm Z) | Cl(H) is totally_bounded
proof
let Z be RealNormSpace,
H be non empty Subset of MetricSpaceNorm Z;
reconsider F=H as non empty Subset of Z;
set K = Cl(H);
set M = MetricSpaceNorm Z;
consider D be Subset of TopSpaceMetr MetricSpaceNorm Z such that
A1: D = H & Cl(H) = Cl D by Def1;
A2: H c= K by A1,PRE_TOPC:18;
A3: the carrier of (M|H) = H by TOPMETR:def 2;
A4: the carrier of (M|K) = K by TOPMETR:def 2;
A5: Cl(F) = Cl(H) by Th1;
hereby assume A6:
M | H is totally_bounded;
for r being Real st r > 0 holds
ex L being Subset-Family of M | K st
L is finite & the carrier of M | K = union L
& for C being Subset of M | K st C in L holds
ex w being Element of M | K st C = Ball (w,r)
proof
let r be Real;
assume A7: r > 0; then
consider L0 being Subset-Family of M | H such that
A8: L0 is finite & the carrier of M | H = union L0
& for C being Subset of M | H st C in L0 holds
ex w being Element of M | H st C = Ball (w,r/2) by A6;
defpred P1[object,object]
means
ex w be Point of M | H
st
$2 = w &
$1 =Ball(w,r/2);
A9: for D be object st D in L0
ex w be object st w in the carrier of M | H & P1[D,w]
proof
let D be object;
assume A10: D in L0; then
reconsider D0=D as Subset of M|H;
consider w being Element of M|H such that
A11: D0 = Ball (w,r/2) by A8,A10;
take w;
thus w in the carrier of M|H & P1[D,w] by A11;
end;
consider U0 being Function of L0,the carrier of M|H such that
A12: for D being object
st D in L0
holds P1[D,U0.D] from FUNCT_2:sch 1(A9);
A13:for D being object st D in L0 holds
D= Ball(U0/.D,r/2)
proof
let D be object;
assume A14: D in L0; then
A15:ex x0 be Point of M|H st U0.D = x0 &
D =Ball(x0,r/2) by A12;
dom U0 = L0 by FUNCT_2:def 1;
hence D = Ball(U0/.D,r/2) by A15,A14,PARTFUN1:def 6;
end;
defpred P2[object,object] means
ex x be Point of (M | K) st $1 = x & $2 = Ball(x,r);
A16: for w be object st w in the carrier of (M | H)
ex B be object st B in bool (the carrier of M | K ) & P2[w,B]
proof
let w be object;
assume w in the carrier of (M | H); then
reconsider x=w as Point of (M | K) by A2,A3,TOPMETR:def 2;
Ball (x,r) in bool the carrier of (M | K);
hence thesis;
end;
consider B being Function of the carrier of M|H,
bool the carrier of M|K such that
A17: for x being object
st x in the carrier of M|H
holds P2[x,B.x] from FUNCT_2:sch 1(A16);
A19: dom U0 = L0 by FUNCT_2:def 1;
reconsider L = B.:rng U0 as Subset-Family of (M|K);
take L;
thus L is finite by A8;
the carrier of M | K c= union L
proof
let z be object;
assume
A20: z in the carrier of M | K; then
consider seq being sequence of Z such that
A21: rng seq c= F & seq is convergent & lim seq = z by A4,A5,NORMSP_3:6;
consider N be Nat such that
A22: for n be Nat st
N<=n holds ||.seq.n-lim seq.|| < r/2 by NORMSP_1:def 7,A21,A7;
A23: ||.seq.N-lim seq.|| < r/2 by A22;
A24: dom seq = NAT & N in NAT by FUNCT_2:def 1,ORDINAL1:def 12; then
seq.N in H by A21,FUNCT_1:3; then
consider D be set such that
A25: seq.N in D & D in L0 by A8,A3,TARSKI:def 4;
reconsider y0 = seq.N as Point of (M|H) by A24,A21,FUNCT_1:3,A3;
A26: D = Ball(U0/.D,r/2) by A13,A25;
y0 in { y where y is Point of (M|H) : dist(U0/.D,y) < r/2 }
by METRIC_1:def 14,A25,A26; then
A27:ex y be Point of (M|H) st y0=y & dist(U0/.D,y) < r/2;
reconsider y01 =y0 as Point of M;
reconsider u0d1 =U0/.D as Point of M by TOPMETR:def 1,TARSKI:def 3;
A28: dist(u0d1,y01) < r/2 by A27,TOPMETR:def 1;
U0/.D in H by A3; then
reconsider u0d = U0/.D as Point of Z;
A29: ||.u0d-seq.N.|| < r/2 by A28,NORMSP_2:def 1;
u0d-lim seq = u0d-seq.N +seq.N -lim seq by RLVECT_4:1
.= u0d-seq.N +(seq.N -lim seq) by RLVECT_1:28; then
A30: ||.u0d-lim seq.|| <= ||.u0d-seq.N.|| + ||.seq.N-lim seq.||
by NORMSP_1:def 1;
||.u0d-seq.N.|| + ||.seq.N-lim seq.||
< r/2 +r/2 by XREAL_1:8,A29,A23; then
A31: ||.u0d-lim seq.|| < r by A30,XXREAL_0:2;
reconsider w =U0/.D as Point of (M|K) by A2,A3,A4;
reconsider v =lim seq as Point of (M|K) by A21,A20;
reconsider v1 = v as Point of M;
dist(u0d1,v1) < r by A31,NORMSP_2:def 1; then
dist(w,v) < r by TOPMETR:def 1; then
v in { y where y is Point of (M|K) : dist(w,y) < r }; then
A32: v in Ball(w,r) by METRIC_1:def 14;
A33: ex w being Point of M|K st U0/.D=w & B.(U0/.D) = Ball(w,r) by A17;
U0/.D in rng U0 by PARTFUN2:2,A25,A19; then
Ball(w,r) in L by A33,FUNCT_2:35;
hence z in union L by A21,A32,TARSKI:def 4;
end;
hence the carrier of M | K = union L;
thus for C being Subset of M | K st C in L holds
ex w being Element of M | K st C = Ball (w,r)
proof
let C be Subset of M | K;
assume C in L; then
consider x being Element of (M|H) such that
A35: x in rng U0 & C=B.x by FUNCT_2:65;
ex w being Point of M|K st x=w & B.x = Ball(w,r) by A17;
hence thesis by A35;
end;
end;
hence (MetricSpaceNorm Z) | K is totally_bounded;
end;
assume A37: (MetricSpaceNorm Z) | K is totally_bounded;
thus (MetricSpaceNorm Z) | H is totally_bounded
proof
let r be Real;
assume r > 0;
then consider L0 being Subset-Family of M | K such that
A38: L0 is finite & the carrier of M | K = union L0 &
for C being Subset of M | K st C in L0 holds
ex w being Element of M | K st C = Ball (w,r/2) by A37;
A39: for x be object
st x in H holds ex B be Subset of M | K
st x in B & B in L0
proof
assume not for x be object
st x in H holds ex B be Subset of M | K
st x in B & B in L0; then
consider x be object such that
A40: x in H & not (ex B be Subset of M | K st x in B & B in L0 );
not x in union L0
proof
assume x in union L0; then
consider D be set such that
A41: x in D & D in L0 by TARSKI:def 4;
reconsider D as Subset of (M|K) by A41;
thus contradiction by A41,A40;
end;
hence contradiction by A2,A40,A4,A38;
end;
set BL = {B where B is Subset of M | K: B in L0 & H /\ B <> {}};
consider x be object such that
A42: x in H by XBOOLE_0:def 1;
consider B be Subset of M | K such that
A43: x in B & B in L0 by A39,A42;
B /\ H <> {} by A42,A43,XBOOLE_0:def 4; then
A44:B in BL by A43;
BL c= L0
proof
let x be object;
assume x in BL; then
ex B be Subset of M | K st B = x & B in L0 & H /\ B <> {};
hence x in L0;
end; then
reconsider BL as non empty finite set by A44,A38;
defpred P1[object,object] means
ex w be Point of M | H,B be Subset of M | K st
B = $1 &
w in B & B in L0 &
$2=Ball(w,r);
A45: for D be object st D in BL
ex w be object st w in bool the carrier of M | H & P1[D,w]
proof
let D be object;
assume D in BL; then
consider B be Subset of M | K such that
A46: B = D & B in L0 & H /\ B <> {};
consider x be object such that
A47: x in H /\ B by XBOOLE_0:def 1,A46;
A48: x in H & x in B by XBOOLE_0:def 4,A47;
reconsider x as Point of (M|H) by A3,XBOOLE_0:def 4,A47;
set Z =Ball(x,r);
P1[D,Z] by A46,A48;
hence thesis;
end;
consider U0 being Function of BL,bool the carrier of M|H such that
A49: for D being object
st D in BL
holds P1[D,U0.D] from FUNCT_2:sch 1(A45);
set L = rng U0;
A50: dom U0 = BL by FUNCT_2:def 1;
reconsider L as Subset-Family of (M|H);
take L;
thus L is finite;
the carrier of M | H c= union L
proof
let z be object;
assume A51: z in the carrier of M | H; then
consider B be Subset of M | K such that
A52: z in B & B in L0 by A39,A3;
z in H /\ B by A51,A3,A52,XBOOLE_0:def 4; then
A53: B in BL by A52; then
consider w be Point of M | H,D be Subset of M | K such that
A54: D = B & w in D & D in L0 &
U0.B=Ball(w,r) by A49;
consider y being Element of M | K such that
A55: D = Ball (y,r/2) by A54,A38;
reconsider x =z as Point of (M | H) by A51;
reconsider x1=x,w1=w as Point of M | K by A52,A54;
reconsider x2=x1,w2=w1 as Point of M by TOPMETR:def 1,TARSKI:def 3;
x1 in { s where s is Point of (M|K) : dist(y,s) < r/2 }
by METRIC_1:def 14,A52,A54,A55; then
A56:ex s be Point of (M|K) st x1=s & dist(y,s) < r/2;
w1 in { s where s is Point of (M|K) : dist(y,s) < r/2 }
by METRIC_1:def 14,A54,A55; then
A57: ex s be Point of (M|K) st w1=s & dist(y,s) < r/2;
A58:dist(w1,x1) <= dist(w1,y) + dist(y,x1) by METRIC_1:4;
dist(w1,y) + dist(y,x1) < r/2+r/2 by A57,A56,XREAL_1:8; then
dist(w1,x1) < r by A58,XXREAL_0:2; then
dist(w2,x2) < r by TOPMETR:def 1; then
dist(w,x) < r by TOPMETR:def 1; then
x in { s where s is Point of (M|H) : dist(w,s) < r }; then
A59: z in U0.B by A54,METRIC_1:def 14;
U0.B in rng U0 by A53,A50,FUNCT_1:def 3;
hence z in union L by A59,TARSKI:def 4;
end;
hence the carrier of M | H = union L;
thus for C being Subset of M | H st C in L holds
ex w being Element of M | H st C = Ball (w,r)
proof
let C be Subset of M | H;
assume C in L; then
consider x being object such that
A61: x in dom U0 & C=U0.x by FUNCT_1:def 3;
ex w be Point of M | H,B be Subset of M | K st
B = x & w in B & B in L0 & U0.x=Ball(w,r) by A49,A61;
hence thesis by A61;
end;
end;
end;
theorem Th9:
for Z be RealNormSpace,
F be non empty Subset of Z,
H be non empty Subset of MetricSpaceNorm Z
st Z is complete & H = F
& (MetricSpaceNorm Z) | H is totally_bounded
holds
Cl(H) is sequentially_compact
&
(MetricSpaceNorm Z) | Cl(H) is compact
&
Cl(F) is compact
proof
let Z be RealNormSpace,
F be non empty Subset of Z,
H be non empty Subset of MetricSpaceNorm Z;
set K = Cl(H);
set M = MetricSpaceNorm Z;
assume A1: Z is complete & H = F & M | H is totally_bounded; then
A2: Cl(H) = Cl(F) by Th1;
(MetricSpaceNorm Z) | K is complete by Th7,A1; then
K is sequentially_compact by TOPMETR4:17,A1,Th8;
hence thesis by TOPMETR4:14,TOPMETR4:18,A2;
end;
theorem
for Z be RealNormSpace,
F be non empty Subset of Z,
H be non empty Subset of MetricSpaceNorm Z,
T being Subset of TopSpaceNorm Z
st Z is complete & H = F & H = T
holds
( (MetricSpaceNorm Z) | H is totally_bounded
iff Cl(H) is sequentially_compact) &
( (MetricSpaceNorm Z) | H is totally_bounded
iff
(MetricSpaceNorm Z) | Cl(H) is compact) &
( (MetricSpaceNorm Z) | H is totally_bounded
iff
Cl(F) is compact) &
( (MetricSpaceNorm Z) | H is totally_bounded
iff
Cl(T) is compact)
proof
let Z be RealNormSpace,
F be non empty Subset of Z,
H be non empty Subset of MetricSpaceNorm Z,
T be Subset of TopSpaceNorm Z;
assume A1: Z is complete;
assume A2: F = H & H = T; then
A3: Cl(F) = Cl(H) by Th1;
consider HH be Subset of TopSpaceMetr MetricSpaceNorm Z such that
A4:HH = H & Cl(H) = Cl(HH) by Def1;
(MetricSpaceNorm Z) | Cl(H) is complete by Th7,A1;
hence
A5: (MetricSpaceNorm Z) | H is totally_bounded
iff Cl(H) is sequentially_compact by TOPMETR4:17,Th8;
thus ((MetricSpaceNorm Z) | H is totally_bounded
iff (MetricSpaceNorm Z) | Cl(H) is compact) by A5,TOPMETR4:14;
thus (MetricSpaceNorm Z) | H is totally_bounded
iff
Cl(F) is compact by A5,TOPMETR4:18,A3;
hence (MetricSpaceNorm Z) | H is totally_bounded iff
Cl(T) is compact by A3,A2,A4,TOPMETR4:19;
end;
theorem Th11:
for S be non empty compact TopSpace,T be NormedLinearTopSpace
st T is complete holds
for H be non empty Subset of
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T))
holds
Cl(H) is sequentially_compact iff
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T) )
| H is totally_bounded
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 H be non empty Subset of
MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T);
reconsider F = H as non empty Subset of Z;
set N = (MetricSpaceNorm Z) | H;
Z is complete by A1,C0SP3:52; then
(MetricSpaceNorm Z) | Cl(H) is totally_bounded
iff Cl(H) is sequentially_compact by TOPMETR4:17,Th7;
hence thesis by Th8;
end;
theorem Th12:
for S be non empty compact TopSpace,T be NormedLinearTopSpace
st T is complete holds
for F be non empty Subset of
R_NormSpace_of_ContinuousFunctions(S,T),
H be non empty Subset of
MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T) st
H = F holds
Cl(F) is compact iff
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T) )
| H is totally_bounded
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 F be non empty Subset of Z, H be non empty Subset of MetricSpaceNorm Z;
assume F = H; then
A3:Cl(F) = Cl(H) by Th1;
Cl(H) is sequentially_compact iff
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T) )
| H is totally_bounded by Th11,A1;
hence thesis by TOPMETR4:18,A3;
end;
theorem Th13:
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace
st S = TopSpaceMetr(M) & T is complete holds
for G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T) st
G = H & (MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T))
| H is totally_bounded holds
G is equibounded & G is equicontinuous
proof
let M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace;
assume A1: S = TopSpaceMetr(M) & T is complete;
let G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T));
assume A2: G = H;
set Z = R_NormSpace_of_ContinuousFunctions(S,T);
set MZH = (MetricSpaceNorm Z) | H;
A3:the carrier of MZH = H by TOPMETR:def 2;
assume
A4: (MetricSpaceNorm Z) | H is totally_bounded;
consider L being Subset-Family of MZH such that
A5: L is finite & the carrier of MZH = union L
& for C being Subset of MZH st C in L holds
ex w being Element of MZH st C = Ball (w,1) by A4;
defpred P1[object,object] means
ex w be Point of MZH st $2 = w & $1 =Ball(w,1);
A6: for D be object st D in L
ex w be object st w in the carrier of MZH & P1[D,w]
proof
let D be object;
assume A7: D in L; then
reconsider D0=D as Subset of MZH;
consider w being Element of MZH such that
A8:D0 = Ball (w,1) by A5,A7;
take w;
thus w in the carrier of MZH & P1[D,w] by A8;
end;
consider U being Function of L,the carrier of MZH such that
A9: for D being object st D in L
holds P1[D,U.D] from FUNCT_2:sch 1(A6);
A10:for D being object st D in L holds D = Ball(U/.D,1)
proof
let D be object;
assume A11: D in L; then
A12: ex x0 be Point of MZH st U.D = x0 & D = Ball(x0,1) by A9;
dom U = L by FUNCT_2:def 1;
hence D = Ball(U/.D,1) by A12,A11,PARTFUN1:def 6;
end;
set NF = the normF of Z;
A13: dom U = L by FUNCT_2:def 1;
reconsider NFU = NF.: (rng U) as finite Subset of REAL by A5;
consider xx be object such that
A14: xx in L by XBOOLE_0:def 1,A5,ZFMISC_1:2;
rng U <> {} by A13,A14,FUNCT_1:3;
then consider xx be object such that
A15: xx in rng U by XBOOLE_0:def 1;
reconsider xx as Point of MZH by A15;
set d0 = upper_bound NFU;
A16: for r be Real st r in NFU holds r <= d0 by SEQ_4:def 1;
set K = d0 + 1;
for f be Function of the carrier of M,the carrier of T
st f in G holds for x be Element of M
holds ||.f.x.|| <= K
proof
let f be Function of the carrier of M,the carrier of T;
assume f in G; then
consider C be set such that
A17: f in C & C in L by A5,TARSKI:def 4,A3,A2;
reconsider C as Subset of the carrier of MZH by A17;
reconsider pf=f as Element of MZH by A17;
A18: pf in H by A3;
set pg = U/.C;
reconsider pg as Element of MZH;
A19:C = Ball (pg,1) by A10,A17;
A20: pg in H by A3; then
pg in Z; then
ex f be Function of the carrier of S, the carrier of T
st pg=f & f is continuous; then
reconsider g=pg as Function of S,T;
pf in { y where y is Point of MZH : dist(pg,y) < 1 }
by METRIC_1:def 14,A17,A19; then
A21:ex y be Point of MZH st pf=y & dist(pg,y) < 1;
reconsider ppf=pf,ppg=pg as Element of MetricSpaceNorm Z by A18,A20;
A22: dist(ppg,ppf) < 1 by A21,TOPMETR:def 1;
reconsider pppf=ppf,pppg=ppg as Point of Z;
A23: ||.pppg-pppf.|| < 1 by A22,NORMSP_2:def 1;
pppf = pppf-pppg + pppg by RLVECT_4:1; then
||.pppf.|| <= ||.pppf-pppg .|| + ||.pppg.|| by NORMSP_1:def 1; then
A24: ||.pppf.|| <= ||.pppg-pppf.|| + ||.pppg.|| by NORMSP_1:7;
A25:C in dom U by FUNCT_2:def 1,A17;
U.C in rng U by FUNCT_1:3,A13,A17; then
pg in rng U by A25,PARTFUN1:def 6; then
||.pppg.|| <= d0 by A16, FUNCT_2:35; then
||.pppg-pppf.|| + ||.pppg.|| <= 1+d0 by XREAL_1:8,A23; then
A26: ||.pppf.|| <= K by A24,XXREAL_0:2;
let x be Element of M;
reconsider x0 = x as Point of S by A1;
reconsider f0=f
as Function of the carrier of S,the carrier of T by A1;
||.f0.x0.|| <=||.pppf.|| by C0SP3:37;
hence ||.f.x.|| <= K by A26,XXREAL_0:2;
end;
hence G is equibounded;
for e be Real st 0 < e
ex d be Real st 0 < d &
for f be Function of the carrier of M,the carrier of T
st f in G
holds
for x1,x2 be Point of M
st dist(x1,x2) < d holds ||.f.x1-f.x2.|| < e
proof
let e be Real;
assume A27:0 < e; then
consider L being Subset-Family of MZH such that
A28: L is finite & the carrier of MZH = union L
& for C being Subset of MZH st C in L holds
ex w being Element of MZH st C = Ball (w,e/3) by A4;
defpred P1[object,object] means
ex w be Point of MZH st $2 = w & $1 = Ball(w,e/3);
A29: for D be object st D in L
ex w be object st w in the carrier of MZH & P1[D,w]
proof
let D be object;
assume A30: D in L; then
reconsider D0=D as Subset of MZH;
consider w being Element of MZH such that
A31: D0 = Ball (w,e/3) by A28,A30;
take w;
thus w in the carrier of MZH & P1[D,w] by A31;
end;
consider U being Function of L,the carrier of MZH such that
A32: for D being object
st D in L
holds P1[D,U.D] from FUNCT_2:sch 1(A29);
A33:for D being object st D in L holds D = Ball(U/.D,e/3)
proof
let D be object;
assume A34: D in L; then
A35: ex x0 be Point of MZH st U.D = x0 & D = Ball(x0,e/3) by A32;
dom U = L by FUNCT_2:def 1;
hence D = Ball(U/.D,e/3) by A35,A34,PARTFUN1:def 6;
end;
defpred P1[Element of MZH,Real] means
ex f be Function of the carrier of S,the carrier of T
st $1=f & 0 < $2
& for x1,x2 be Point of M st dist(x1,x2) < $2
holds ||.f/.x1-f/.x2.|| < e/3;
A36: for x0 being Element of the carrier of MZH
ex d being Element of REAL st P1[x0,d]
proof
let x0 be Element of the carrier of MZH;
x0 in H by A3; then
x0 in Z; then
A37: ex f be Function of the carrier of S, the carrier of T
st x0=f & f is continuous; then
reconsider f=x0 as Function of the carrier of S,
the carrier of T;
consider d be Real such that
A38: 0 < d &
for x1,x2 be Point of M st dist(x1,x2) < d
holds ||.f/.x1-f/.x2.|| < e/3 by A27,Th4,A1,A37;
reconsider d0=d as Element of REAL by XREAL_0:def 1;
take d0;
thus thesis by A38;
end;
consider NF being Function of the carrier of MZH,REAL such that
A39: for f being Element of the carrier of MZH
holds P1[f,NF.f] from FUNCT_2:sch 3(A36);
A40: dom U = L by FUNCT_2:def 1;
reconsider NFU = NF.: (rng U) as finite Subset of REAL by A28;
consider xx be object such that
A41: xx in L by XBOOLE_0:def 1,A28,ZFMISC_1:2;
rng U <> {} by A40,A41,FUNCT_1:3; then
consider xx be object such that
A42: xx in rng U by XBOOLE_0:def 1;
reconsider xx as Point of MZH by A42;
A43: NFU is bounded_below & lower_bound NFU in NFU by SEQ_4:133,A42;
set d = lower_bound NFU;
consider xx being object such that
A44: xx in dom NF & xx in rng U & d = NF . xx by FUNCT_1:def 6,A43;
reconsider xx as Point of MZH by A44;
A45:ex f be Function of the carrier of S,the carrier of T
st xx=f & 0 < NF.xx
& for x1,x2 be Point of M st dist(x1,x2) < NF.xx
holds ||.f/.x1-f/.x2.|| < e/3 by A39;
take d;
thus 0 < d by A45,A44;
thus for f be Function of the carrier of M,the carrier of T
st f in G holds
for x1,x2 be Point of M
st dist(x1,x2) < d holds ||.f.x1-f.x2.|| < e
proof
let f0 be Function of the carrier of M,the carrier of T;
assume f0 in G; then
consider C be set such that
A46: f0 in C & C in L by A28,TARSKI:def 4,A3,A2;
reconsider f=f0 as Function of the carrier of S,the carrier of T by A1;
reconsider C as Subset of the carrier of MZH by A46;
reconsider pf=f0 as Element of MZH by A46;
A47: pf in H by A3;
reconsider pg = U/.C as Element of MZH;
A48:C = Ball (pg,e/3) by A33,A46;
A49: pg in H by A3; then
pg in ContinuousFunctions(S,T); then
ex f be Function of the carrier of S, the carrier of T
st pg=f & f is continuous; then
reconsider g=pg as Function of S,T;
pf in { y where y is Point of MZH : dist(pg,y) < e/3 }
by METRIC_1:def 14,A46,A48; then
A50:ex y be Point of MZH st pf=y & dist(pg,y) < e/3;
reconsider ppf=pf,ppg=pg as Element of MetricSpaceNorm Z by A47,A49;
A51: dist(ppg,ppf) < e/3 by A50,TOPMETR:def 1;
reconsider pppf=ppf,pppg=ppg as Point of Z;
A52: ||.pppg-pppf.|| < e/3 by A51,NORMSP_2:def 1;
A53:C in dom U by FUNCT_2:def 1,A46;
U.C in rng U by FUNCT_1:3,A40,A46; then
pg in rng U by A53,PARTFUN1:def 6; then
A54: NF.pppg in NF.: (rng U) by FUNCT_2:35;
let x1,x2 be Element of M;
reconsider x10 = x1,x20 = x2 as Point of S by A1;
assume A55: dist(x1,x2) < d;
d <=NF.pg by A54,SEQ_4:def 2; then
A56: dist(x1,x2) < NF.pg by A55,XXREAL_0:2;
ex f be Function of the carrier of S,the carrier of T
st pg=f & 0 < NF.pg
& for x1,x2 be Point of M st dist(x1,x2) < NF.pg
holds ||.f/.x1-f/.x2.|| < e/3 by A39; then
A57: ||.g/.x1-g/.x2.|| < e/3 by A56;
pppg-pppf in ContinuousFunctions(S,T); then
ex f be Function of the carrier of S, the carrier of T
st pppg-pppf=f & f is continuous; then
reconsider gf=pppg-pppf as Function of S,T;
pppf-pppg in ContinuousFunctions(S,T); then
ex f be Function of the carrier of S, the carrier of T
st pppf-pppg=f & f is continuous; then
reconsider fg=pppf-pppg as Function of S,T;
||.gf.x20.|| <= ||.pppg-pppf.|| by C0SP3:37; then
A59: ||.g.x20 - f.x20 .|| <= ||.pppg-pppf.|| by C0SP3:48;
f/.x20=f.x20 & g/.x20 =g.x20; then
A60: ||.g/.x2-f/.x2.|| < e/3 by A59,XXREAL_0:2,A52;
||.fg.x10.|| <= ||.pppf-pppg.|| by C0SP3:37; then
||.f.x10 - g.x10 .|| <= ||.pppf-pppg.|| by C0SP3:48; then
A62: ||.f.x10 - g.x10 .|| <= ||.pppg-pppf.|| by NORMSP_1:7;
f/.x10=f.x10 & g/.x10 =g.x10; then
A63: ||.f/.x1-g/.x1.|| < e/3 by A62,XXREAL_0:2,A52;
f/.x1-f/.x2 = f/.x1-g/.x1+g/.x1-f/.x2 by RLVECT_4:1
.= f/.x1-g/.x1+ (g/.x1-f/.x2) by RLVECT_1:28
.= f/.x1-g/.x1+ (g/.x1-g/.x2+ g/.x2 -f/.x2) by RLVECT_4:1
.= f/.x1-g/.x1+ (g/.x1-g/.x2+ (g/.x2 -f/.x2)) by RLVECT_1:28; then
A64:||.f/.x1-f/.x2.|| <= ||.f/.x1-g/.x1.||
+ ||.g/.x1-g/.x2+ (g/.x2 -f/.x2).|| by NORMSP_1:def 1;
A65: ||.g/.x1-g/.x2+ (g/.x2 -f/.x2).||
<= ||.g/.x1-g/.x2.|| + ||.g/.x2 -f/.x2.|| by NORMSP_1:def 1;
||.g/.x1-g/.x2.|| + ||.g/.x2 -f/.x2.||
< e/3 + e/3 by A57,A60,XREAL_1:8; then
||.g/.x1-g/.x2+ (g/.x2 -f/.x2).|| < (e/3+e/3) by XXREAL_0:2,A65; then
A66: ||.f/.x1-g/.x1.|| + ||.g/.x1-g/.x2+ (g/.x2 -f/.x2).||
< e/3 + (e/3+e/3) by A63,XREAL_1:8;
f/.x10=f.x10 & f/.x20 = f.x20;
hence ||.f0.x1-f0.x2.|| < e by A66,A64,XXREAL_0:2;
end;
end;
hence G is equicontinuous;
end;
theorem Th14:
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace
st S = TopSpaceMetr(M) & T is complete holds
for G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T)
st G = H &
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T))
| H is totally_bounded holds
( for x be Point of S,
Hx be non empty Subset of MetricSpaceNorm T
st Hx = {f.x where f is Function of S,T :f in H }
holds (MetricSpaceNorm T) | Hx is totally_bounded )
& G is equicontinuous
proof
let M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace;
assume A1: S = TopSpaceMetr(M) & T is complete;
let G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T);
assume A2: G = H;
set Z = R_NormSpace_of_ContinuousFunctions(S,T);
set MZH = (MetricSpaceNorm Z) | H;
A3:the carrier of MZH = H by TOPMETR:def 2;
assume A4: (MetricSpaceNorm Z) | H is totally_bounded;
thus for x be Point of S,
Hx be non empty Subset of MetricSpaceNorm T
st Hx = {f.x where f is Function of S,T :f in H }
holds (MetricSpaceNorm T) | Hx is totally_bounded
proof
let x be Point of S,
Hx be non empty Subset of MetricSpaceNorm T;
assume A5:Hx = {f.x where f is Function of S,T :f in H };
set MTHx = (MetricSpaceNorm T) | Hx;
let e be Real;
assume 0 < e; then
consider L being Subset-Family of MZH such that
A6: L is finite & the carrier of MZH = union L
& for C being Subset of MZH st C in L holds
ex w being Element of MZH st C = Ball (w,e) by A4;
defpred P1[object,object] means
ex w be Point of MZH st $2 = w & $1 =Ball(w,e);
A7: for D be object st D in L
ex w be object st w in the carrier of MZH & P1[D,w]
proof
let D be object;
assume A8: D in L; then
reconsider D0=D as Subset of MZH;
consider w being Element of MZH such that A9: D0 = Ball (w,e) by A6,A8;
take w;
thus w in the carrier of MZH & P1[D,w] by A9;
end;
consider U being Function of L,the carrier of MZH such that
A10: for D being object
st D in L
holds P1[D,U.D] from FUNCT_2:sch 1(A7);
A11:for D being object st D in L holds D = Ball(U/.D,e)
proof
let D be object;
assume A12: D in L; then
A13: ex x0 be Point of MZH st U.D = x0 & D =Ball(x0,e) by A10;
dom U = L by FUNCT_2:def 1;
hence D = Ball(U/.D,e) by A13,A12,PARTFUN1:def 6;
end;
defpred Q1[object,object] means
ex w be Function of S,T,
p be Point of MTHx st
$1 = w & p= w.x & $2 =Ball(p,e);
A14: for f be object st f in (the carrier of MZH)
ex B be object st B in bool the carrier of MTHx & Q1[f,B]
proof
let f be object;
assume
A15: f in the carrier of MZH; then
f in Z by A3; then
ex g be Function of the carrier of S, the carrier of T
st f=g & g is continuous; then
reconsider g = f as Function of S,T;
g.x in Hx by A15,A5,A3; then
reconsider p=g.x as Point of MTHx by TOPMETR:def 2;
take B = Ball(p,e);
thus thesis;
end;
consider NF being Function of the carrier of MZH,
bool the carrier of MTHx such that
A16: for D being object
st D in the carrier of MZH holds Q1[D,NF.D] from FUNCT_2:sch 1(A14);
A17: dom U = L by FUNCT_2:def 1;
set Le = NF .:(rng U);
reconsider Le as Subset-Family of MTHx;
take Le;
thus Le is finite by A6;
for t be object holds t in the carrier of MTHx iff t in union Le
proof
let t0 be object;
hereby assume A18: t0 in the carrier of MTHx; then
A19:t0 in Hx by TOPMETR:def 2;
reconsider t = t0 as Point of MTHx by A18;
consider f be Function of S,T such that
A20:t=f.x & f in H by A5,A19;
consider K be set such that
A21: f in K & K in L by TARSKI:def 4,A6,A3,A20;
U/.K =U.K by PARTFUN1:def 6,A21,A17; then
A22:U/.K in rng U by FUNCT_1:def 3,A17,A21;
consider g be Function of S,T,
p be Point of MTHx such that
A23: (U/.K) = g & p= g.x & NF.(U/.K) =Ball(p,e) by A16;
A24: f in Ball(U/.K,e) by A21,A11;
reconsider f0= f as Point of MZH by A21;
A25: dist(f0,U/.K) < e by A24,METRIC_1:11;
reconsider f1=f0 as Point of MetricSpaceNorm Z
by TOPMETR:def 1,TARSKI:def 3;
reconsider g1=U/.K as Point of MetricSpaceNorm Z
by TOPMETR:def 1,TARSKI:def 3;
A26: dist(f1,g1) < e by A25,TOPMETR:def 1;
reconsider f2=f1,g2=g1 as Point of Z;
A27: ||.f2-g2.|| < e by NORMSP_2:def 1,A26;
g2-f2 in ContinuousFunctions(S,T); then
ex f be Function of the carrier of S,the carrier of T
st g2-f2 =f & f is continuous; then
reconsider fg=g2-f2 as Function of S,T;
||.fg.x.|| <= ||.g2-f2.|| by C0SP3:37; then
||.fg.x.|| <= ||.f2-g2.|| by NORMSP_1:7; then
||.g.x - f.x .|| <= ||.f2-g2.|| by A23,C0SP3:48; then
A30: ||.g/.x-f/.x.|| < e by A27,XXREAL_0:2;
A31: NF.(U/.K) in Le by A22,FUNCT_2:35;
reconsider tt=t as Point of MetricSpaceNorm T by A20;
reconsider pp = p as Point of MetricSpaceNorm T
by TOPMETR:def 1,TARSKI:def 3;
reconsider p1 = pp as Point of T;
dist(pp,tt) < e by NORMSP_2:def 1,A23,A20,A30; then
dist(p,t) < e by TOPMETR:def 1; then
f.x in { y where y is Point of MTHx : dist(p,y) < e } by A20; then
f.x in NF.(U/.K) by A23,METRIC_1:def 14;
hence t0 in union Le by TARSKI:def 4,A31,A20;
end;
assume t0 in union Le;
hence t0 in the carrier of MTHx;
end;
hence the carrier of MTHx = union Le by TARSKI:2;
thus for C being Subset of MTHx st C in Le holds
ex p being Element of MTHx st C = Ball (p,e)
proof
let C be Subset of MTHx;
assume C in Le; then
consider t be object such that
A33: t in dom NF & t in rng U & C = NF.t by FUNCT_1:def 6;
consider w be Function of S,T,
p be Point of MTHx such that
A34: t = w & p= w.x & NF.t=Ball(p,e) by A33,A16;
take p;
thus C = Ball(p,e) by A34,A33;
end;
end;
thus G is equicontinuous by Th13,A1,A2,A4;
end;
theorem Th15:
for T be NormedLinearTopSpace,
RNS be RealNormSpace st
RNS = the NORMSTR of T &
the topology of T = the topology of TopSpaceNorm RNS holds
distance_by_norm_of RNS = distance_by_norm_of T &
MetricSpaceNorm RNS = MetricSpaceNorm T &
TopSpaceNorm T = TopSpaceNorm RNS
proof
let T be NormedLinearTopSpace, RNS be RealNormSpace;
assume
A1: RNS = the NORMSTR of T
& the topology of T = the topology of TopSpaceNorm RNS;
A2: for x, y being Point of RNS
holds (distance_by_norm_of T) . (x,y) = ||. x - y .||
proof
let x, y being Point of RNS;
reconsider x1=x,y1=y as Point of T by A1;
thus (distance_by_norm_of T) . (x,y) = ||.x1 - y1.|| by NORMSP_2:def 1
.= ||.x - y.|| by C0SP3:19,A1;
end;
hence distance_by_norm_of RNS
= distance_by_norm_of T by A1,NORMSP_2:def 1;
thus MetricSpaceNorm RNS = MetricSpaceNorm T by A2,NORMSP_2:def 1,A1;
thus TopSpaceNorm T = TopSpaceNorm RNS by A2,NORMSP_2:def 1,A1;
end;
theorem Th16:
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace,
G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T)
st S = TopSpaceMetr(M) & T is complete & G = H holds
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T))
| H is totally_bounded
iff
G is equicontinuous &
for x be Point of S,
Hx be non empty Subset of MetricSpaceNorm T
st Hx = {f.x where f is Function of S,T :f in H }
holds (MetricSpaceNorm T) | Cl(Hx) is compact
proof
let M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace;
let G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T);
assume A1: S = TopSpaceMetr(M) & T is complete;
assume A2: G = H;
set Z = R_NormSpace_of_ContinuousFunctions(S,T);
set MZH = (MetricSpaceNorm Z) | H;
A3:the carrier of MZH = H by TOPMETR:def 2;
hereby assume A4: (MetricSpaceNorm Z) | H is totally_bounded;
hence G is equicontinuous by Th14,A1,A2;
thus for x be Point of S,
Hx be non empty Subset of MetricSpaceNorm T
st Hx = {f.x where f is Function of S,T :f in H }
holds
(MetricSpaceNorm T) | Cl(Hx) is compact
proof
let x be Point of S,
Hx be non empty Subset of MetricSpaceNorm T;
assume A5: Hx = {f.x where f is Function of S,T :f in H };
(MetricSpaceNorm T) | Hx is totally_bounded by Th14,A1,A2,A4,A5;
hence (MetricSpaceNorm T) | Cl(Hx) is compact by Th9,A1;
end;
end;
assume
A6:G is equicontinuous &
for x be Point of S, Hx be non empty Subset of MetricSpaceNorm T
st Hx = {f.x where f is Function of S,T :f in H }
holds (MetricSpaceNorm T) | Cl(Hx) is compact;
for e being Real st e > 0 holds
ex L being Subset-Family of MZH st
L is finite & the carrier of MZH = union L
& for C being Subset of MZH st C in L holds
ex w being Element of MZH st C = Ball (w,e)
proof
let e0 be Real;
assume
A7: e0 > 0; then
A8: 0 < e0/2 & e0/2 < e0 by XREAL_1:216;
set e=e0/2;
consider d be Real such that
A9: 0 < d &
for f be Function of the carrier of M,the carrier of T
st f in G holds
for x1,x2 be Point of M
st dist(x1,x2) < d holds ||.f.x1-f.x2.|| < e/4 by A6,A7;
set BM = the set of all Ball (x0,d)
where x0 is Element of M;
BM c= bool the carrier of S
proof
let z be object;
assume z in BM; then
consider x0 be Point of M such that
A10: z = Ball (x0,d);
thus z in bool the carrier of S by A10,A1;
end; then
reconsider BM as Subset-Family of S;
for P being Subset of S st P in BM holds P is open
proof
let P be Subset of S;
assume P in BM; then
consider x0 be Point of M such that
A11: P = Ball (x0,d);
thus P is open by A1,A11,PCOMPS_1:29;
end; then
A12: BM is open by TOPS_2:def 1;
the carrier of S c= union BM
proof
let z be object;
assume z in the carrier of S; then
reconsider x0=z as Point of M by A1;
A13:Ball(x0,d) in BM;
dist(x0,x0) < d by A9,METRIC_1:1; then
x0 in { y where y is Element of M : dist (x0,y) < d }; then
x0 in Ball(x0,d) by METRIC_1:def 14;
hence z in union BM by TARSKI:def 4,A13;
end; then
BM is Cover of [#] S by SETFAM_1:def 11; then
consider BM0 being Subset-Family of S such that
A15: BM0 c= BM & BM0 is Cover of [#] S & BM0 is finite
by COMPTS_1:def 4,COMPTS_1:1,A12;
reconsider BM0 as finite set by A15;
defpred P1[object,object] means
ex w be Point of M st $2 = w & $1 =Ball(w,d);
A16: for D be object st D in BM
ex w be object st w in the carrier of M & P1[D,w]
proof
let D be object;
assume D in BM; then
consider w being Element of M such that
A17: D = Ball (w,d);
take w;
thus w in the carrier of M & P1[D,w] by A17;
end;
consider U being Function of BM,the carrier of M such that
A18: for D being object st D in BM
holds P1[D,U.D] from FUNCT_2:sch 1(A16);
A19:for D being object st D in BM holds D = Ball(U/.D,d)
proof
let D be object;
assume A20: D in BM; then
A21: ex x0 be Point of M st U.D = x0 &
D = Ball(x0,d) by A18;
dom U = BM by FUNCT_2:def 1;
hence D = Ball(U/.D,d) by A21,A20,PARTFUN1:def 6;
end;
set CF = canFS(BM0);
A22: len CF = card (BM0) by FINSEQ_1:93;
A23: rng CF = BM0 by FUNCT_2:def 3;
A24: dom U = BM by FUNCT_2:def 1; then
reconsider PS = U*CF as FinSequence by A23,A15,FINSEQ_1:16;
rng PS c= rng U by RELAT_1:26; then
reconsider PS as FinSequence of the carrier of S
by FINSEQ_1:def 4,A1,XBOOLE_1:1;
A25: dom PS = dom CF by A23,A24,A15,RELAT_1:27
.=Seg card BM0 by A22,FINSEQ_1:def 3;
A26: dom CF = Seg len CF by FINSEQ_1:def 3
.= dom PS by A25,FINSEQ_1:93;
A27: for i be Nat st i in dom PS holds CF.i = Ball((U*CF)/.i,d)
proof
let i be Nat;
assume A28: i in dom PS; then
A29: CF.i in rng CF by FUNCT_1:3,A26; then
U/.(CF.i) = U.(CF.i) by PARTFUN1:def 6,A24,A15
.=PS.i by FUNCT_1:12,A28
.=(U*CF)/.i by PARTFUN1:def 6,A28;
hence thesis by A29,A19,A15;
end;
union rng CF = union BM0 by FUNCT_2:def 3; then
A30:the carrier of S c=union rng CF by A15,SETFAM_1:def 11;
A31:BM0 <> {}
proof
assume BM0 = {}; then
[#]S c= {} by SETFAM_1:def 11,A15,ZFMISC_1:2;
hence contradiction;
end;
defpred Q1[object,object] means
ex x be Point of S,
NHx be non empty Subset of T,
CHx be non empty Subset of MetricSpaceNorm T st
$1 = x & NHx={f.x where f is Function of S,T :f in H } &
$2 = Cl(NHx);
A32: for x be object st x in the carrier of S
ex B be object st
B in bool the carrier of MetricSpaceNorm T & Q1[x,B]
proof
let x be object;
assume x in the carrier of S; then
reconsider x0= x as Point of S;
set NHx = {f.x0 where f is Function of S,T :f in H };
consider f0 be object such that
A33: f0 in H by XBOOLE_0:def 1;
f0 in Z by A33; then
ex g be Function of the carrier of S, the carrier of T
st f0=g & g is continuous; then
reconsider g=f0 as Function of S,T;
A34:g.x0 in NHx by A33;
NHx c= the carrier of T
proof
let z be object;
assume z in NHx; then
consider f be Function of S,T such that
A35: z= f.x0 & f in H;
thus z in the carrier of T by A35;
end; then
reconsider NHx as non empty Subset of T by A34;
set CHx = Cl(NHx);
NHx c= Cl(NHx) by NORMSP_3:4; then
reconsider CHx as non empty Subset of MetricSpaceNorm T;
CHx in bool the carrier of MetricSpaceNorm T;
hence thesis;
end;
consider ST being Function of
the carrier of S, bool the carrier of MetricSpaceNorm T such that
A36: for x being object
st x in the carrier of S
holds Q1[x,ST.x] from FUNCT_2:sch 1(A32);
A37: dom ST = the carrier of S by FUNCT_2:def 1;
A38: rng PS c= the carrier of S; then
reconsider STPS = ST*PS as FinSequence by A37,FINSEQ_1:16;
rng STPS c= rng ST by RELAT_1:26; then
reconsider STPS as FinSequence of bool the carrier of TopSpaceNorm T
by FINSEQ_1:def 4,XBOOLE_1:1;
A39: dom STPS = Seg card BM0 by A25,A37,A38,RELAT_1:27;
A40: for i be Nat st i in dom STPS holds
(ex NHx be non empty Subset of T,
CHx be non empty Subset of MetricSpaceNorm T
st NHx= {f.(PS/.i) where f is Function of S,T :f in H }
& STPS/.i = Cl(NHx) ) & STPS/.i is non empty
proof
let i be Nat;
assume
A41:i in dom STPS; then
A44: STPS/.i = STPS.i by PARTFUN1:def 6
.= ST.(PS.i) by FUNCT_1:12,A41;
consider x be Point of S,
NHx be non empty Subset of T,
CHx be non empty Subset of MetricSpaceNorm T such that
A45:PS/.i = x &
NHx={f.x where f is Function of S,T :f in H } &
ST.(PS/.i) = Cl(NHx) by A36;
A46: STPS/.i = Cl(NHx) by A45,A44,A39,A25,A41,PARTFUN1:def 6;
consider f0 be object such that
A47: f0 in H by XBOOLE_0:def 1;
f0 in Z by A47; then
ex g be Function of the carrier of S, the carrier of T
st f0=g & g is continuous; then
reconsider g=f0 as Function of S,T;
NHx c= Cl(NHx) by NORMSP_3:4;
hence thesis by A45,A46;
end;
for i be Nat st i in Seg len STPS holds STPS/.i is compact
proof
let i be Nat;
assume i in Seg len STPS; then
i in dom STPS by FINSEQ_1:def 3; then
consider NHx be non empty Subset of T,
CHx be non empty Subset of MetricSpaceNorm T such that
A48:NHx= {f.(PS/.i) where f is Function of S,T :f in H } &
STPS/.i = Cl(NHx) by A40;
reconsider Hx1 = NHx as non empty Subset of MetricSpaceNorm T;
A49: (MetricSpaceNorm T) | Cl(Hx1) is compact by A48,A6;
reconsider NHx1=Hx1 as non empty Subset of T;
NHx1 c= Cl(NHx1) by NORMSP_3:4; then
reconsider KK = Cl(NHx1) as non empty Subset of TopSpaceNorm T;
A50: Cl(NHx1) = Cl(Hx1) by Th1;
consider RNS be RealNormSpace such that
A51: RNS = the NORMSTR of T
& the topology of T = the topology of TopSpaceNorm RNS by C0SP3:def 6;
A52: MetricSpaceNorm RNS = MetricSpaceNorm T by Th15,A51;
reconsider RNV1= Cl(NHx1) as Subset of RNS by A51;
A53: TopSpaceNorm T = TopSpaceNorm RNS by Th15,A51;
Cl(Hx1) is sequentially_compact by TOPMETR4:14,A49; then
RNV1 is compact by A52,TOPMETR4:18,A50;
hence thesis by A48,TOPMETR4:19,A53;
end; then
A54: union rng STPS is compact by Th2;
consider i0 be object such that
A55: i0 in dom STPS by A31,A39,XBOOLE_0:def 1;
reconsider i0 as Nat by A55;
STPS/.i0 = STPS.i0 by A55,PARTFUN1:def 6; then
STPS/.i0 c= union rng STPS by ZFMISC_1:74,A55,FUNCT_1:3; then
reconsider URSTPS = union rng STPS
as non empty Subset of MetricSpaceNorm T by A55,A40;
URSTPS is sequentially_compact by A54,TOPMETR4:15; then
A58: (MetricSpaceNorm T) | URSTPS is compact by TOPMETR4:14;
set MURSTPS = (MetricSpaceNorm T) | URSTPS;
set BM2 = the set of all
Ball (w,e/4) where w is Element of MURSTPS;
BM2 c= bool the carrier of MURSTPS
proof
let z be object;
assume z in BM2; then
consider x0 be Point of MURSTPS such that
A59: z = Ball (x0,e/4);
thus z in bool the carrier of MURSTPS by A59;
end; then
reconsider BM2 as Subset-Family of MURSTPS;
A60: for P being set st P in BM2 holds
ex x0 be Point of MURSTPS st
ex r be Real st P = Ball(x0,r)
proof
let P be set;
assume P in BM2; then
consider x0 be Point of MURSTPS such that
A61: P = Ball (x0,e/4);
take x0,e/4;
thus thesis by A61;
end;
the carrier of MURSTPS c= union BM2
proof
let z be object;
assume z in the carrier of MURSTPS; then
reconsider x0=z as Point of MURSTPS;
A62:Ball(x0,e/4) in BM2;
dist(x0,x0) = 0 by METRIC_1:1; then
x0 in { y where y is Element of MURSTPS : dist (x0,y) < e/4 } by A7; then
x0 in Ball(x0,e/4) by METRIC_1:def 14;
hence z in union BM2 by TARSKI:def 4,A62;
end; then
BM2 is Cover of [#] MURSTPS by SETFAM_1:def 11; then
consider BM02 being Subset-Family of MURSTPS such that
A64: BM02 c= BM2 & BM02 is Cover of [#] MURSTPS & BM02 is finite
by A58,TOPMETR:16,A60,TOPMETR:def 4;
reconsider BM02 as finite set by A64;
A65: BM02 <> {}
proof
assume BM02 = {}; then
[#]MURSTPS c= {} by SETFAM_1:def 11,A64,ZFMISC_1:2;
hence contradiction;
end;
defpred P2[object,object] means ex w be Point of MURSTPS st $2 = w &
$1 = Ball(w,e/4);
A66: for D be object st D in BM2
ex w be object st w in the carrier of MURSTPS & P2[D,w]
proof
let D be object;
assume D in BM2; then
consider w being Element of MURSTPS such that
A67: D = Ball (w,e/4);
take w;
thus w in the carrier of MURSTPS & P2[D,w] by A67;
end;
consider U2 being Function of BM2,the carrier of MURSTPS such that
A68: for D being object st D in BM2
holds P2[D,U2.D] from FUNCT_2:sch 1(A66);
A69:for D being object st D in BM2 holds D = Ball(U2/.D,e/4)
proof
let D be object;
assume A70: D in BM2; then
A71: ex x0 be Point of MURSTPS st U2.D = x0 & D =Ball(x0,e/4) by A68;
dom U2 = BM2 by FUNCT_2:def 1;
hence D = Ball(U2/.D,e/4) by A71,A70,PARTFUN1:def 6;
end;
set CF2 = canFS BM02;
A72: len CF2 = card BM02 by FINSEQ_1:93;
A73: rng CF2 = BM02 by FUNCT_2:def 3;
A74: dom U2 = BM2 by FUNCT_2:def 1; then
reconsider PS2 = U2*CF2 as FinSequence by A73,A64,FINSEQ_1:16;
rng PS2 c= rng U2 by RELAT_1:26; then
reconsider PS2 as FinSequence of the carrier of MURSTPS
by FINSEQ_1:def 4,XBOOLE_1:1;
A75: dom PS2 = dom CF2 by A73,A74,A64,RELAT_1:27
.=Seg (card (BM02)) by A72,FINSEQ_1:def 3;
A76: dom CF2 = Seg len CF2 by FINSEQ_1:def 3
.= dom PS2 by A75,FINSEQ_1:93;
A77: for i be Nat st i in dom PS2 holds CF2.i = Ball((U2*CF2)/.i,e/4)
proof
let i be Nat;
assume A78: i in dom PS2;
A79:CF2.i in rng CF2 by FUNCT_1:3,A76,A78; then
U2/.(CF2.i) = U2.(CF2.i) by PARTFUN1:def 6,A74,A64
.=PS2.i by FUNCT_1:12,A78
.=(U2*CF2)/.i by PARTFUN1:def 6,A78;
hence thesis by A79,A69,A64;
end;
union rng CF2 = union BM02 by FUNCT_2:def 3; then
A80:the carrier of MURSTPS c=union rng CF2 by A64,SETFAM_1:def 11;
defpred Q2[object,object] means
ex sigm be Function of Seg len PS,Seg len CF2 st
$1 = sigm & $2={ f where f is Function of S,T :f in MZH
& for i be Nat st i in Seg len PS
holds f.(PS/.i) in Ball( (U2*CF2)/.(sigm.i),e/4 ) };
A81: for x be object st x in Funcs(Seg len PS,Seg len CF2)
ex B be object st B in bool the carrier of MZH & Q2[x,B]
proof
let x be object;
assume x in Funcs(Seg len PS,Seg len CF2); then
reconsider sigm = x as Function of Seg len PS,Seg len CF2
by FUNCT_2:66;
set NHx = { f where f is Function of S,T :f in MZH
& for i be Nat st i in Seg len PS
holds f.(PS/.i) in Ball ((U2*CF2)/.(sigm.i),e/4) };
NHx c= the carrier of MZH
proof
let z be object;
assume z in NHx; then
ex f be Function of S,T st z=f & f in MZH
& for i be Nat st i in Seg len PS
holds f.(PS/.i) in Ball( (U2*CF2)/.(sigm.i),e/4 );
hence z in the carrier of MZH;
end;
hence thesis;
end;
consider BST being Function of
Funcs(Seg len PS,Seg len CF2),bool the carrier of MZH such that
A82: for x being object
st x in Funcs(Seg len PS,Seg len CF2)
holds Q2[x,BST.x] from FUNCT_2:sch 1(A81);
A83: for sigm be Function of Seg len PS,Seg len CF2
holds BST.sigm
= { f where f is Function of S,T :f in MZH
& for i be Nat st i in Seg len PS
holds f.(PS/.i) in Ball( (U2*CF2)/.(sigm.i),e/4 ) }
proof
let sigm be Function of Seg len PS,Seg len CF2;
sigm in Funcs(Seg len PS,Seg len CF2) by FUNCT_2:8,A65; then
ex sigm1 be Function of Seg len PS,Seg len CF2 st
sigm= sigm1 &
BST.sigm={ f where f is Function of S,T :f in MZH
& for i be Nat st i in Seg len PS
holds f.(PS/.i) in Ball( (U2*CF2)/.(sigm1.i),e/4 ) } by A82;
hence thesis;
end;
A84:Funcs(Seg len PS,Seg len CF2) c= bool [:Seg len PS,Seg len CF2:]
proof
let x be object;
assume x in Funcs(Seg len PS,Seg len CF2); then
reconsider f = x as Function of Seg len PS,Seg len CF2 by FUNCT_2:66;
f in bool [:Seg len PS,Seg len CF2:];
hence x in bool [:Seg len PS,Seg len CF2:];
end;
A85: for sigm be Function of Seg len PS,Seg len CF2 holds
for f,g be Point of MZH
st f in BST.sigm & g in BST.sigm holds dist(f,g) < e0
proof
let sigm be Function of Seg len PS,Seg len CF2;
let f,g be Point of MZH;
assume A86:f in BST.sigm & g in BST.sigm;
A87: BST.sigm = { f where f is Function of S,T :f in MZH
& for i be Nat st i in Seg len PS
holds f.(PS/.i) in Ball( (U2*CF2)/.(sigm.i),e/4 ) } by A83; then
A88: ex f0 be Function of S,T st f=f0 & f0 in MZH
& for i be Nat st i in Seg len PS
holds f0.(PS/.i) in Ball( (U2*CF2)/.(sigm.i),e/4 ) by A86; then
reconsider f0=f as Function of S,T;
reconsider f1=f0 as Function of M,T by A1;
A89:ex f0 be Function of S,T st g=f0 & f0 in MZH
& for i be Nat st i in Seg len PS
holds f0.(PS/.i) in Ball( (U2*CF2)/.(sigm.i),e/4 ) by A86,A87; then
reconsider g0=g as Function of S,T;
reconsider g1=g0 as Function of M,T by A1;
A90: for x be Point of S holds ||.f0.x-g0.x.|| <= e
proof
let x be Point of S;
x in union rng CF by A30; then
consider D be set such that
A91: x in D & D in rng CF by TARSKI:def 4;
consider i be object such that
A92: i in dom CF & D=CF.i by A91,FUNCT_1:def 3;
reconsider i as Nat by A92;
A93:x in Ball((U*CF)/.i,d) by A92,A91,A26,A27;
A94: PS/.i =PS.i by A26,A92,PARTFUN1:def 6
.= (U*CF)/.i by A26,A92,PARTFUN1:def 6;
reconsider ym = (U*CF)/.i as Point of M;
reconsider ys = PS/.i as Point of S;
x in { z where z is Point of M : dist(ym,z) < d }
by METRIC_1:def 14,A93; then
A95:ex z be Point of M st x=z & dist(ym,z) < d; then
reconsider xm=x as Point of M;
A96: ||.f1.ym-f1.xm.|| < e/4 by A3,A9,A95,A2;
A97: ||.g1.ym-g1.xm.|| < e/4 by A3,A9,A95,A2;
i in Seg len PS by A26,A92,FINSEQ_1:def 3; then
f0.ys in Ball( (U2*CF2)/.(sigm.i),e/4 ) by A88; then
f0.ys in { y where y is Element of MURSTPS :
dist ((U2*CF2)/.(sigm.i),y) < e/4 } by METRIC_1:def 14; then
A98: ex y be Element of MURSTPS st f0.ys = y
& dist ((U2*CF2)/.(sigm.i),y) < e/4; then
reconsider f0ys=f0.ys as Point of MURSTPS;
reconsider u2cf2 =(U2*CF2)/.(sigm.i) as
Point of MetricSpaceNorm T by TOPMETR:def 1,TARSKI:def 3;
reconsider f0ysm =f0ys as Point of MetricSpaceNorm T;
A99: dist (u2cf2,f0ysm) < e/4 by A98,TOPMETR:def 1;
reconsider u2cf2n = u2cf2,f0ysn=f0ysm as Point of T;
A100: ||.u2cf2n-f1.ym.|| < e/4 by A94,A99,NORMSP_2:def 1;
i in Seg len PS by A26,A92,FINSEQ_1:def 3; then
g0.ys in Ball( (U2*CF2)/.(sigm.i),e/4 ) by A89; then
g0.ys in { y where y is Element of MURSTPS :
dist ((U2*CF2)/.(sigm.i),y) < e/4 } by METRIC_1:def 14; then
A101: ex y be Element of MURSTPS st g0.ys = y
& dist ((U2*CF2)/.(sigm.i),y) < e/4; then
reconsider g0ys=g0.ys as Point of MURSTPS;
reconsider g0ysm =g0ys as Point of MetricSpaceNorm T;
A102: dist (u2cf2,g0ysm) < e/4 by A101,TOPMETR:def 1;
reconsider g0ysn=g0ysm as Point of T;
A103: ||.u2cf2n-g1.ym.|| < e/4 by A94,A102,NORMSP_2:def 1;
u2cf2n -f1.xm = u2cf2n -f1.ym + f1.ym -f1.xm by RLVECT_4:1
.= u2cf2n -f1.ym + (f1.ym -f1.xm) by RLVECT_1:28; then
A104:||.u2cf2n -f1.xm.||
<= ||.u2cf2n -f1.ym.|| + ||.f1.ym -f1.xm.|| by NORMSP_1:def 1;
||.u2cf2n -f1.ym.|| + ||.f1.ym -f1.xm.||
< e/4 + e/4 by A96,A100,XREAL_1:8; then
A105: ||.u2cf2n -f1.xm.|| < e/2 by XXREAL_0:2,A104;
u2cf2n -g1.xm = u2cf2n -g1.ym + g1.ym -g1.xm by RLVECT_4:1
.= u2cf2n -g1.ym + (g1.ym -g1.xm) by RLVECT_1:28; then
A106:||.u2cf2n -g1.xm.||
<= ||.u2cf2n -g1.ym.|| + ||.g1.ym -g1.xm.|| by NORMSP_1:def 1;
||.u2cf2n -g1.ym.|| + ||.g1.ym -g1.xm.||
< e/4 + e/4 by A97,A103,XREAL_1:8; then
A107: ||.u2cf2n -g1.xm.|| < e/2 by XXREAL_0:2,A106;
f1.xm-g1.xm = f1.xm-u2cf2n +u2cf2n - g1.xm by RLVECT_4:1
.= f1.xm-u2cf2n +(u2cf2n - g1.xm) by RLVECT_1:28; then
||.f1.xm-g1.xm.||
<= ||.f1.xm-u2cf2n.|| + ||.u2cf2n - g1.xm.|| by NORMSP_1:def 1; then
A108: ||.f1.xm-g1.xm.||
<= ||.u2cf2n - f1.xm.|| + ||.u2cf2n - g1.xm.|| by NORMSP_1:7;
||.u2cf2n - f1.xm.|| + ||.u2cf2n - g1.xm.||
< e/2 + e/2 by A105,A107,XREAL_1:8;
hence ||.f0.x-g0.x.|| <= e by XXREAL_0:2,A108;
end;
reconsider f1=f,g1=g as Point of
MetricSpaceNorm Z by TOPMETR:def 1,TARSKI:def 3;
reconsider f2=f1,g2=g1 as Point of Z;
A109: f2 in BoundedFunctions (the carrier of S,T) &
g2 in BoundedFunctions (the carrier of S,T) by C0SP3:34;
reconsider f3=f2,g3=g2 as Point of
R_NormSpace_of_BoundedFunctions (the carrier of S,T) by C0SP3:34;
reconsider f4=f2,g4=g2 as bounded Function of the carrier of S,T
by RSSPACE4:def 5,A109;
reconsider fg4=f3-g3 as bounded Function of the carrier of S,T
by RSSPACE4:def 5;
A110: ||.f3-g3.|| = upper_bound (PreNorms fg4) by RSSPACE4:14;
for s be Real st s in PreNorms fg4 holds s <= e
proof
let s be Real;
assume s in PreNorms fg4; then
consider t be Element of S such that
A111: s = ||.(fg4 . t).||;
fg4 . t = f4.t-g4.t by RSSPACE4:24
.=f0.t -g0.t;
hence thesis by A90,A111;
end; then
A112: ||.f3-g3.|| <= e by A110,SEQ_4:45;
A113: (-1)*g2 = (-1)*g3 by C0SP3:39;
f2-g2 =f2+(-1)*g2 by RLVECT_1:16
.=f3+(-1)*g3 by C0SP3:38,A113
.=f3-g3 by RLVECT_1:16; then
||.f2-g2.|| <= e by A112,C0SP3:36; then
dist(f1,g1) <= e by NORMSP_2:def 1; then
dist(f,g) <= e by TOPMETR:def 1;
hence dist(f,g) < e0 by A8,XXREAL_0:2;
end;
A114: for f be Point of MZH
holds ex sigm be Function of Seg len PS,Seg len CF2 st f in BST.sigm
proof
let f be Point of MZH;
f in H by A3; then
f in Z; then
ex g be Function of the carrier of S, the carrier of T
st f=g & g is continuous; then
reconsider g=f as Function of the carrier of S, the carrier of T;
defpred QQ[object,object] means
ex i,j be Nat st i=$1 & j=$2 &
g.(PS/.i) in Ball ((U2*CF2)/.j,e/4);
A115: for x be object st x in Seg len PS
ex y be object st y in Seg len CF2 & QQ[x,y]
proof
let x be object;
assume A116: x in Seg len PS; then
reconsider i = x as Nat;
A117: i in dom PS by A116,FINSEQ_1:def 3;
consider NHx be non empty Subset of T,
CHx be non empty Subset of MetricSpaceNorm T such that
A119: NHx= {f.(PS/.i) where f is Function of S,T :f in H }
& STPS/.i = Cl(NHx) by A40,A117,A25,A39;
A120: g.(PS/.i) in NHx by A119,A3;
NHx c= Cl(NHx) by NORMSP_3:4; then
A121: g.(PS/.i) in STPS/.i by A120,A119;
A122: i in dom STPS by A117,A25,A39;
A123: g.(PS/.i) in STPS.i by A121,PARTFUN1:def 6,A117,A25,A39;
STPS.i in rng STPS by A122,FUNCT_1:3; then
g.(PS/.i) in URSTPS by A123,TARSKI:def 4; then
g.(PS/.i) in the carrier of MURSTPS by TOPMETR:def 2; then
consider V be set such that
A124: g.(PS/.i) in V & V in rng CF2 by A80,TARSKI:def 4;
consider j be object such that
A125: j in dom CF2 & V=CF2.j by A124,FUNCT_1:def 3;
A126: j in Seg card BM02 by A72,FINSEQ_1:def 3,A125;
reconsider j as Nat by A125;
A127: CF2.j = Ball((U2*CF2)/.j,e/4) by A77,A75,A126;
j in Seg len CF2 by FINSEQ_1:def 3,A125;
hence thesis by A124,A125,A127;
end;
consider sigm being Function of Seg len PS,Seg len CF2 such that
A128: for x being object st x in Seg len PS
holds QQ[x,sigm.x] from FUNCT_2:sch 1(A115);
A129: for i be Nat st i in Seg len PS
holds g.(PS/.i) in Ball( (U2*CF2)/.(sigm.i),e/4 )
proof
let i be Nat;
assume i in Seg len PS; then
ex i0,j0 be Nat st i0=i & j0=sigm.i &
g.(PS/.i0) in Ball ((U2*CF2)/.j0,e/4) by A128;
hence thesis;
end;
A130: BST.sigm = { f where f is Function of S,T :f in MZH
& for i be Nat st i in Seg len PS
holds f.(PS/.i) in Ball( (U2*CF2)/.(sigm.i),e/4 ) } by A83;
take sigm;
g in MZH;
hence f in BST.sigm by A130,A129;
end;
A131: for sigm be Function of Seg len PS,Seg len CF2
holds ex f be Point of MZH st BST.sigm c= Ball (f,e0)
proof
let sigm be Function of Seg len PS,Seg len CF2;
per cases;
suppose A132: BST.sigm = {};
set f = the Point of MZH;
take f;
thus BST.sigm c= Ball (f,e0) by A132;
end;
suppose BST.sigm <> {}; then
consider f be object such that
A133: f in BST.sigm by XBOOLE_0:def 1;
sigm in Funcs(Seg len PS,Seg len CF2) by A65,FUNCT_2:8; then
A134: BST.sigm in bool the carrier of MZH by FUNCT_2:5; then
reconsider f as Point of MZH by A133;
take f;
let z be object;
assume A135:z in BST.sigm; then
reconsider g = z as Point of MZH by A134;
dist(f,g) < e0 by A133,A135,A85; then
g in { y where y is Point of MZH : dist(f,y) < e0 };
hence z in Ball (f,e0) by METRIC_1:def 14;
end;
end;
defpred PP[object,object] means
ex f be Point of MZH st
BST.$1 c= Ball(f,e0) & $2 = Ball(f,e0);
A136: for z be object st z in Funcs(Seg len PS,Seg len CF2)
ex f be object st f in bool (the carrier of MZH) & PP[z,f]
proof
let z be object;
assume z in Funcs(Seg len PS,Seg len CF2); then
reconsider sigm = z as Function of Seg len PS,Seg len CF2 by FUNCT_2:66;
ex f being Point of MZH st BST.sigm c= Ball (f,e0) by A131;
hence thesis;
end;
consider FF be Function of Funcs(Seg len PS,Seg len CF2),
bool the carrier of MZH such that
A138: for z being object
st z in Funcs(Seg len PS,Seg len CF2)
holds PP[z,FF.z] from FUNCT_2:sch 1(A136);
A139: dom FF = Funcs(Seg len PS,Seg len CF2) by FUNCT_2:def 1;
reconsider L = rng FF as finite set by A84;
reconsider L as Subset-Family of MZH;
take L;
thus L is finite;
the carrier of MZH c= union L
proof
let f be object;
assume f in the carrier of MZH; then
reconsider g = f as Point of MZH;
consider sigm be Function of Seg len PS,Seg len CF2 such that
A140: g in BST.sigm by A114;
A141: sigm in Funcs(Seg len PS,Seg len CF2) by A65,FUNCT_2:8; then
consider w be Point of MZH such that
A142: BST.sigm c= Ball(w,e0) & FF.sigm = Ball(w,e0) by A138;
FF.sigm in rng FF by FUNCT_1:3,A141,A139;
hence f in union L by TARSKI:def 4,A140,A142;
end;
hence the carrier of MZH = union L;
thus for C being Subset of MZH st C in L holds
ex w being Element of MZH st C = Ball (w,e0)
proof
let C be Subset of MZH;
assume C in L; then
consider x be object such that
A145: x in dom FF & C = FF.x by FUNCT_1:def 3;
consider w be Point of MZH such that
A146: BST.x c= Ball(w,e0) & FF.x = Ball(w,e0) by A138,A145;
take w;
thus C = Ball (w,e0) by A145,A146;
end;
end;
hence (MetricSpaceNorm Z) | H is totally_bounded;
end;
theorem
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace,
G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T))
st S = TopSpaceMetr(M) & T is complete & G = H
holds
Cl(H) is sequentially_compact
iff
G is equicontinuous
&
for x be Point of S, Hx be non empty Subset of MetricSpaceNorm T
st Hx = {f.x where f is Function of S,T :f in H }
holds (MetricSpaceNorm T) | Cl(Hx) is compact
proof
let M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace;
let G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T);
assume A1: S = TopSpaceMetr(M) & T is complete;
assume A2: G = H;
set Z = R_NormSpace_of_ContinuousFunctions(S,T);
(MetricSpaceNorm Z) | H is totally_bounded iff
Cl(H) is sequentially_compact by A1,Th11;
hence thesis by A1,A2,Th16;
end;
theorem Th18:
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace,
F be non empty Subset of
R_NormSpace_of_ContinuousFunctions(S,T),
G be Subset of Funcs(the carrier of M, the carrier of T)
st S = TopSpaceMetr(M) & T is complete & G = F holds
Cl(F) is compact
iff
G is equicontinuous
&
for x be Point of S,
Fx be non empty Subset of MetricSpaceNorm T
st Fx = {f.x where f is Function of S,T :f in F }
holds
(MetricSpaceNorm T) | Cl(Fx) is compact
proof
let M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace;
let F be non empty Subset of
R_NormSpace_of_ContinuousFunctions(S,T),
G be Subset of Funcs(the carrier of M, the carrier of T);
reconsider H = F as non empty Subset of
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T));
assume A1: S = TopSpaceMetr(M) & T is complete;
assume A2: G = F;
set Z = R_NormSpace_of_ContinuousFunctions(S,T);
(MetricSpaceNorm Z) | H is totally_bounded iff
Cl(F) is compact by A1,Th12;
hence thesis by A1,A2,Th16;
end;
theorem
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace,
F be non empty Subset of
R_NormSpace_of_ContinuousFunctions(S,T),
G be Subset of Funcs(the carrier of M, the carrier of T)
st S = TopSpaceMetr(M) & T is complete & G = F
holds
Cl(F) is compact
iff
( for x be Point of M holds G is_equicontinuous_at x ) &
for x be Point of S,
Fx be non empty Subset of MetricSpaceNorm T
st Fx = {f.x where f is Function of S,T :f in F }
holds (MetricSpaceNorm T) | Cl(Fx) is compact
proof
let M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace;
let F be non empty Subset of
R_NormSpace_of_ContinuousFunctions(S,T),
G be Subset of Funcs(the carrier of M, the carrier of T);
assume A1: S = TopSpaceMetr(M) & T is complete;
assume G = F; then
Cl(F) is compact iff G is equicontinuous &
for x be Point of S, Fx be non empty Subset of MetricSpaceNorm T
st Fx = {f.x where f is Function of S,T :f in F } holds
(MetricSpaceNorm T) | Cl(Fx) is compact by Th18,A1;
hence thesis by Th5,A1;
end;
theorem Th20:
for T be NormedLinearTopSpace holds
T is compact iff TopSpaceNorm T is compact
proof
let T be NormedLinearTopSpace;
consider RNS be RealNormSpace such that
A1: RNS = the NORMSTR of T
& the topology of T = the topology of TopSpaceNorm RNS by C0SP3:def 6;
A2: TopSpaceMetr MetricSpaceNorm T
= TopStruct(# the carrier of T, the topology of T #) by A1,Th15;
A3: [#] T = [#](TopSpaceMetr MetricSpaceNorm T);
hereby assume T is compact; then
[#] T is compact Subset of TopSpaceMetr MetricSpaceNorm T
by A2,COMPTS_1:23,COMPTS_1:1;
hence TopSpaceNorm T is compact by A3,COMPTS_1:1;
end;
assume TopSpaceNorm T is compact; then
[#] T is compact Subset of TopSpaceMetr MetricSpaceNorm T by A3,COMPTS_1:1;
hence T is compact by A2,COMPTS_1:1,COMPTS_1:23;
end;
theorem Th21:
for T be NormedLinearTopSpace,
X be set holds
X is compact Subset of T
iff
X is compact Subset of TopSpaceNorm T
proof
let T be NormedLinearTopSpace, X be set;
consider RNS be RealNormSpace such that
A1: RNS = the NORMSTR of T
& the topology of T = the topology of TopSpaceNorm RNS by C0SP3:def 6;
A2: TopSpaceMetr MetricSpaceNorm T
= TopStruct(# the carrier of T, the topology of T #) by A1,Th15;
hence X is compact Subset of T implies
X is compact Subset of TopSpaceNorm T by COMPTS_1:23;
assume X is compact Subset of TopSpaceNorm T; then
reconsider X0=X as compact Subset of TopSpaceNorm T;
X0 is compact Subset of TopStruct(# the carrier of T, the topology of T #)
by A2;
hence X is compact Subset of T by COMPTS_1:23;
end;
theorem ThLast:
for T be NormedLinearTopSpace
st T is compact holds
T is complete
proof
let T be NormedLinearTopSpace;
assume T is compact; then
TopSpaceNorm T is compact by Th20; then
MetricSpaceNorm T is sequentially_compact by TOPMETR4:11;
hence T is complete by Th6,TOPMETR4:12;
end;
registration
cluster compact -> complete for NormedLinearTopSpace;
coherence by ThLast;
end;
::$N Arzelà âAscoli theorem
::$L https://en.wikipedia.org/wiki/Arzelà âAscoli_theorem Arzelà âAscoli theorem
theorem
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace,
U be compact Subset of T,
F be non empty Subset of
R_NormSpace_of_ContinuousFunctions(S,T),
G be Subset of Funcs(the carrier of M, the carrier of T)
st S = TopSpaceMetr(M) & T is complete
& G = F & for f be Function st f in F holds rng f c= U
holds
( Cl(F) is compact implies G is equibounded & G is equicontinuous )
&
( G is equicontinuous implies Cl(F) is compact )
proof
let M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace,U be compact Subset of T;
let F be non empty Subset of
R_NormSpace_of_ContinuousFunctions(S,T),
G be Subset of Funcs(the carrier of M, the carrier of T);
assume that
A1: S = TopSpaceMetr(M) and
A2: T is complete;
assume
A3: G = F & for f be Function st f in F holds rng f c= U;
reconsider H = F as non empty Subset of
MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T);
set Z = R_NormSpace_of_ContinuousFunctions(S,T);
(MetricSpaceNorm Z) | H is totally_bounded iff
Cl(F) is compact by A2,Th12;
hence Cl(F) is compact implies G is equibounded & G is equicontinuous
by A2,A1,Th13,A3;
assume
A5:G is equicontinuous;
for x be Point of S,
Fx be non empty Subset of MetricSpaceNorm T
st Fx = {f.x where f is Function of S,T :f in F } holds
(MetricSpaceNorm T) | Cl(Fx) is compact
proof
let x be Point of S,
Fx be non empty Subset of MetricSpaceNorm T;
assume
A6: Fx = {f.x where f is Function of S,T :f in F };
reconsider V = U as Subset of TopSpaceNorm T;
A7: V is compact by Th21;
A10: Fx c= V
proof
let y be object;
assume y in Fx; then
consider f be Function of S,T such that
A8:y=f.x & f in F by A6;
A9: f.x in rng f by FUNCT_2:4;
rng f c= V by A3,A8;
hence y in V by A8,A9;
end;
consider Gx be Subset of TopSpaceMetr MetricSpaceNorm T such that
A11: Fx = Gx & Cl(Fx) = Cl Gx by Def1;
reconsider HClx=Cl(Gx) as non empty Subset of MetricSpaceNorm T by A11;
A12:TopSpaceNorm T is T_2 by PCOMPS_1:34;
Cl(Gx) c= Cl V by A10,A11,PRE_TOPC:19; then
Cl(Gx) c= V by A12,A7,PRE_TOPC:22; then
Cl(Gx) is compact by Th21,COMPTS_1:9; then
HClx is sequentially_compact by TOPMETR4:15;
hence (MetricSpaceNorm T) | Cl(Fx) is compact by A11,TOPMETR4:14;
end;
hence thesis by Th18,A1,A2,A3,A5;
end;