Copyright (c) 1991 Association of Mizar Users
environ
vocabulary METRIC_1, SETFAM_1, RELAT_2, FUNCT_1, POWER, SEQ_1, SEQ_2,
ORDINAL2, ABSVALUE, ARYTM_1, FINSET_1, TARSKI, NORMSP_1, RELAT_1,
ARYTM_3, BHSP_3, ALI2, PRE_TOPC, PCOMPS_1, COMPTS_1, BOOLE, SUBSET_1,
LATTICES, FINSEQ_1, TBSP_1, HAHNBAN, ARYTM;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, REAL_1, NAT_1, RELAT_1,
ORDINAL1, FUNCT_1, FINSEQ_1, DOMAIN_1, SETFAM_1, FUNCT_2, FINSET_1,
STRUCT_0, PRE_TOPC, TOPS_2, ABSVALUE, SEQ_1, SEQ_2, COMPTS_1, METRIC_1,
POWER, PCOMPS_1, ALI2, NORMSP_1;
constructors REAL_1, NAT_1, DOMAIN_1, TOPS_2, ABSVALUE, SEQ_2, COMPTS_1,
POWER, PCOMPS_1, ALI2, NORMSP_1, MEMBERED, XBOOLE_0;
clusters FINSET_1, PRE_TOPC, PCOMPS_1, STRUCT_0, XREAL_0, FINSEQ_1, METRIC_1,
RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions COMPTS_1, TARSKI, ORDINAL1, XBOOLE_0;
theorems METRIC_1, SUBSET_1, REAL_1, SQUARE_1, REAL_2, FUNCT_1, PCOMPS_1,
PRE_TOPC, TOPS_2, TARSKI, COMPTS_1, NAT_1, SEQ_2, ZFMISC_1, AXIOMS,
POWER, SERIES_1, ABSVALUE, FUNCT_2, SETFAM_1, FINSEQ_1, ALI2, NORMSP_1,
RELSET_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1;
schemes DOMAIN_1, SETFAM_1, NAT_1, SEQ_1, RECDEF_1, FINSET_1;
begin
reserve M for non empty MetrSpace,
c,g1,g2 for Element of M;
reserve N for non empty MetrStruct,
w for Element of N,
G for Subset-Family of N,
C for Subset of N;
reserve R for Reflexive (non empty MetrStruct);
reserve T for Reflexive symmetric triangle (non empty MetrStruct),
t1 for Element of T,
Y for Subset-Family of T,
P for Subset of T;
reserve f for Function,
n,m,p,n1,n2,k for Nat,
r,s,L for Real,
x,y for set;
theorem Th1:
for L st 0<L & L<1 holds for n,m st n<=m holds L to_power m <= L to_power n
proof
let L such that A1: 0<L & L<1;
let n,m such that A2:n<=m;
now per cases by A2,REAL_1:def 5;
suppose n<m;
hence L to_power n >= L to_power m by A1,POWER:45;
suppose n=m;
hence L to_power n >= L to_power m;
end;
hence thesis;
end;
theorem Th2:
for L st 0<L & L<1 holds for k holds L to_power k <= 1 & 0 < L to_power k
proof
let L; assume A1: 0<L & L<1;
defpred X[Nat] means L to_power $1 <= 1 & 0 < L to_power $1;
A2: X[0]
proof
L to_power 0 = 1 by POWER:29;
hence thesis;
end;
A3: for k st X[k] holds X[k+1]
proof
let k be Nat such that
A4: L to_power k <= 1 & 0 < L to_power k;
A5: L to_power (k+1) = L to_power k*L to_power 1 by A1,POWER:32
.= L to_power k*L by POWER:30;
L to_power k*L<=L to_power k by A1,A4,REAL_2:147;
hence thesis by A1,A4,A5,AXIOMS:22,REAL_2:122;
end;
thus for k holds X[k] from Ind(A2,A3);
end;
theorem Th3:
for L st 0<L & L<1 holds for s st 0<s ex n st L to_power n<s
proof
let L such that A1: 0<L & L<1;
deffunc U(Nat) = L to_power ($1+1);
consider rseq being Real_Sequence such that
A2: for n holds rseq.n = U(n) from ExRealSeq;
A3: rseq is convergent & lim rseq = 0 by A1,A2,SERIES_1:1;
let s; assume 0<s;
then consider n such that
A4: for m st n<=m holds abs(rseq.m-0)<s by A3,SEQ_2:def 7;
A5: 0<L to_power (n+1) by A1,Th2;
A6: abs(rseq.n-0) = abs(L to_power (n+1)) by A2
.= L to_power (n+1) by A5,ABSVALUE:def 1;
take n+1;
thus thesis by A4,A6;
end;
definition let N;
attr N is totally_bounded means :Def1:
for r st r>0 ex G st G is finite & the carrier of N = union G &
for C st C in G ex w st C = Ball(w,r);
end;
definition let N;
redefine mode sequence of N -> Function means :Def2:
dom it = NAT & rng it c= the carrier of N;
compatibility
proof let f be Function;
thus f is sequence of N implies
dom f = NAT & rng f c= the carrier of N by FUNCT_2:def 1,RELSET_1:12;
assume dom f = NAT & rng f c= the carrier of N;
then f is Function of NAT, the carrier of N by FUNCT_2:def 1,RELSET_1:11;
hence thesis by NORMSP_1:def 3;
end;
coherence
proof let f be sequence of N;
thus thesis;
end;
end;
reserve S1 for sequence of M,
S2 for sequence of N;
Lm1: f is sequence of N iff
(dom f = NAT & for x st x in NAT holds f.x is Element of N)
proof
thus f is sequence of N implies
(dom f = NAT & for x st x in NAT holds f.x is Element of N)
proof
assume A1:f is sequence of N;
hence dom f = NAT by Def2;
A2: rng f c= the carrier of N by A1,Def2;
let x;
assume x in NAT;
then x in dom f by A1,Def2;
then f.x in rng f by FUNCT_1:def 5;
hence f.x is Element of N by A2;
end;
assume that
A3: dom f = NAT and
A4: for x st x in NAT holds f.x is Element of N;
now let y; assume
y in rng f;
then consider x such that A5: x in dom f and
A6: y=f.x by FUNCT_1:def 5;
f.x is Element of N by A3,A4,A5;
hence y in the carrier of N by A6;
end;
then rng f c= the carrier of N by TARSKI:def 3;
hence thesis by A3,Def2;
end;
canceled;
theorem
f is sequence of N iff
dom f = NAT & for n holds f.n is Element of N
proof
thus f is sequence of N implies
(dom f = NAT & for n holds f.n is Element of N) by Lm1;
assume that
A1: dom f = NAT and
A2: for n holds f.n is Element of N;
for x holds x in NAT implies f.x is Element of N by A2;
hence thesis by A1,Lm1;
end;
definition let N,S2;
attr S2 is convergent means :Def3:
ex x being Element of N st
for r st r>0 ex n st for m st n<=m holds dist(S2.m,x)<r;
end;
definition let M,S1;
assume A1:S1 is convergent;
func lim S1 -> Element of M means
for r st r>0 ex n st for m st m>=n holds dist(S1.m,it)<r;
existence by A1,Def3;
uniqueness
proof
given g1,g2 such that
A2: for r st r>0 ex n st for m st n<=m holds dist(S1.m,g1)<r and
A3: for r st r>0 ex n st for m st n<=m holds dist(S1.m,g2)<r and
A4: g1<>g2;
A5: dist(g1,g2)<>0 by A4,METRIC_1:2;
A6: dist(g1,g2)>=0 by METRIC_1:5;
then A7: 0< dist(g1,g2)/4 by A5,SEQ_2:3;
set a=dist(g1,g2)/4;
consider n1 such that
A8: for m st n1<=m holds dist(S1.m,g1)<a by A2,A7;
consider n2 such that
A9: for m st n2<=m holds dist(S1.m,g2)<a by A3,A7;
set k=n1+n2;
n1<=k by NAT_1:37;
then A10: dist(S1.k,g1)<a by A8;
n2<=k by NAT_1:37;
then dist(S1.k,g2)<a by A9;
then A11: dist(g1,S1.k)+dist(S1.k,g2)<a+a by A10,REAL_1:67;
dist(g1,g2)<=dist(g1,S1.k)+dist(S1.k,g2) by METRIC_1:4;
then dist(g1,g2)<a+a by A11,AXIOMS:22;
then dist(g1,g2)<dist(g1,g2)/2 by XCMPLX_1:72;
hence contradiction by A5,A6,SEQ_2:4;
end;
end;
definition let N,S2;
attr S2 is Cauchy means:Def5:
for r st r>0 ex p st for n,m st p<=n & p<=m holds dist(S2.n,S2.m)<r;
end;
definition let N;
attr N is complete means :Def6:
for S2 st S2 is Cauchy holds S2 is convergent;
end;
canceled;
theorem Th7:
N is triangle symmetric & S2 is convergent implies S2 is Cauchy
proof
assume that
A1: N is triangle and
A2: N is symmetric;
assume S2 is convergent;
then consider g being Element of N such that
A3: for r st 0<r ex n st for m st n<=m holds dist(S2.m,g)<r by Def3;
let r; assume 0<r;
then 0<r/2 by SEQ_2:3;
then consider n such that
A4: for m st n<=m holds dist(S2.m,g)<r/2 by A3;
take n;
let m,m' be Nat; assume
A5: m>=n & m'>=n;
then A6: dist(S2.m,g)<r/2 by A4;
dist(S2.m',g)<r/2 by A4,A5;
then dist(g,S2.m')<r/2 by A2,METRIC_1:3;
then A7: dist(S2.m,g)+dist(g,S2.m')<r/2+r/2 by A6,REAL_1:67;
dist(S2.m,S2.m')<=dist(S2.m,g)+dist(g,S2.m') by A1,METRIC_1:4;
then dist(S2.m,S2.m')<r/2+r/2 by A7,AXIOMS:22;
hence thesis by XCMPLX_1:66;
end;
definition let M be triangle symmetric (non empty MetrStruct);
cluster convergent -> Cauchy sequence of M;
coherence by Th7;
end;
theorem Th8:
N is symmetric implies
(S2 is Cauchy iff
for r st r>0 ex p st for n,k st p<=n holds dist(S2.(n+k),S2.n)<r)
proof
assume
A1: N is symmetric;
thus S2 is Cauchy implies
for r st r>0 ex p st for n,k st p<=n holds dist(S2.(n+k),S2.n)<r
proof
assume
A2: S2 is Cauchy;
let r; assume 0<r;
then consider p such that
A3: for n,m st p<=n & p<=m holds dist(S2.n,S2.m)<r by A2,Def5;
take p;
let n,k be Nat such that
A4:p<=n;
n<=n+k by NAT_1:29;
then p<=n+k & p<=n by A4,AXIOMS:22;
hence thesis by A3;
end;
assume
A5: for r st r>0 ex p st for n,k st p<=n holds dist(S2.(n+k),S2.n)<r;
let r; assume 0<r;
then consider p such that
A6: for n,k st p<=n holds dist(S2.(n+k),S2.n)<r by A5;
take p;
let n,m such that
A7: p<=n & p<=m;
now per cases;
suppose n<=m; then ex k st m=n+k by NAT_1:28;
then dist(S2.m,S2.n)<r by A6,A7;
hence dist(S2.n,S2.m)<r by A1,METRIC_1:3;
suppose m<=n; then ex k st n=m+k by NAT_1:28;
hence dist(S2.n,S2.m)<r by A6,A7;
end;
hence thesis;
end;
theorem for f being contraction of M st M is complete
ex c st f.c = c & for y being Element of M st f.y=y holds y=c
proof
let f be contraction of M; consider L such that
A1: 0<L & L<1 and
A2: for x,y being Point of M holds
dist(f.x,f.y)<=L*dist(x,y) by ALI2:def 1;
A3: 1-L>0 by A1,SQUARE_1:11;
A4: 1-L<>0 by A1,SQUARE_1:11;
assume
A5: M is complete;
ex S1 st for n holds S1.(n+1)=f.(S1.n)
proof
deffunc U(Nat,Element of M) = f.$2;
consider z being Element of M;
ex h being Function of NAT,the carrier of M st
h.0 = z &
for n being Nat holds h.(n+1) = U(n,h.n) from LambdaRecExD;
then consider h being Function of NAT,the carrier of M such that
A6: h.0 = z & for n being Nat holds h.(n + 1) = f.(h.n);
dom h = NAT & rng h c= the carrier of M
by FUNCT_2:def 1,RELSET_1:12;
then reconsider h as sequence of M by Def2;
take h;
let n;
thus h.(n+1)=f.(h.n) by A6;
end;
then consider S1 such that
A7: for n holds S1.(n+1)=f.(S1.n);
set r = dist(S1.1,S1.0);
A8: 0<=r by METRIC_1:5;
now per cases;
suppose A9: 0=r;
A10: f.(S1.0) = S1.(0+1) by A7
.= S1.0 by A9,METRIC_1:2;
for y being Element of M st f.y=y holds y=S1.0
proof
let y be Element of M; assume
A11: f.y=y;
assume y<>S1.0;
then A12: dist(y,S1.0)<>0 by METRIC_1:2;
dist(y,S1.0)>=0 by METRIC_1:5;
then L*dist(y,S1.0)<dist(y,S1.0) by A1,A12,REAL_2:145;
hence contradiction by A2,A10,A11;
end;
hence ex c st f.c = c &
for y being Element of M st f.y=y holds y=c by A10;
suppose A13: 0<>r;
A14: for n holds dist(S1.(n+1),S1.n)<=r*L to_power n
proof
defpred X[Nat] means dist(S1.($1+1),S1.$1)<=r*L to_power $1;
A15: X[0]
proof
dist(S1.(0+1),S1.0) = r*1
.= r*L to_power 0 by POWER:29;
hence thesis;
end;
A16: for k st X[k] holds X[k+1]
proof
let k be Nat such that
A17: dist(S1.(k+1),S1.k)<=r*L to_power k;
dist(S1.((k+1)+1),S1.(k+1))
= dist(f.(S1.(k+1)),S1.(k+1)) by A7
.= dist(f.(S1.(k+1)),f.(S1.k)) by A7;
then A18: dist(S1.((k+1)+1),S1.(k+1)) <= L*dist(S1.(k+1),S1.k) by A2;
A19: L*dist(S1.(k+1),S1.k)<=L*(r*L to_power k) by A1,A17,AXIOMS:25;
L*(r*L to_power k) = r*(L*L to_power k) by XCMPLX_1:4
.= r*(L to_power k*L to_power 1) by POWER:30
.= r*L to_power (k+1) by A1,POWER:32;
hence thesis by A18,A19,AXIOMS:22;
end;
thus for k holds X[k] from Ind(A15,A16);
end;
A20: for n,k holds
dist(S1.(n+k),S1.n)<=L to_power n*dist(S1.k,S1.0)
proof
defpred X[Nat] means for k holds
dist(S1.($1+k),S1.$1)<=L to_power $1*dist(S1.k,S1.0);
A21: X[0]
proof
let n;
L to_power 0*dist(S1.n,S1.0)
= 1*dist(S1.n,S1.0) by POWER:29
.= dist(S1.n,S1.0);
hence thesis;
end;
A22: for n st X[n] holds X[n+1]
proof
let n such that
A23: for k holds
dist(S1.(n+k),S1.n)<=L to_power n*dist(S1.k,S1.0);
let k be Nat;
A24: dist(S1.(n+k),S1.n)<=L to_power n*dist(S1.k,S1.0) by A23;
dist(S1.((n+1)+k),S1.(n+1))
= dist(S1.((n+k)+1),S1.(n+1)) by XCMPLX_1:1
.= dist(f.(S1.(n+k)),S1.(n+1)) by A7
.= dist(f.(S1.(n+k)),f.(S1.n)) by A7;
then A25: dist(S1.((n+1)+k),S1.(n+1))<=L*dist(S1.(n+k),S1.n) by A2;
A26: L*dist(S1.(n+k),S1.n)
<=L*(L to_power n*dist(S1.k,S1.0)) by A1,A24,AXIOMS:25;
L*(L to_power n*dist(S1.k,S1.0))
= L*L to_power n*dist(S1.k,S1.0) by XCMPLX_1:4
.= L to_power n*L to_power 1*dist(S1.k,S1.0) by POWER:30
.= L to_power (n+1)*dist(S1.k,S1.0) by A1,POWER:32;
hence thesis by A25,A26,AXIOMS:22;
end;
thus for k holds X[k] from Ind(A21,A22);
end;
A27: for k holds dist(S1.k,S1.0)<=r*((1-L to_power k)/(1-L))
proof
defpred X[Nat] means dist(S1.$1,S1.0)<=r*((1-L to_power $1)/(1-L));
A28: X[0]
proof
r*((1-L to_power 0)/(1-L)) = r*((1-1)/(1-L)) by POWER:29
.= 0;
hence thesis by METRIC_1:1;
end;
A29: for k st X[k] holds X[k+1]
proof
let k be Nat such that
A30: dist(S1.k,S1.0)<=r*((1-L to_power k)/(1-L));
A31: dist(S1.(k+1),S1.0)
<= dist(S1.(k+1),S1.k) + dist(S1.k,S1.0) by METRIC_1:4;
dist(S1.(k+1),S1.k)<=r*L to_power k by A14;
then A32: dist(S1.(k+1),S1.k) + dist(S1.k,S1.0)
<= r*L to_power k + r*((1-L to_power k)/(1-L)) by A30,REAL_1:55;
r*L to_power k + r*((1-L to_power k)/(1-L))
= r*(L to_power k + (1-L to_power k)/(1-L)) by XCMPLX_1:8
.= r*(L to_power k/(1-L)*(1-L) + (1-L to_power k)/(1-L))
by A4,XCMPLX_1:88
.= r*((1-L)*L to_power k/(1-L) + (1-L to_power k)/(1-L))
by XCMPLX_1:75
.= r*(((1-L)*L to_power k + (1-L to_power k))/(1-L))
by XCMPLX_1:63
.= r*((1*L to_power k-L*L to_power k + (1-L to_power k))/(1-L))
by XCMPLX_1:40
.= r*((1-L*L to_power k)/(1-L)) by XCMPLX_1:39
.= r*((1-L to_power k*L to_power 1)/(1-L)) by POWER:30
.= r*((1-L to_power (k+1))/(1-L)) by A1,POWER:32;
hence thesis by A31,A32,AXIOMS:22;
end;
thus for k holds X[k] from Ind(A28,A29);
end;
A33: for k holds dist(S1.k,S1.0)<=r/(1-L)
proof
let k be Nat;
A34: dist(S1.k,S1.0)<=r*((1-L to_power k)/(1-L)) by A27;
L to_power k <= 1 & 0 < L to_power k by A1,Th2;
then 1-L to_power k<=1 by REAL_2:174;
then (1-L to_power k)/(1-L) <= 1/(1-L) by A3,REAL_1:73;
then r*((1-L to_power k)/(1-L)) <= r*(1/(1-L)) by A8,AXIOMS:25;
then dist(S1.k,S1.0)<=r*(1/(1-L)) by A34,AXIOMS:22;
hence thesis by XCMPLX_1:100;
end;
A35: for n,k holds
dist(S1.(n+k),S1.n)<=(r/(1-L))*L to_power n
proof
let n,k be Nat;
A36: dist(S1.k,S1.0)<=r/(1-L) by A33;
A37: dist(S1.(n+k),S1.n)<=L to_power n*dist(S1.k,S1.0) by A20;
0 <= L to_power n by A1,Th2;
then L to_power n*dist(S1.k,S1.0) <= L to_power n*(r/(1-L)) by A36,AXIOMS:25;
hence thesis by A37,AXIOMS:22;
end;
S1 is Cauchy
proof
for s st s>0 ex p st for n,k st p<=n holds dist(S1.(n+k),S1.n)<s
proof
let s such that
A38: s>0;
A39: r/(1-L)>0 by A3,A8,A13,REAL_2:127;
A40: r*(1-L)<>0 by A4,A13,XCMPLX_1:6;
(1-L)/r>0 by A3,A8,A13,REAL_2:127;
then (1-L)/r*s>0 by A38,REAL_2:122;
then consider p such that
A41: L to_power p<(1-L)/r*s by A1,Th3;
take p;
let n,k be Nat; assume p<=n;
then L to_power n<=L to_power p by A1,Th1;
then L to_power n<(1-L)/r*s by A41,AXIOMS:22;
then A42: (r/(1-L))*L to_power n<(r/(1-L))*((1-L)/r*s) by A39,REAL_1:70;
A43: dist(S1.(n+k),S1.n)<=(r/(1-L))*L to_power n by A35;
(r/(1-L))*((1-L)/r*s) = ((r/(1-L))*((1-L)/r))*s by XCMPLX_1:4
.= ((r*(1-L))/(r*(1-L)))*s by XCMPLX_1:77
.= 1*s by A40,XCMPLX_1:60
.= s;
hence thesis by A42,A43,AXIOMS:22;
end;
hence thesis by Th8;
end;
then S1 is convergent by A5,Def6;
then consider x being Element of M such that
A44: for r st r>0 ex n st
for m st n<=m holds dist(S1.m,x)<r by Def3;
A45: f.x = x
proof
assume x <> f.x;
then A46: dist(x,f.x) <> 0 by METRIC_1:2;
A47: dist(x,f.x) >= 0 by METRIC_1:5;
then A48: 0 < dist(x,f.x)/4 by A46,SEQ_2:3;
set a = dist(x,f.x)/4;
consider n such that
A49: for m st n<=m holds dist(S1.m,x)<a by A44,A48;
n<=n+1 by NAT_1:29;
then A50: dist(x,S1.(n+1))<a by A49;
dist(S1.(n+1),f.x) = dist(f.(S1.n),f.x) by A7;
then A51: dist(S1.(n+1),f.x) <= L*dist(S1.n,x) by A2;
A52: dist(S1.n,x)<a by A49;
dist(S1.n,x)>=0 by METRIC_1:5;
then L*dist(S1.n,x)<=dist(S1.n,x) by A1,REAL_2:147;
then dist(S1.(n+1),f.x)<= dist(S1.n,x) by A51,AXIOMS:22;
then dist(S1.(n+1),f.x)<a by A52,AXIOMS:22;
then dist(x,S1.(n+1))+dist(S1.(n+1),f.x)<a+a by A50,REAL_1:67;
then A53: dist(x,S1.(n+1))+dist(S1.(n+1),f.x)< dist(x,f.x)/2 by XCMPLX_1:
72;
A54: dist(x,f.x)<=dist(x,S1.(n+1))+dist(S1.(n+1),f.x) by METRIC_1:4;
dist(x,f.x)/2 < dist(x,f.x) by A46,A47,SEQ_2:4;
hence contradiction by A53,A54,AXIOMS:22;
end;
for y being Element of M st f.y=y holds y=x
proof
let y be Element of M; assume
A55: f.y=y;
assume y<>x;
then A56: dist(y,x)<>0 by METRIC_1:2;
dist(y,x)>=0 by METRIC_1:5;
then L*dist(y,x)<dist(y,x) by A1,A56,REAL_2:145;
hence contradiction by A2,A45,A55;
end;
hence ex c st f.c = c &
for y being Element of M st f.y=y holds y=c by A45;
end;
hence thesis;
end;
theorem
TopSpaceMetr(T) is compact implies T is complete
proof
set TM = TopSpaceMetr(T);
A1: TM = TopStruct (# the carrier of T,Family_open_set(T) #)
by PCOMPS_1:def 6;
assume A2: TopSpaceMetr(T) is compact;
let S2 be sequence of T such that
A3: S2 is Cauchy;
S2 is convergent
proof
defpred X[Subset of TopSpaceMetr T] means
ex p st $1 = {x where x is Point of T : ex n st p<=n & x = S2.n};
consider F being Subset-Family of TopSpaceMetr(T) such that
A4: for B being Subset of TopSpaceMetr(T) holds
B in F iff X[B] from SubFamEx;
A5: for p holds
{x where x is Point of T : ex n st p<=n & x = S2.n} <> {}
proof
let p be Nat;
(S2.p) in {x where x is Point of T : ex n st p<=n & x = S2.n};
hence thesis;
end;
defpred X[Point of T] means ex n st 0<=n & $1 = S2.n;
set B0 = {x where x is Point of T : X[x]};
A6: B0 is Subset of T from SubsetD;
then A7: B0 in F by A1,A4;
reconsider F as Subset-Family of TopSpaceMetr(T);
set G = clf F;
reconsider B0 as Subset of TopSpaceMetr(T) by A1,A6;
A8: Cl B0 in G by A7,PCOMPS_1:def 3;
A9: G is closed by PCOMPS_1:14;
G is centered
proof
thus G<>{} by A8;
let H be set such that
A10: H <> {} and
A11: H c= G and
A12: H is finite;
A13: H c= bool the carrier of TM by A11,XBOOLE_1:1;
H is c=-linear
proof
let B,C be set; assume
A14: B in H & C in H;
then reconsider B, C as Subset of TM by A13;
consider V being Subset of TM such that
A15: B = Cl V & V in F by A11,A14,PCOMPS_1:def 3;
consider W being Subset of TM such that
A16: C = Cl W & W in F by A11,A14,PCOMPS_1:def 3;
consider p such that
A17: V = {x where x is Point of T : ex n st p<=n & x = S2.n} by A4,A15;
consider q being Nat such that
A18: W = {x where x is Point of T : ex n st q<=n & x = S2.n} by A4,A16;
V c= W or W c= V
proof
now per cases;
case A19: q<=p;
thus V c= W
proof
let y be set;
assume y in V; then consider x being Point of T such that
A20: y = x & ex n st p<=n & x = S2.n by A17;
consider n such that
A21: p<=n & x = S2.n by A20;
q<=n & x = S2.n by A19,A21,AXIOMS:22;
hence y in W by A18,A20;
end;
case A22: p<=q;
thus W c= V
proof
let y be set;
assume y in W; then consider x being Point of T such that
A23: y = x & ex n st q<=n & x = S2.n by A18;
consider n such that
A24: q<=n & x = S2.n by A23;
p<=n & x = S2.n by A22,A24,AXIOMS:22;
hence y in V by A17,A23;
end;
end;
hence thesis;
end;
then B c= C or C c= B by A15,A16,PRE_TOPC:49;
hence thesis by XBOOLE_0:def 9;
end;
then consider m being set such that
A25: m in H and
A26: for C being set st C in H holds m c= C by A10,A12,ALI2:1;
A27: m c= meet H by A10,A26,SETFAM_1:6;
reconsider m as Subset of TM by A13,A25;
consider A being Subset of TM such that
A28: m = Cl A & A in F by A11,A25,PCOMPS_1:def 3;
A29: A <> {} by A4,A5,A28;
A c= m by A28,PRE_TOPC:48;
then m <> {} by A29,XBOOLE_1:3;
hence thesis by A27,XBOOLE_1:3;
end;
then meet G <> {} by A2,A9,COMPTS_1:13;
then consider c being Point of TM such that
A30: c in meet G by SUBSET_1:10;
reconsider c as Point of T by A1;
take c;
let r;
assume 0<r;
then A31: 0<r/2 by SEQ_2:3;
then consider p such that
A32: for n,m st p<=n & p<=m holds dist(S2.n,S2.m)<r/2
by A3,Def5;
defpred X[set] means ex n st p<=n & $1 = S2.n;
set B = {x where x is Point of T : X[x]};
A33: B is Subset of T from SubsetD;
then A34: B in F by A1,A4;
reconsider B as Subset of TopSpaceMetr(T) by A1,A33;
Cl B in G by A34,PCOMPS_1:def 3;
then A35: c in Cl B by A30,SETFAM_1:def 1;
dist(c,c)<r/2 by A31,METRIC_1:1;
then A36: c in Ball(c,r/2) by METRIC_1:12;
A37: Ball(c,r/2) in Family_open_set(T) by PCOMPS_1:33;
reconsider Z = Ball(c,r/2) as Subset of TopSpaceMetr(T)
by A1;
Z is open by A1,A37,PRE_TOPC:def 5;
then B meets Z by A35,A36,PRE_TOPC:def 13;
then consider g being set such that
A38: g in B /\ Z by XBOOLE_0:4;
A39: g in B & g in Z by A38,XBOOLE_0:def 3;
then reconsider g as Point of T;
consider x being Point of T such that
A40: g = x & ex n st p<=n & x = S2.n by A39;
consider n such that
A41: p<=n & x = S2.n by A40;
A42: dist(S2.n,c)<r/2 by A39,A40,A41,METRIC_1:12;
take p;
let m;
assume p<=m;
then dist(S2.m,S2.n)<r/2 by A32,A41;
then dist(S2.m,S2.n)+dist(S2.n,c)<r/2+r/2 by A42,REAL_1:67;
then A43: dist(S2.m,S2.n)+dist(S2.n,c)<r by XCMPLX_1:66;
dist(S2.m,c)<=dist(S2.m,S2.n)+dist(S2.n,c) by METRIC_1:4;
hence thesis by A43,AXIOMS:22;
end;
hence thesis;
end;
canceled;
theorem
N is Reflexive triangle & TopSpaceMetr(N) is compact implies
N is totally_bounded
proof
assume A1: N is Reflexive;
assume A2: N is triangle;
set TM = TopSpaceMetr(N);
A3: TM = TopStruct (# the carrier of N,Family_open_set(N) #)
by PCOMPS_1:def 6;
assume
A4: TopSpaceMetr(N) is compact;
let r such that A5: r>0;
defpred X[Subset of N] means
ex x being Element of N st $1 = Ball(x,r);
consider G being Subset-Family of N such that
A6: for C holds C in G iff X[C] from SubFamEx;
reconsider G as Subset-Family of TopSpaceMetr(N) by A3;
for C being Subset of TopSpaceMetr(N) st C in G holds C is open
proof
let C be Subset of TopSpaceMetr(N) such that A7: C in G;
reconsider C as Subset of N by A3;
ex x being Element of N
st C = Ball(x,r) by A6,A7;
then C in the topology of TM by A2,A3,PCOMPS_1:33;
hence thesis by PRE_TOPC:def 5;
end;
then A8: G is open by TOPS_2:def 1;
G is_a_cover_of TM
proof
A9: for x being Element of TM holds x in union G
proof
let x be Element of TM;
reconsider x as Element of N by A3;
dist(x,x)=0 by A1,METRIC_1:1;
then A10: x in Ball(x,r) by A5,METRIC_1:12;
Ball(x,r) in G by A6;
hence thesis by A10,TARSKI:def 4;
end;
[#](TM) = the carrier of TM by PRE_TOPC:def 3
.= union G by A9,SUBSET_1:49;
hence thesis by PRE_TOPC:def 8;
end;
then consider H being Subset-Family of TM such that
A11: H c= G & H is_a_cover_of TM & H is finite by A4,A8,COMPTS_1:def 3;
reconsider H as Subset-Family of N by A3;
take H;
union H = [#] TM by A11,PRE_TOPC:def 8
.= the carrier of TM by PRE_TOPC:def 3;
hence thesis by A3,A6,A11;
end;
definition let N;
canceled;
attr N is bounded means :Def8:
ex r st 0<r & for x,y being Point of N holds dist(x,y)<=r;
let C be Subset of N;
attr C is bounded means :Def9:
ex r st 0<r & for x,y being Point of N st
x in C & y in C holds dist(x,y)<=r;
end;
definition let A be non empty set;
cluster DiscreteSpace(A) -> bounded;
coherence
proof
set N = DiscreteSpace(A);
take 2;
thus 0<2;
A1: N = MetrStruct (#A,discrete_dist A#) by METRIC_1:def 12;
let x,y being Point of N;
A2: x = y or x <> y;
dist(x,y) = (the distance of N).(x,y) by METRIC_1:def 1;
then dist(x,y) = 0 or dist(x,y) = 1 by A1,A2,METRIC_1:def 11;
hence dist(x,y)<=2;
end;
end;
definition
cluster bounded (non empty MetrSpace);
existence
proof take DiscreteSpace{0}; thus thesis; end;
end;
canceled;
theorem
Th14: {}N is bounded
proof
take 1;
thus thesis;
end;
theorem Th15:
for C being Subset of N holds
( C <> {} & C is bounded implies
ex r,w st 0<r & w in C &
for z being Point of N st z in C holds dist(w,z)<=r ) &
(N is symmetric triangle &
(ex r,w st 0<r & w in C &
for z being Point of N st z in C holds dist(w,z)<=r)
implies C is bounded)
proof
let C be Subset of N;
thus C <> {} & C is bounded implies ex r,w st
0<r & w in C & for z being Point of N st z in C holds dist(w,z)<=r
proof
assume
A1: C <> {};
assume C is bounded;
then consider r such that
A2: 0<r & for x,y being Point of N st x in C & y in C
holds dist(x,y)<=r by Def9;
take r;
consider w being Element of C;
reconsider w as Point of N by A1,TARSKI:def 3;
take w;
thus 0<r by A2;
thus w in C by A1;
let z be Point of N;
assume z in C;
hence thesis by A2;
end;
assume A3: N is symmetric;
assume A4: N is triangle;
given r,w such that
A5: 0<r & w in C & for z being Point of N st z in C holds dist(w,z)<=r;
set s = r+r;
A6: s = 2*r by XCMPLX_1:11;
ex s st 0<s &
for x,y being Point of N st x in C & y in C holds dist(x,y)<=s
proof
take s;
thus 0<s by A5,A6,REAL_2:122;
let x,y be Point of N;
assume x in C & y in C;
then dist(w,x)<=r & dist(w,y)<=r by A5;
then dist(x,w)<=r & dist(w,y)<=r by A3,METRIC_1:3;
then A7: dist(x,w)+dist(w,y)<=s by REAL_1:55;
dist(x,y)<=dist(x,w)+dist(w,y) by A4,METRIC_1:4;
hence dist(x,y)<=s by A7,AXIOMS:22;
end;
hence thesis by Def9;
end;
theorem
Th16: N is Reflexive & 0<r implies w in Ball(w,r) & Ball(w,r) <> {}
proof
assume N is Reflexive;
then A1: dist(w,w) = 0 by METRIC_1:1;
assume 0<r;
hence thesis by A1,METRIC_1:12;
end;
theorem
Th17: r<=0 implies Ball(t1,r) = {}
proof
assume A1: r<=0;
assume A2: Ball(t1,r) <> {};
consider c being Element of Ball(t1,r);
reconsider c as Point of T by A2,TARSKI:def 3;
dist(t1,c)<r by A2,METRIC_1:12;
hence contradiction by A1,METRIC_1:5;
end;
Lm2: 0<r implies Ball(t1,r) is bounded
proof
assume A1: 0<r;
set P = Ball(t1,r);
ex r,t1 st
0<r & t1 in P & for z being Point of T st z in P holds dist(t1,z)<=r
proof
take r,t1;
thus 0<r by A1;
thus t1 in P by A1,Th16;
let z be Point of T;
assume z in P;
hence dist(t1,z)<=r by METRIC_1:12;
end;
hence thesis by Th15;
end;
canceled;
theorem
Th19: Ball(t1,r) is bounded
proof
now per cases;
suppose r<=0;
then Ball(t1,r) = {}T by Th17;
hence Ball(t1,r) is bounded by Th14;
suppose 0<r;
hence Ball(t1,r) is bounded by Lm2;
end;
hence thesis;
end;
theorem
Th20: for P, Q being Subset of T holds
P is bounded & Q is bounded implies P \/ Q is bounded
proof
let P, Q be Subset of T;
assume A1: P is bounded & Q is bounded;
per cases;
suppose P = {};
hence thesis by A1;
suppose A2: P <> {};
now per cases;
suppose Q = {};
hence P \/ Q is bounded by A1;
suppose A3:Q <> {};
consider r,t1 such that
A4: 0<r & t1 in P & for z being Point of T st z in P holds dist(t1,z)<=r
by A1,A2,Th15;
consider s be Real, d be Element of T such that
A5: 0<s & d in Q & for z being Point of T st z in Q holds dist(d,z)<=s
by A1,A3,Th15;
set t = r+s+dist(t1,d);
A6: t = r+(dist(t1,d)+s) by XCMPLX_1:1;
A7: dist(t1,d)<dist(t1,d)+s by A5,REAL_1:69;
0<=dist(t1,d) by METRIC_1:5;
then A8: r<r+(dist(t1,d)+s) by A7,REAL_1:69;
ex t being Real,t1 st
0<t & t1 in P \/ Q &
for z being Point of T st z in P \/ Q holds dist(t1,z)<=t
proof
take t,t1;
thus 0<t by A4,A6,A8,AXIOMS:22;
thus t1 in P \/ Q by A4,XBOOLE_0:def 2;
let z be Point of T; assume z in P \/ Q;
then A9: z in P or z in Q by XBOOLE_0:def 2;
now per cases by A4,A5,A9;
suppose dist(t1,z)<=r;
hence dist(t1,z)<=t by A6,A8,AXIOMS:22;
suppose A10: dist(d,z)<=s;
A11: dist(t1,z)<=dist(t1,d)+dist(d,z) by METRIC_1:4;
dist(t1,d)+dist(d,z)<=dist(t1,d)+s by A10,REAL_1:55;
then A12: dist(t1,z)<=dist(t1,d)+s by A11,AXIOMS:22;
dist(t1,d)+s<=r+(dist(t1,d)+s) by A4,REAL_1:69;
hence dist(t1,z)<=t by A6,A12,AXIOMS:22;
end;
hence thesis;
end;
hence thesis by Th15;
end;
hence thesis;
end;
theorem
Th21: for C, D being Subset of N holds
C is bounded & D c= C implies D is bounded
proof
let C, D be Subset of N;
assume A1: C is bounded & D c= C;
then consider r such that
A2: 0<r & for x,y being Point of N st x in C & y in C holds dist(x,y)<=r
by Def9;
ex r st 0<r &
for x,y being Point of N st x in D & y in D holds dist(x,y)<=r
proof
take r;
thus 0<r by A2;
let x,y be Point of N; assume
x in D & y in D; hence thesis by A1,A2;
end;
hence D is bounded by Def9;
end;
theorem
Th22: for P being Subset of T holds P = {t1} implies P is bounded
proof
let P be Subset of T;
assume A1: P = {t1}; t1 in Ball(t1,1) by Th16;
then A2:{t1} is Subset of Ball(t1,1) by SUBSET_1:63;
Ball(t1,1) is bounded by Th19;
hence thesis by A1,A2,Th21;
end;
theorem Th23: for P being Subset of T holds P is finite implies P is bounded
proof
let P be Subset of T;
assume A1: P is finite;
defpred P[set] means
ex X being Subset of T st X = $1 & X is bounded;
A2: P[{}]
proof
{}T is bounded by Th14;
hence thesis;
end;
A3: for x,B being set st x in P & B c= P & P[B] holds P[B \/ {x}]
proof
let x,B be set such that
A4: x in P and
B c= P and
A5: P[B];
consider X being Subset of T such that
A6: X = B and
A7: X is bounded by A5;
reconsider x as Element of T by A4;
reconsider W = {x} as Subset of T;
A8: W is bounded by Th22;
ex Y being Subset of T st Y = B \/ {x} & Y is bounded
proof
take X \/ W;
thus thesis by A6,A7,A8,Th20;
end;
hence thesis;
end;
P[P] from Finite(A1,A2,A3);
hence thesis;
end;
definition let T;
cluster finite -> bounded Subset of T;
coherence by Th23;
end;
definition let T;
cluster finite non empty Subset of T;
existence
proof
consider X being finite non empty Subset of T;
reconsider X as Subset of T;
take X;
thus thesis;
end;
end;
theorem Th24:
Y is finite & (for P being Subset of T st P in Y holds P is bounded) implies
union Y is bounded
proof
assume that
A1: Y is finite and
A2: for P being Subset of T st P in Y holds P is bounded;
defpred P[set] means
ex X being Subset of T st X = union $1 & X is bounded;
A3: P[{}]
proof
set m = {}T;
m = union {} & m is bounded by ZFMISC_1:2;
hence thesis;
end;
A4: for x,B being set st x in Y & B c= Y & P[B] holds P[B \/ {x}]
proof
let x,B be set such that
A5: x in Y and
B c= Y and
A6: P[B];
consider X being Subset of T such that
A7: X = union B and
A8: X is bounded by A6;
reconsider x as Subset of T by A5;
A9: union (B \/ {x}) = union B \/ union {x} by ZFMISC_1:96
.= union B \/ x by ZFMISC_1:31;
A10: x is bounded by A2,A5;
ex Y being Subset of T st Y = union (B \/ {x}) & Y is bounded
proof
take X \/ x;
thus thesis by A7,A8,A9,A10,Th20;
end;
hence thesis;
end;
P[Y] from Finite(A1,A3,A4);
hence thesis;
end;
theorem
Th25: N is bounded iff [#]N is bounded
proof
thus N is bounded implies [#]N is bounded
proof
assume N is bounded; then consider r such that
A1: 0<r & for x,y being Point of N holds dist(x,y)<=r by Def8;
0<r & for x,y being Point of N st x in [#]N & y in [#]N holds dist(x,y)<=
r
by A1;
hence thesis by Def9;
end;
assume [#]N is bounded; then consider r such that
A2: 0<r & for x,y being Point of N st
x in [#]N & y in [#]N holds dist(x,y)<=r by Def9;
take r;
thus 0<r by A2;
let x,y be Point of N;
x in the carrier of N;
then A3: x in [#]N by PRE_TOPC:12;
y in the carrier of N;
then y in [#]N by PRE_TOPC:12;
hence thesis by A2,A3;
end;
definition let N be bounded (non empty MetrStruct);
cluster [#]N -> bounded;
coherence by Th25;
end;
theorem T is totally_bounded implies T is bounded
proof
assume T is totally_bounded; then consider Y such that
A1: Y is finite and
A2: the carrier of T = union Y and
A3: for P st P in Y ex x being Element of T st P = Ball(x,1)
by Def1;
the carrier of T c= the carrier of T;
then reconsider B = the carrier of T as Subset of T;
for P being Subset of T st P in Y holds P is bounded
proof
thus for P being Subset of T st P in Y holds P is bounded
proof
let P be Subset of T; assume P in Y;
then ex x being Element of T st P = Ball(x,1) by A3;
hence P is bounded by Th19;
end;
end;
then B is bounded by A1,A2,Th24;
then [#]T is bounded by PRE_TOPC:12;
hence thesis by Th25;
end;
definition let N be Reflexive (non empty MetrStruct),
C be Subset of N;
assume A1: C is bounded;
func diameter C -> Real means :Def10:
(for x,y being Point of N st x in C & y in C holds dist(x,y)<=it) &
for s st (for x,y being Point of N st x in C & y in C holds dist(x,y)<=s) holds
it<=s if C <> {}
otherwise it = 0;
consistency;
existence
proof
thus C <> {} implies ex r being Real st
(for x,y being Point of N st x in C & y in C holds dist(x,y)<=r) &
for s st for x,y being Point of N st x in C & y in C holds dist(x,y)<=s
holds r<=s
proof assume
A2: C <> {};
defpred X[Real] means for x,y being Point of N st x in C & y in C holds
dist(x,y)<=$1;
set I = { r : X[r] };
defpred X[set] means
ex x,y being Point of N st x in C & y in C & $1 = dist(x,y);
set J = { r : X[r] };
consider r such that 0<r and
A3: for x,y being Point of N st x in C & y in C holds
dist(x,y)<=r by A1,Def9;
A4: r in I by A3;
consider c being Element of C;
reconsider c as Point of N by A2,TARSKI:def 3;
dist(c,c) = 0 by METRIC_1:1; then A5: 0 in J by A2;
A6: for a,b being real number st a in J & b in I holds a<=b
proof
let a,b be real number such that A7: a in J and A8: b in I;
consider t being Real such that
A9: t = a and
A10: ex x,y being Point of N st x in C & y in C & t = dist(x,y) by A7;
ex t' being Real st t'=b &
for x,y being Point of N st x in C & y in C holds dist(x,y)<=t' by A8;
hence thesis by A9,A10;
end;
I is Subset of REAL from SubsetD; then reconsider I as Subset of REAL;
J is Subset of REAL from SubsetD; then reconsider J as Subset of REAL;
consider d being real number such that
A11: for a being real number st a in J holds a<=d and
A12: for b being real number st b in I holds d<=b by A4,A5,A6,REAL_2:204;
take d;
thus d is Real by XREAL_0:def 1;
thus for x,y being Point of N st x in C & y in C holds dist(x,y)<=d
proof
let x,y be Point of N;
assume x in C & y in C; then dist(x,y) in J; hence dist(x,y)<=d by A11;
end;
let s;
assume for x,y being Point of N st x in C & y in C holds dist(x,y)<=s;
then s in I; hence thesis by A12;
end;
thus thesis;
end;
uniqueness
proof
let r1,r2 be Real;
hereby assume C <> {};
assume that
A13: for x,y being Point of N st x in C & y in C holds dist(x,y)<=r1 and
A14: for s st for x,y being Point of N st x in C & y in C holds dist(x,y)<= s
holds r1<=s and
A15: for x,y being Point of N st x in C & y in C holds dist(x,y)<=r2 and
A16: for s st for x,y being Point of N st x in C & y in C holds dist(x,y)<= s
holds r2<=s;
A17: r1 <= r2 by A14,A15;
r2 <= r1 by A13,A16;
hence r1 = r2 by A17,AXIOMS:21;
end;
thus thesis;
end;
end;
canceled;
theorem
for P being Subset of T holds P = {x} implies diameter P = 0
proof
let P be Subset of T;
assume A1: P = {x};
then A2: x in P by TARSKI:def 1;
then reconsider t1 = x as Element of T;
A3: P = {t1} by A1;
(for x,y being Point of T st x in P & y in P holds dist(x,y)<=0) &
(for s st
(for x,y being Point of T st x in P & y in P holds dist(x,y)<=s)
holds 0<=s)
proof
thus for x,y being Point of T st x in P & y in P holds dist(x,y)<=0
proof
let x,y be Point of T such that
A4: x in P and
A5: y in P;
x = t1 by A1,A4,TARSKI:def 1;
then dist(x,y) = dist(t1,t1) by A1,A5,TARSKI:def 1
.= 0 by METRIC_1:1;
hence thesis;
end;
let s;
assume for x,y being Point of T st x in P & y in P holds dist(x,y)<=s;
then dist(t1,t1)<=s by A2;
hence thesis by METRIC_1:1;
end;
hence thesis by A3,Def10;
end;
theorem Th29:
for S being Subset of R st S is bounded holds 0 <= diameter S
proof
let S be Subset of R;
assume A1: S is bounded;
per cases;
suppose S = {};
hence thesis by A1,Def10;
suppose
A2: S <> {};
consider x being Element of S;
reconsider x as Element of R by A2,TARSKI:def 3;
dist(x,x)<=diameter S by A1,A2,Def10;
hence thesis by METRIC_1:1;
end;
theorem
for A being Subset of M holds A <> {} & A is bounded & diameter A = 0 implies
ex g being Point of M st A = {g}
proof
let A be Subset of M;
assume A1: A <> {} & A is bounded;
thus diameter A = 0 implies ex g being Point of M st A = {g}
proof
assume A2: diameter A = 0;
consider g being Element of A;
reconsider g as Element of M by A1,TARSKI:def 3;
take g;
reconsider Z = {g} as Subset of M;
for x being Element of M holds x in A iff x in Z
proof
let x be Element of M;
thus x in A implies x in Z
proof
assume x in A;
then dist(x,g)<=0 by A1,A2,Def10;
then dist(x,g) = 0 by METRIC_1:5;
then x = g by METRIC_1:2;
hence thesis by TARSKI:def 1;
end;
A3: g in A by A1;
assume x in Z;
hence thesis by A3,TARSKI:def 1;
end;
hence thesis by SUBSET_1:8;
end;
end;
theorem 0<r implies diameter Ball(t1,r) <= 2*r
proof
assume 0<r;
then A1: t1 in Ball(t1,r) & Ball(t1,r) <> {} by Th16;
A2: Ball(t1,r) is bounded by Th19;
for x,y being Point of T st x in Ball(t1,r) & y in Ball(t1,r) holds
dist(x,y)<= 2*r
proof
let x,y be Point of T; assume
x in Ball(t1,r) & y in Ball(t1,r);
then dist(t1,x)<r & dist(t1,y)<r by METRIC_1:12;
then dist(t1,x)+dist(t1,y)<r+r by REAL_1:67;
then A3: dist(x,t1)+dist(t1,y)<2*r by XCMPLX_1:11;
dist(x,y)<=dist(x,t1)+dist(t1,y) by METRIC_1:4;
hence thesis by A3,AXIOMS:22;
end;
hence thesis by A1,A2,Def10;
end;
theorem
for S, V being Subset of R holds
S is bounded & V c= S implies diameter V <= diameter S
proof
let S, V be Subset of R;
assume that
A1: S is bounded and
A2: V c= S;
A3: V is bounded by A1,A2,Th21;
per cases;
suppose
V = {};
then diameter V = 0 by A3,Def10;
hence thesis by A1,Th29;
suppose
A4: V <> {};
for x,y being Point of R st x in V & y in V holds dist(x,y)<=(diameter S)
by A1,A2,Def10;
hence thesis by A3,A4,Def10;
end;
theorem
for P, Q being Subset of T holds
P is bounded & Q is bounded & P meets Q implies
diameter (P \/ Q) <= diameter P + diameter Q
proof
let P, Q be Subset of T;
assume that
A1: P is bounded and
A2: Q is bounded and
A3: P /\ Q <> {};
A4: P <> {} & Q <> {} by A3;
A5: P \/ Q is bounded by A1,A2,Th20;
P c= P \/ Q by XBOOLE_1:7;
then A6: P \/ Q <> {} by A4,XBOOLE_1:3;
set a = diameter P;
A7: 0<=a by A1,Th29;
set b = diameter Q;
A8: 0<=b by A2,Th29;
consider g being Element of P /\ Q;
A9: g in P & g in Q by A3,XBOOLE_0:def 3;
reconsider g as Element of T by A3,TARSKI:def 3;
set s = diameter P + diameter Q;
A10: a<=s by A8,REAL_2:173;
A11: b<=s by A7,REAL_2:173;
for x,y being Point of T st x in P \/ Q & y in P \/ Q holds dist(x,y)<=s
proof
let x,y be Point of T such that A12: x in P \/ Q & y in P \/ Q;
A13: dist(x,y)<=dist(x,g)+dist(g,y) by METRIC_1:4;
now per cases by A12,XBOOLE_0:def 2;
suppose A14: x in P;
now per cases by A12,XBOOLE_0:def 2;
suppose y in P; then dist(x,y)<=a by A1,A14,Def10;
hence dist(x,y)<=s by A10,AXIOMS:22;
suppose y in Q; then A15: dist(g,y)<=b by A2,A9,Def10;
dist(x,g)<=a by A1,A9,A14,Def10;
then dist(x,g)+dist(g,y)<=a+b by A15,REAL_1:55;
hence dist(x,y)<=s by A13,AXIOMS:22;
end;
hence dist(x,y)<=s;
suppose A16: x in Q;
now per cases by A12,XBOOLE_0:def 2;
suppose y in P; then A17: dist(g,y)<=a by A1,A9,Def10;
dist(x,g)<=b by A2,A9,A16,Def10;
then dist(x,g)+dist(g,y)<=b+a by A17,REAL_1:55;
hence dist(x,y)<=s by A13,AXIOMS:22;
suppose y in Q; then dist(x,y)<=b by A2,A16,Def10;
hence dist(x,y)<=s by A11,AXIOMS:22;
end;
hence dist(x,y)<=s;
end;
hence thesis;
end;
hence thesis by A5,A6,Def10;
end;
definition let N,S2;
redefine func rng S2 -> Subset of N;
coherence by Def2;
end;
theorem
for S1 being sequence of T holds S1 is Cauchy implies rng S1 is bounded
proof
let S1 be sequence of T;
assume A1: S1 is Cauchy;
set A = rng S1; consider p such that
A2: for n,m st p<=n & p<=m holds dist(S1.n,S1.m)<1
by A1,Def5;
defpred X[set] means ex n st p<=n & $1 = S1.n;
reconsider B = {t1 where t1 is Point of T : X[t1] }
as Subset of T from SubsetD;
defpred X[set] means ex n st n<=p & $1 = S1.n;
reconsider C = {t1 where t1 is Point of T : X[t1] }
as Subset of T from SubsetD;
reconsider B, C as Subset of T;
C is finite
proof
set K = Seg p; set J = {0} \/ K;
C = S1.:J
proof
now
let x;
thus x in C implies x in S1.:J
proof
assume x in C;
then consider t1 such that A3: x = t1 & ex n st n<=p & t1 = S1.n;
consider n such that A4: n<=p & t1 = S1.n by A3;
n in NAT;
then A5: n in dom S1 by Def2;
now per cases by NAT_1:22;
suppose n=0; then n in {0} by TARSKI:def 1;
then n in J by XBOOLE_0:def 2;
hence x in S1.:J by A3,A4,A5,FUNCT_1:def 12;
suppose ex m st n=m+1; then consider m such that A6: n=m+1;
1<=n by A6,NAT_1:29;
then n in { k : 1<=k & k<=p } by A4;
then n in K by FINSEQ_1:def 1;
then n in J by XBOOLE_0:def 2;
hence x in S1.:J by A3,A4,A5,FUNCT_1:def 12;
end;
hence x in S1.:J;
end;
assume x in S1.:J;
then consider y such that
A7: y in dom S1 & y in J & x=S1.y by FUNCT_1:def 12;
reconsider y as Nat by A7;
now per cases by A7,XBOOLE_0:def 2;
suppose y in {0}; then y=0 by TARSKI:def 1; then A8: y<=p by NAT_1:18;
S1.y is Element of T;
then reconsider x'=x as Element of T by A7;
ex n st n<=p & x'=S1.n by A7,A8;
hence x in C;
suppose y in K;
then y in {k : 1<=k & k<=p } by FINSEQ_1:def 1;
then A9: ex k st y = k & 1<=k & k<=p;
S1.y is Element of T;
then reconsider x'=x as Element of T by A7;
ex n st n<=p & x'=S1.n by A7,A9;
hence x in C;
end;
hence x in C;
end;
hence thesis by TARSKI:2;
end;
hence thesis;
end;
then A10: C is bounded by Th23;
A11: B is bounded
proof
set x=S1.p;
ex r,t1 st
0<r & t1 in B & for z being Point of T st z in B holds dist(t1,z)<=r
proof
take 1,x;
thus 0<1;
thus x in B;
let z be Point of T;
assume z in B; then consider
t1 such that A12: z = t1 & ex n st p<=n & t1 = S1.n;
thus thesis by A2,A12;
end;
hence thesis by Th15;
end;
A = B \/ C
proof
thus A c= B \/ C
proof
let x;
assume x in A;
then consider y such that
A13: y in dom S1 & x = S1.y by FUNCT_1:def 5;
reconsider y as Nat by A13,Def2;
S1.y is Element of T;
then reconsider x'=x as Element of T by A13;
now per cases;
suppose y<=p;
then ex n st n<=p & x'= S1.n by A13; then x in C;
hence x in B \/ C by XBOOLE_0:def 2;
suppose p<=y;
then ex n st p<=n & x'= S1.n by A13; then x in B;
hence x in B \/ C by XBOOLE_0:def 2;
end;
hence x in B \/ C;
end;
let x;
assume A14: x in B \/ C;
now per cases by A14,XBOOLE_0:def 2;
suppose x in B; then consider
t1 such that A15: x = t1 & ex n st p<=n & t1 = S1.n;
consider n such that A16: p<=n & t1 = S1.n by A15;
n in NAT; then n in dom S1 by Def2;
hence x in A by A15,A16,FUNCT_1:def 5;
suppose x in C; then consider
t1 such that A17: x = t1 & ex n st n<=p & t1 = S1.n;
consider n such that A18: n<=p & t1 = S1.n by A17;
n in NAT; then n in dom S1 by Def2;
hence x in A by A17,A18,FUNCT_1:def 5;
end;
hence x in A;
end;
hence thesis by A10,A11,Th20;
end;