:: Totally Bounded Metric Spaces
:: by Alicia de la Cruz
::
:: Received September 30, 1991
:: Copyright (c) 1991-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 NUMBERS, XBOOLE_0, METRIC_1, SUBSET_1, SETFAM_1, RELAT_2,
FUNCT_1, REAL_1, CARD_1, ARYTM_3, XXREAL_0, POWER, RELAT_1, SEQ_1, SEQ_2,
ORDINAL2, COMPLEX1, ARYTM_1, FINSET_1, STRUCT_0, TARSKI, NAT_1, BHSP_3,
REWRITE1, ALI2, PRE_TOPC, PCOMPS_1, RCOMP_1, ZFMISC_1, ORDINAL1,
XXREAL_2, MEASURE5, FINSEQ_1, TBSP_1, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
COMPLEX1, REAL_1, RELAT_1, FUNCT_1, RELSET_1, FINSEQ_1, DOMAIN_1,
SETFAM_1, FUNCT_2, BINOP_1, FINSET_1, NAT_1, STRUCT_0, PRE_TOPC, TOPS_2,
SEQ_1, SEQ_2, COMPTS_1, METRIC_1, POWER, PCOMPS_1, ALI2, XXREAL_0;
constructors SETFAM_1, DOMAIN_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1, FINSEQ_1,
SEQ_2, POWER, TOPS_2, COMPTS_1, PCOMPS_1, ALI2, VALUED_1, RELSET_1,
COMSEQ_2, BINOP_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NUMBERS,
XREAL_0, NAT_1, MEMBERED, FINSEQ_1, STRUCT_0, METRIC_1, PCOMPS_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, ORDINAL1, XBOOLE_0, FINSET_1;
equalities STRUCT_0;
expansions TARSKI, XBOOLE_0;
theorems METRIC_1, SUBSET_1, FUNCT_1, PCOMPS_1, PRE_TOPC, MEMBERED, TOPS_2,
TARSKI, COMPTS_1, NAT_1, SEQ_2, ZFMISC_1, POWER, SERIES_1, ABSVALUE,
FUNCT_2, SETFAM_1, FINSEQ_1, ALI2, RELSET_1, XREAL_0, XBOOLE_0, XBOOLE_1,
XCMPLX_1, FINSET_1, XREAL_1, XXREAL_0, ORDINAL1, RELAT_1;
schemes DOMAIN_1, SUBSET_1, NAT_1, SEQ_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;
per cases by A2,XXREAL_0:1;
suppose n<m;
hence thesis by A1,POWER:40;
end;
suppose n=m;
hence thesis;
end;
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 that
A1: 0<L and
A2: L<1;
defpred X[Nat] means L to_power $1 <= 1 & 0 < L to_power $1;
A3: for k st X[k] holds X[k+1]
proof
let k be Nat such that
A4: L to_power k <= 1 and
A5: 0 < L to_power k;
A6: L to_power (k+1) = L to_power k*L to_power 1 by A1,POWER:27
.= L to_power k*L by POWER:25;
L to_power k*L<=L to_power k by A2,A5,XREAL_1:153;
hence thesis by A1,A4,A5,A6,XREAL_1:129,XXREAL_0:2;
end;
A7: X[0] by POWER:24;
thus for k holds X[k] from NAT_1:sch 2(A7,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;
let s;
deffunc U(Nat) = L to_power ($1+1);
consider rseq being Real_Sequence such that
A2: for n being Nat holds rseq.n = U(n) from SEQ_1:sch 1;
assume
A3: 0<s;
rseq is convergent & lim rseq = 0 by A1,A2,SERIES_1:1;
then consider n being Nat such that
A4: for m being Nat st n<=m holds |.rseq.m-0.|<s by A3,SEQ_2:def 7;
take n+1;
A5: 0<L to_power (n+1) by A1,Th2;
|.rseq.n-0.| = |.L to_power (n+1).| by A2
.= L to_power (n+1) by A5,ABSVALUE:def 1;
hence thesis by A4;
end;
definition
let N;
attr N is totally_bounded means
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;
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 FUNCT_2:def 1;
let x;
assume x in NAT;
then x in dom f by A1,FUNCT_2:def 1;
then
A2: f.x in rng f by FUNCT_1:def 3;
rng f c= the carrier of N by A1,RELAT_1:def 19;
hence thesis 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 be object;
assume y in rng f;
then consider x being object such that
A5: x in dom f and
A6: y=f.x by FUNCT_1:def 3;
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;
hence thesis by A3,FUNCT_2:def 1,RELSET_1:4;
end;
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,ORDINAL1:def 12;
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
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;
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;
set a=dist(g1,g2)/4;
A5: dist(g1,g2)>=0 by METRIC_1:5;
A6: dist(g1,g2)<>0 by A4,METRIC_1:2;
then consider n1 such that
A7: for m st n1<=m holds dist(S1.m,g1)<a by A2,A5,XREAL_1:224;
consider n2 such that
A8: for m st n2<=m holds dist(S1.m,g2)<a by A3,A6,A5,XREAL_1:224;
set k=n1+n2;
A9: dist(S1.k,g2)<a by A8,NAT_1:12;
A10: dist(g1,g2)<=dist(g1,S1.k)+dist(S1.k,g2) by METRIC_1:4;
dist(S1.k,g1)<a by A7,NAT_1:12;
then dist(g1,S1.k)+dist(S1.k,g2)<a+a by A9,XREAL_1:8;
then dist(g1,g2)<dist(g1,g2)/2 by A10,XXREAL_0:2;
hence contradiction by A6,A5,XREAL_1:216;
end;
end;
definition
let N,S2;
attr S2 is Cauchy means
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
for S2 st S2 is Cauchy holds S2 is convergent;
end;
theorem Th5:
N is triangle symmetric & S2 is convergent implies S2 is Cauchy
proof
assume that
A1: N is triangle and
A2: N is symmetric;
reconsider N as symmetric non empty MetrStruct by A2;
assume
A3: S2 is convergent;
reconsider S2 as sequence of N;
consider g being Element of N such that
A4: for r st 0<r ex n st for m st n<=m holds dist(S2.m,g)<r by A3;
let r;
assume 0<r;
then consider n such that
A5: for m st n<=m holds dist(S2.m,g)<r/2 by A4,XREAL_1:215;
take n;
let m,m9 be Nat;
assume that
A6: m>=n and
A7: m9>=n;
A8: dist(S2.m9,g)<r/2 by A5,A7;
dist(S2.m,g)<r/2 by A5,A6;
then
A9: dist(S2.m,g)+dist(g,S2.m9)<r/2+r/2 by A8,XREAL_1:8;
dist(S2.m,S2.m9)<=dist(S2.m,g)+dist(g,S2.m9) by A1,METRIC_1:4;
hence thesis by A9,XXREAL_0:2;
end;
registration
let M be triangle symmetric non empty MetrStruct;
cluster convergent -> Cauchy for sequence of M;
coherence by Th5;
end;
theorem Th6:
for N being symmetric non empty MetrStruct, S2 being sequence of N
holds 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 let N be symmetric non empty MetrStruct, S2 be sequence of N;
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
A1: S2 is Cauchy;
let r;
assume 0<r;
then consider p such that
A2: for n,m st p<=n & p<=m holds dist(S2.n,S2.m)<r by A1;
take p;
let n,k be Nat such that
A3: p<=n;
n<=n+k by NAT_1:11;
then p<=n+k by A3,XXREAL_0:2;
hence thesis by A2,A3;
end;
assume
A4: 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
A5: for n,k st p<=n holds dist(S2.(n+k),S2.n)<r by A4;
take p;
let n,m such that
A6: p<=n and
A7: p<=m;
per cases;
suppose
n<=m;
then consider k be Nat such that
A8: m=n+k by NAT_1:10;
reconsider m9=m,n9=n,k as Nat;
m = n+k by A8;
then dist(S2.m9,S2.n9)<r by A5,A6;
hence thesis;
end;
suppose
m<=n;
then consider k be Nat such that
A9: n=m+k by NAT_1:10;
reconsider k as Nat;
n = m+k by A9;
hence thesis by A5,A7;
end;
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 and
A2: L<1 and
A3: for x,y being Point of M holds dist(f.x,f.y)<=L*dist(x,y) by ALI2:def 1;
A4: 1-L>0 by A2,XREAL_1:50;
ex S1 st for n holds S1.(n+1)=f.(S1.n)
proof
set z = the Element of M;
deffunc U(Nat,Element of M) = f.$2;
ex h being sequence of the carrier of M st h.0 = z & for n being
Nat holds h.(n+1) = U(n,h.n) from NAT_1:sch 12;
then consider h being sequence of the carrier of M such that
h.0 = z and
A5: for n being Nat holds h.(n + 1) = f.(h.n);
take h;
let n;
thus thesis by A5;
end;
then consider S1 such that
A6: for n holds S1.(n+1)=f.(S1.n);
set r = dist(S1.1,S1.0);
A7: 0<=r by METRIC_1:5;
A8: 1-L<>0 by A2;
assume
A9: M is complete;
now
per cases;
suppose
A10: 0=r;
A11: f.(S1.0) = S1.(0+1) by A6
.= S1.0 by A10,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
A12: f.y=y;
A13: dist(y,S1.0)>=0 by METRIC_1:5;
assume y<>S1.0;
then dist(y,S1.0)<>0 by METRIC_1:2;
then L*dist(y,S1.0)<dist(y,S1.0) by A2,A13,XREAL_1:157;
hence contradiction by A3,A11,A12;
end;
hence thesis by A11;
end;
suppose
A14: 0<>r;
A15: 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;
A16: for k st X[k] holds X[k+1]
proof
let k be Nat;
assume dist(S1.(k+1),S1.k)<=r*L to_power k;
then
A17: L*dist(S1.(k+1),S1.k)<=L*(r*L to_power k) by A1,XREAL_1:64;
dist(S1.((k+1)+1),S1.(k+1)) = dist(f.(S1.(k+1)),S1.(k+1)) by A6
.= dist(f.(S1.(k+1)),f.(S1.k)) by A6;
then
A18: dist(S1.((k+1)+1),S1.(k+1)) <= L*dist(S1.(k+1),S1.k) by A3;
L*(r*L to_power k) = r*(L*L to_power k)
.= r*(L to_power k*L to_power 1) by POWER:25
.= r*L to_power (k+1) by A1,POWER:27;
hence thesis by A18,A17,XXREAL_0:2;
end;
dist(S1.(0+1),S1.0) = r*1 .= r*L to_power 0 by POWER:24;
then
A19: X[0];
thus for k holds X[k] from NAT_1:sch 2(A19,A16);
end;
A20: 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));
A21: for k st X[k] holds X[k+1]
proof
let k be Nat such that
A22: dist(S1.k,S1.0)<=r*((1-L to_power k)/(1-L));
dist(S1.(k+1),S1.k)<=r*L to_power k by A15;
then
A23: dist(S1.(k+1),S1.0) <= dist(S1.(k+1),S1.k) + dist(S1.k,S1.0) &
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 A22,METRIC_1:4,XREAL_1:7;
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))
.= r*(L to_power k/(1-L)*(1-L) + (1-L to_power k)/(1-L)) by A8,
XCMPLX_1:87
.= r*((1-L)*L to_power k/(1-L) + (1-L to_power k)/(1-L)) by
XCMPLX_1:74
.= r*((1*L to_power k-L*L to_power k + (1-L to_power k))/(1-L))
by XCMPLX_1:62
.= r*((1-L*L to_power k)/(1-L))
.= r*((1-L to_power k*L to_power 1)/(1-L)) by POWER:25
.= r*((1-L to_power (k+1))/(1-L)) by A1,POWER:27;
hence thesis by A23,XXREAL_0:2;
end;
r*((1-L to_power 0)/(1-L)) = r*((1-1)/(1-L)) by POWER:24
.= 0;
then
A24: X[0] by METRIC_1:1;
thus for k holds X[k] from NAT_1:sch 2(A24,A21);
end;
A25: for k holds dist(S1.k,S1.0)<=r/(1-L)
proof
let k be Nat;
0 < L to_power k by A1,A2,Th2;
then 1-L to_power k<=1 by XREAL_1:44;
then (1-L to_power k)/(1-L) <= 1/(1-L) by A4,XREAL_1:72;
then
A26: r*((1-L to_power k)/(1-L)) <= r*(1/(1-L)) by A7,XREAL_1:64;
dist(S1.k,S1.0)<=r*((1-L to_power k)/(1-L)) by A20;
then dist(S1.k,S1.0)<=r*(1/(1-L)) by A26,XXREAL_0:2;
hence thesis by XCMPLX_1:99;
end;
A27: 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);
A28: for n st X[n] holds X[n+1]
proof
let n such that
A29: for k holds dist(S1.(n+k),S1.n)<=L to_power n*dist(S1.k,S1. 0);
let k be Nat;
A30: L*(L to_power n*dist(S1.k,S1.0)) = L*L to_power n*dist(S1.k,S1. 0)
.= L to_power n*L to_power 1*dist(S1.k,S1.0) by POWER:25
.= L to_power (n+1)*dist(S1.k,S1.0) by A1,POWER:27;
dist(S1.((n+1)+k),S1.(n+1)) = dist(S1.((n+k)+1),S1.(n+1))
.= dist(f.(S1.(n+k)),S1.(n+1)) by A6
.= dist(f.(S1.(n+k)),f.(S1.n)) by A6;
then
A31: dist(S1.((n+1)+k),S1.(n+1))<=L*dist(S1.(n+k),S1.n) by A3;
L*dist(S1.(n+k),S1.n) <=L*(L to_power n*dist(S1.k,S1.0)) by A1,A29,
XREAL_1:64;
hence thesis by A31,A30,XXREAL_0:2;
end;
A32: X[0]
proof
let n;
L to_power 0*dist(S1.n,S1.0) = 1*dist(S1.n,S1.0) by POWER:24
.= dist(S1.n,S1.0);
hence thesis;
end;
thus for k holds X[k] from NAT_1:sch 2(A32,A28);
end;
A33: for n,k holds dist(S1.(n+k),S1.n)<=(r/(1-L))*L to_power n
proof
let n,k be Nat;
0 <= L to_power n by A1,A2,Th2;
then
A34: L
to_power n*dist(S1.k,S1.0) <= L to_power n*(r/(1-L)) by A25,XREAL_1:64;
dist(S1.(n+k),S1.n)<=L to_power n*dist(S1.k,S1.0) by A27;
hence thesis by A34,XXREAL_0:2;
end;
for s st s>0 ex p st for n,k st p<=n holds dist(S1.(n+k),S1.n)<s
proof
A35: (1-L)/r>0 by A4,A7,A14,XREAL_1:139;
let s;
assume s>0;
then (1-L)/r*s>0 by A35,XREAL_1:129;
then consider p such that
A36: L to_power p<(1-L)/r*s by A1,A2,Th3;
take p;
let n,k be Nat;
assume p<=n;
then L to_power n<=L to_power p by A1,A2,Th1;
then
A37: L to_power n<(1-L)/r*s by A36,XXREAL_0:2;
r/(1-L)>0 by A4,A7,A14,XREAL_1:139;
then
A38: (r/(1-L))*L to_power n<(r/(1-L))*((1-L)/r*s) by A37,XREAL_1:68;
A39: dist(S1.(n+k),S1.n)<=(r/(1-L))*L to_power n by A33;
(r/(1-L))*((1-L)/r*s) = ((r/(1-L))*((1-L)/r))*s
.= ((r*(1-L))/(r*(1-L)))*s by XCMPLX_1:76
.= 1*s by A8,A14,XCMPLX_1:6,60
.= s;
hence thesis by A38,A39,XXREAL_0:2;
end;
then S1 is Cauchy by Th6;
then S1 is convergent by A9;
then consider x being Element of M such that
A40: for r st r>0 ex n st for m st n<=m holds dist(S1.m,x)<r;
A41: f.x = x
proof
set a = dist(x,f.x)/4;
assume x <> f.x;
then
A42: dist(x,f.x) <> 0 by METRIC_1:2;
A43: dist(x,f.x) >= 0 by METRIC_1:5;
then consider n such that
A44: for m st n<=m holds dist(S1.m,x)<a by A40,A42,XREAL_1:224;
dist(S1.(n+1),f.x) = dist(f.(S1.n),f.x) by A6;
then
A45: dist(S1.(n+1),f.x) <= L*dist(S1.n,x) by A3;
A46: dist(S1.n,x)<a by A44;
L*dist(S1.n,x)<=dist(S1.n,x) by A2,METRIC_1:5,XREAL_1:153;
then dist(S1.(n+1),f.x)<= dist(S1.n,x) by A45,XXREAL_0:2;
then
A47: dist(S1.(n+1),f.x)<a by A46,XXREAL_0:2;
A48: dist(x,f.x)<=dist(x,S1.(n+1))+dist(S1.(n+1),f.x) & dist(x,f.x)/2
< dist(x,f. x) by A42,A43,METRIC_1:4,XREAL_1:216;
dist(x,S1.(n+1))<a by A44,NAT_1:11;
then dist(x,S1.(n+1))+dist(S1.(n+1),f.x)<a+a by A47,XREAL_1:8;
hence contradiction by A48,XXREAL_0:2;
end;
for y being Element of M st f.y=y holds y=x
proof
let y be Element of M;
assume
A49: f.y=y;
A50: dist(y,x)>=0 by METRIC_1:5;
assume y<>x;
then dist(y,x)<>0 by METRIC_1:2;
then L*dist(y,x)<dist(y,x) by A2,A50,XREAL_1:157;
hence contradiction by A3,A41,A49;
end;
hence thesis by A41;
end;
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 5;
assume
A2: TopSpaceMetr(T) is compact;
let S2 be sequence of T such that
A3: S2 is Cauchy;
S2 is convergent
proof
A4: 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[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
A5: for B being Subset of TopSpaceMetr(T) holds B in F iff X[B] from
SUBSET_1:sch 3;
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 DOMAIN_1:sch 7;
then
A7: B0 in F by A1,A5;
reconsider B0 as Subset of TopSpaceMetr(T) by A1,A6;
reconsider F as Subset-Family of TopSpaceMetr(T);
set G = clf F;
A8: Cl B0 in G by A7,PCOMPS_1:def 2;
A9: 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 that
A14: B in H and
A15: C in H;
reconsider B, C as Subset of TM by A13,A14,A15;
consider V being Subset of TM such that
A16: B = Cl V and
A17: V in F by A11,A14,PCOMPS_1:def 2;
consider p such that
A18: V = {x where x is Point of T : ex n st p<=n & x = S2.n} by A5,A17;
consider W being Subset of TM such that
A19: C = Cl W and
A20: W in F by A11,A15,PCOMPS_1:def 2;
consider q being Nat such that
A21: W = {x where x is Point of T : ex n st q<=n & x = S2.n} by A5,A20;
now
per cases;
case
A22: q<=p;
thus V c= W
proof
let y be object;
assume y in V;
then consider x being Point of T such that
A23: y = x and
A24: ex n st p<=n & x = S2.n by A18;
consider n such that
A25: p<=n and
A26: x = S2.n by A24;
q<=n by A22,A25,XXREAL_0:2;
hence thesis by A21,A23,A26;
end;
end;
case
A27: p<=q;
thus W c= V
proof
let y be object;
assume y in W;
then consider x being Point of T such that
A28: y = x and
A29: ex n st q<=n & x = S2.n by A21;
consider n such that
A30: q<=n and
A31: x = S2.n by A29;
p<=n by A27,A30,XXREAL_0:2;
hence thesis by A18,A28,A31;
end;
end;
end;
then B c= C or C c= B by A16,A19,PRE_TOPC:19;
hence thesis;
end;
then consider m being set such that
A32: m in H and
A33: for C being set st C in H holds m c= C by A10,A12,FINSET_1:11;
A34: m c= meet H by A10,A33,SETFAM_1:5;
reconsider m as Subset of TM by A13,A32;
consider A being Subset of TM such that
A35: m = Cl A and
A36: A in F by A11,A32,PCOMPS_1:def 2;
A <> {} by A5,A4,A36;
then m <> {} by A35,PRE_TOPC:18,XBOOLE_1:3;
hence thesis by A34;
end;
G is closed by PCOMPS_1:11;
then meet G <> {} by A2,A9,COMPTS_1:4;
then consider c being Point of TM such that
A37: c in meet G by SUBSET_1:4;
reconsider c as Point of T by A1;
take c;
let r;
assume 0<r;
then
A38: 0<r/2 by XREAL_1:215;
then consider p such that
A39: for n,m st p<=n & p<=m holds dist(S2.n,S2.m)<r/2 by A3;
dist(c,c)<r/2 by A38,METRIC_1:1;
then
A40: c in Ball(c,r/2) by METRIC_1:11;
reconsider Z = Ball(c,r/2) as Subset of TopSpaceMetr(T) by A1;
Ball(c,r/2) in Family_open_set(T) by PCOMPS_1:29;
then
A41: Z is open by A1,PRE_TOPC:def 2;
defpred X[set] means ex n st p<=n & $1 = S2.n;
set B = {x where x is Point of T : X[x]};
A42: B is Subset of T from DOMAIN_1:sch 7;
then
A43: B in F by A1,A5;
reconsider B as Subset of TopSpaceMetr(T) by A1,A42;
Cl B in G by A43,PCOMPS_1:def 2;
then c in Cl B by A37,SETFAM_1:def 1;
then B meets Z by A40,A41,PRE_TOPC:def 7;
then consider g being object such that
A44: g in B /\ Z by XBOOLE_0:4;
take p;
let m;
A45: g in B by A44,XBOOLE_0:def 4;
A46: g in Z by A44,XBOOLE_0:def 4;
then reconsider g as Point of T;
consider x being Point of T such that
A47: g = x and
A48: ex n st p<=n & x = S2.n by A45;
consider n such that
A49: p<=n and
A50: x = S2.n by A48;
assume p<=m;
then
A51: dist(S2.m,S2.n)<r/2 by A39,A49;
dist(S2.n,c)<r/2 by A46,A47,A50,METRIC_1:11;
then
A52: dist(S2.m,S2.n)+dist(S2.n,c)<r/2+r/2 by A51,XREAL_1:8;
dist(S2.m,c)<=dist(S2.m,S2.n)+dist(S2.n,c) by METRIC_1:4;
hence thesis by A52,XXREAL_0:2;
end;
hence thesis;
end;
theorem
N is Reflexive triangle & TopSpaceMetr(N) is compact implies N is
totally_bounded
proof
assume
A1: N is Reflexive;
set TM = TopSpaceMetr(N);
assume
A2: N is triangle;
assume
A3: TopSpaceMetr(N) is compact;
let r such that
A4: 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
A5: for C holds C in G iff X[C] from SUBSET_1:sch 3;
A6: TM = TopStruct (# the carrier of N,Family_open_set(N) #) by PCOMPS_1:def 5;
then reconsider G as Subset-Family of TopSpaceMetr(N);
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 A6;
dist(x,x)=0 by A1,METRIC_1:1;
then
A7: x in Ball(x,r) by A4,METRIC_1:11;
Ball(x,r) in G by A5;
hence thesis by A7,TARSKI:def 4;
end;
then [#](TM) = union G by SUBSET_1:28;
then
A8: G is Cover of TM by SETFAM_1:45;
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
A9: C in G;
reconsider C as Subset of N by A6;
ex x being Element of N st C = Ball(x,r) by A5,A9;
then C in the topology of TM by A2,A6,PCOMPS_1:29;
hence thesis by PRE_TOPC:def 2;
end;
then G is open by TOPS_2:def 1;
then consider H being Subset-Family of TM such that
A10: H c= G and
A11: H is Cover of TM and
A12: H is finite by A3,A8,COMPTS_1:def 1;
reconsider H as Subset-Family of N by A6;
take H;
union H = the carrier of TM by A11,SETFAM_1:45;
hence thesis by A6,A5,A10,A12;
end;
definition
let N be non empty MetrStruct;
attr N is bounded means
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
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;
registration
let A be non empty set;
cluster DiscreteSpace(A) -> bounded;
coherence
proof
take 2;
set N = DiscreteSpace(A);
thus 0<2;
let x,y being Point of N;
A1: N = MetrStruct (#A,discrete_dist A#) & dist(x,y) = (the distance of N)
.(x,y) by METRIC_1:def 1,def 11;
x = y or x <> y;
then dist(x,y) = 0 or dist(x,y) = 1 by A1,METRIC_1:def 10;
hence dist(x,y)<=2;
end;
end;
registration
cluster bounded for non empty MetrSpace;
existence
proof
take DiscreteSpace{0};
thus thesis;
end;
end;
registration
let N;
cluster empty -> bounded for Subset of N;
coherence
proof
let S be Subset of N;
assume
A1: S is empty;
take 1;
thus thesis by A1;
end;
end;
registration
let N;
cluster bounded for Subset of N;
existence
proof
take {}N;
thus thesis;
end;
end;
theorem Th10:
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 & 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
set w = the Element of C;
assume
A1: C <> {};
then reconsider w as Point of N by TARSKI:def 3;
assume C is bounded;
then consider r such that
A2: 0<r and
A3: for x,y being Point of N st x in C & y in C holds dist(x,y)<=r;
take r;
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 A3;
end;
assume
A4: N is symmetric;
assume
A5: N is triangle;
given r,w such that
A6: 0<r and
A7: for z being Point of N st z in C holds dist(w,z)<=r;
set s = r+r;
reconsider N as symmetric MetrStruct by A4;
reconsider w as Element of N;
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 A6;
let x,y be Point of N;
assume that
A8: x in C and
A9: y in C;
A10: dist(w,x)<=r by A7,A8;
dist(w,y)<=r by A7,A9;
then
A11: dist(x,w)+dist(w,y)<=s by A10,XREAL_1:7;
dist(x,y)<=dist(x,w)+dist(w,y) by A5,METRIC_1:4;
hence thesis by A11,XXREAL_0:2;
end;
hence thesis;
end;
theorem Th11:
for r being Real holds N is Reflexive & 0<r implies w in Ball(w,r)
proof
let r be Real;
assume N is Reflexive;
then
A1: dist(w,w) = 0 by METRIC_1:1;
assume 0<r;
hence thesis by A1,METRIC_1:11;
end;
theorem Th12:
for r being Real holds r<=0 implies Ball(t1,r) = {}
proof
let r be Real;
assume
A1: r<=0;
set c = the Element of Ball(t1,r);
assume
A2: Ball(t1,r) <> {};
then reconsider c as Point of T by TARSKI:def 3;
dist(t1,c)<r by A2,METRIC_1:11;
hence contradiction by A1,METRIC_1:5;
end;
Lm2: for r being Real holds 0<r implies Ball(t1,r) is bounded
proof
let r be Real;
assume
A1: 0<r;
set P = Ball(t1,r);
reconsider r as Real;
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,Th11;
let z be Point of T;
assume z in P;
hence thesis by METRIC_1:11;
end;
hence thesis by Th10;
end;
registration
let T,t1; let r be Real;
cluster Ball(t1,r) -> bounded;
coherence
proof
per cases;
suppose r<=0;
then Ball(t1,r) = {}T by Th12;
hence thesis;
end;
suppose 0<r;
hence thesis by Lm2;
end;
end;
end;
theorem Th13:
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 that
A1: P is bounded and
A2: Q is bounded;
per cases;
suppose
P = {};
hence thesis by A2;
end;
suppose
A3: P <> {};
now
per cases;
suppose
Q = {};
hence thesis by A1;
end;
suppose
Q <> {};
then consider s be Real, d be Element of T such that
A4: 0<s and
d in Q and
A5: for z being Point of T st z in Q holds dist(d,z)<=s by A2,Th10;
consider r,t1 such that
A6: 0<r and
A7: t1 in P and
A8: for z being Point of T st z in P holds dist(t1,z)<=r by A1,A3,Th10;
set t = r+s+dist(t1,d);
A9: 0<=dist(t1,d) by METRIC_1:5;
then
A10: r<r+(dist(t1,d)+s) by A4,XREAL_1:29;
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 reconsider t as Real;
take t,t1;
thus 0<t by A6,A4,A9;
thus t1 in P \/ Q by A7,XBOOLE_0:def 3;
let z be Point of T;
assume z in P \/ Q;
then
A11: z in P or z in Q by XBOOLE_0:def 3;
now
per cases by A8,A5,A11;
suppose
dist(t1,z)<=r;
hence thesis by A10,XXREAL_0:2;
end;
suppose
dist(d,z)<=s;
then dist(t1,z)<=dist(t1,d)+dist(d,z) & dist(t1,d)+dist(d,z)<=
dist(t1,d)+s by METRIC_1:4,XREAL_1:7;
then
A12: dist(t1,z)<=dist(t1,d)+s by XXREAL_0:2;
dist(t1,d)+s<=r+(dist(t1,d)+s) by A6,XREAL_1:29;
hence thesis by A12,XXREAL_0:2;
end;
end;
hence thesis;
end;
hence thesis by Th10;
end;
end;
hence thesis;
end;
end;
theorem Th14:
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 that
A1: C is bounded and
A2: D c= C;
consider r such that
A3: 0<r and
A4: for x,y being Point of N st x in C & y in C holds dist(x,y)<=r by A1;
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 A3;
let x,y be Point of N;
assume x in D & y in D;
hence thesis by A2,A4;
end;
hence thesis;
end;
theorem Th15:
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} is Subset of Ball(t1,1) by Th11,SUBSET_1:41;
hence thesis by A1,Th14;
end;
theorem Th16:
for P being Subset of T holds P is finite implies P is bounded
proof
let P be Subset of T;
defpred P[set] means ex X being Subset of T st X = $1 & X is bounded;
{}T is bounded;
then
A1: P[{}];
A2: 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
A3: x in P and
B c= P and
A4: P[B];
reconsider x as Element of T by A3;
reconsider W = {x} as Subset of T;
consider X being Subset of T such that
A5: X = B & X is bounded by A4;
A6: W is bounded by Th15;
ex Y being Subset of T st Y = B \/ {x} & Y is bounded
proof
take X \/ W;
thus thesis by A5,A6,Th13;
end;
hence thesis;
end;
assume
A7: P is finite;
P[P] from FINSET_1:sch 2(A7,A1,A2);
hence thesis;
end;
registration
let T;
cluster finite -> bounded for Subset of T;
coherence by Th16;
end;
registration
let T;
cluster finite non empty for Subset of T;
existence
proof
take the finite non empty Subset of T;
thus thesis;
end;
end;
theorem Th17:
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: 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
A4: x in Y and
B c= Y and
A5: P[B];
consider X being Subset of T such that
A6: X = union B & X is bounded by A5;
reconsider x as Subset of T by A4;
A7: union (B \/ {x}) = union B \/ union {x} by ZFMISC_1:78
.= union B \/ x by ZFMISC_1:25;
A8: x is bounded by A2,A4;
ex Y being Subset of T st Y = union (B \/ {x}) & Y is bounded
proof
take X \/ x;
thus thesis by A6,A7,A8,Th13;
end;
hence thesis;
end;
A9: P[{}]
proof
set m = {}T;
m = union {} by ZFMISC_1:2;
hence thesis;
end;
P[Y] from FINSET_1:sch 2(A1,A9,A3);
hence thesis;
end;
theorem Th18:
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 and
A2: for x,y being Point of N holds dist(x,y)<=r;
for x,y being Point of N st x in [#]N & y in [#]N holds dist(x,y ) <=
r by A2;
hence thesis by A1;
end;
assume [#]N is bounded;
then consider r such that
A3: 0<r and
A4: for x,y being Point of N st x in [#]N & y in [#]N holds dist(x,y)<=r;
take r;
thus 0<r by A3;
let x,y be Point of N;
thus thesis by A4;
end;
registration
let N be bounded non empty MetrStruct;
cluster [#]N -> bounded;
coherence by Th18;
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 & the carrier of T = union Y and
A2: for P st P in Y ex x being Element of T st P = Ball(x,1);
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 A2;
hence thesis;
end;
then [#]T is bounded by A1,Th17;
hence thesis by Th18;
end;
definition
let N be Reflexive non empty MetrStruct, C be Subset of N;
assume
A1: C is bounded;
func diameter C -> Real means
:Def8:
(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
set c = the Element of 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 where r is Element of REAL: 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 where r is Element of REAL : X[r] };
A2: for a,b being Real st a in J & b in I holds a<=b
proof
let a,b be Real;
assume a in J & b in I;
then
(ex t being Element of REAL
st t = a & ex x,y being Point of N st x in C & y in C & t = dist(x,y) )&
ex t9 being Element of REAL st t9=b & for x,y being Point of N st
x in C & y in C holds dist(x,y)<=t9;
hence thesis;
end;
A3: J is Subset of REAL from DOMAIN_1:sch 7;
assume
A4: C <> {};
then reconsider c as Point of N by TARSKI:def 3;
dist(c,c) = 0 by METRIC_1:1;
then
A5: In(0,REAL) in J by A4;
reconsider J as Subset of REAL by A3;
A6: I is Subset of REAL from DOMAIN_1:sch 7;
consider r such that
0<r and
A7: for x,y being Point of N st x in C & y in C holds dist(x,y)<=r
by A1;
reconsider r as Element of REAL by XREAL_0:def 1;
A8: r in I by A7;
reconsider I as Subset of REAL by A6;
consider d being Real such that
A9: for a being Real st a in J holds a<=d and
A10: for b being Real st b in I holds d<=b by A8,A5,A2,MEMBERED:37;
take d;
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
A11: x in C & y in C;
dist(x,y) in REAL by XREAL_0:def 1;
then dist(x,y) in J by A11;
hence thesis by A9;
end;
let s;
assume
A12: for x,y being Point of N st x in C & y in C holds dist(x,y)<=s;
reconsider s as Element of REAL by XREAL_0:def 1;
s in I by A12;
hence thesis by A10;
end;
thus thesis;
end;
uniqueness
proof
let r1,r2 be Real;
hereby
assume C <> {};
assume ( for x,y being Point of N st x in C & y in C holds dist(x,y)<=
r1)&( ( 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) & for x,y being Point of N st x in C & y in C holds dist(x,y)<=
r2 ) & 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;
then r1 <= r2 & r2 <= r1;
hence r1 = r2 by XXREAL_0:1;
end;
thus thesis;
end;
end;
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;
(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
A3: x in P and
A4: y in P;
x = t1 by A1,A3,TARSKI:def 1;
then dist(x,y) = dist(t1,t1) by A1,A4,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 A1,Def8;
end;
theorem Th21:
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 Def8;
end;
suppose
A2: S <> {};
set x = the Element of S;
reconsider x as Element of R by A2,TARSKI:def 3;
dist(x,x)<=diameter S by A1,A2,Def8;
hence thesis by METRIC_1:1;
end;
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 that
A1: A <> {} and
A2: A is bounded;
thus diameter A = 0 implies ex g being Point of M st A = {g}
proof
set g = the Element of A;
reconsider g as Element of M by A1,TARSKI:def 3;
assume
A3: diameter A = 0;
reconsider Z = {g} as Subset of M;
take g;
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 A2,A3,Def8;
then dist(x,g) = 0 by METRIC_1:5;
then x = g by METRIC_1:2;
hence thesis by TARSKI:def 1;
end;
assume
A4: x in Z;
g in A by A1;
hence thesis by A4,TARSKI:def 1;
end;
hence thesis by SUBSET_1:3;
end;
end;
theorem
0<r implies diameter Ball(t1,r) <= 2*r
proof
A1: 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:11;
then
A2: dist(t1,x)+dist(t1,y)<r+r by XREAL_1:8;
dist(x,y)<=dist(x,t1)+dist(t1,y) by METRIC_1:4;
hence thesis by A2,XXREAL_0:2;
end;
assume 0<r;
then t1 in Ball(t1,r) by Th11;
hence thesis by A1,Def8;
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,Th14;
per cases;
suppose
V = {};
then diameter V = 0 by Def8;
hence thesis by A1,Th21;
end;
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,Def8;
hence thesis by A3,A4,Def8;
end;
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 <> {};
set g = the Element of P /\ Q;
A4: g in Q by A3,XBOOLE_0:def 4;
set s = diameter P + diameter Q;
set b = diameter Q;
A5: b<=s by A1,Th21,XREAL_1:31;
set a = diameter P;
A6: g in P by A3,XBOOLE_0:def 4;
reconsider g as Element of T by A3,TARSKI:def 3;
A7: a<=s by A2,Th21,XREAL_1:31;
A8: 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
A9: x in P \/ Q and
A10: y in P \/ Q;
A11: dist(x,y)<=dist(x,g)+dist(g,y) by METRIC_1:4;
now
per cases by A9,XBOOLE_0:def 3;
suppose
A12: x in P;
now
per cases by A10,XBOOLE_0:def 3;
suppose
y in P;
then dist(x,y)<=a by A1,A12,Def8;
hence thesis by A7,XXREAL_0:2;
end;
suppose
A13: y in Q;
A14: dist(x,g)<=a by A1,A6,A12,Def8;
dist(g,y)<=b by A2,A4,A13,Def8;
then dist(x,g)+dist(g,y)<=a+b by A14,XREAL_1:7;
hence thesis by A11,XXREAL_0:2;
end;
end;
hence thesis;
end;
suppose
A15: x in Q;
now
per cases by A10,XBOOLE_0:def 3;
suppose
A16: y in P;
A17: dist(x,g)<=b by A2,A4,A15,Def8;
dist(g,y)<=a by A1,A6,A16,Def8;
then dist(x,g)+dist(g,y)<=b+a by A17,XREAL_1:7;
hence thesis by A11,XXREAL_0:2;
end;
suppose
y in Q;
then dist(x,y)<=b by A2,A15,Def8;
hence thesis by A5,XXREAL_0:2;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
P <> {} & P \/ Q is bounded by A1,A2,A3,Th13;
hence thesis by A8,Def8;
end;
theorem
for S1 being sequence of T holds S1 is Cauchy implies rng S1 is bounded
proof
let S1 be sequence of T;
set A = rng S1;
assume S1 is Cauchy;
then consider p such that
A1: for n,m st p<=n & p<=m holds dist(S1.n,S1.m)<1;
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
DOMAIN_1:sch 7;
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
DOMAIN_1:sch 7;
reconsider B, C as Subset of T;
A2: C is finite
proof
set K = Seg p;
set J = {0} \/ K;
now
let x be object;
thus x in C implies x in S1.:J
proof
assume x in C;
then consider t1 such that
A3: x = t1 and
A4: ex n st n<=p & t1 = S1.n;
consider n such that
A5: n<=p and
A6: t1 = S1.n by A4;
n in NAT by ORDINAL1:def 12;
then
A7: n in dom S1 by FUNCT_2:def 1;
now
per cases by NAT_1:6;
suppose
n=0;
then n in {0} by TARSKI:def 1;
then n in J by XBOOLE_0:def 3;
hence thesis by A3,A6,A7,FUNCT_1:def 6;
end;
suppose
ex m be Nat st n=m+1;
then 1<=n by NAT_1:11;
then n in { k where k is Nat: 1<=k & k<=p } by A5;
then n in K by FINSEQ_1:def 1;
then n in J by XBOOLE_0:def 3;
hence thesis by A3,A6,A7,FUNCT_1:def 6;
end;
end;
hence thesis;
end;
assume x in S1.:J;
then consider y being object such that
A8: y in dom S1 and
A9: y in J and
A10: x=S1.y by FUNCT_1:def 6;
reconsider y as Nat by A8;
now
per cases by A9,XBOOLE_0:def 3;
suppose
A11: y in {0};
S1.y is Element of T;
then reconsider x9=x as Element of T by A10;
y=0 by A11,TARSKI:def 1;
then ex n st n<=p & x9=S1.n by A10;
hence x in C;
end;
suppose
A12: y in K;
S1.y is Element of T;
then reconsider x9=x as Element of T by A10;
y in {k where k is Nat : 1<=k & k<=p } by A12,FINSEQ_1:def 1;
then ex k being Nat st y = k & 1<=k & k<=p;
then ex n st n<=p & x9=S1.n by A10;
hence x in C;
end;
end;
hence x in C;
end;
hence thesis by TARSKI:2;
end;
A13: A = B \/ C
proof
thus A c= B \/ C
proof
let x be object;
assume x in A;
then consider y being object such that
A14: y in dom S1 and
A15: x = S1.y by FUNCT_1:def 3;
reconsider y as Nat by A14;
S1.y is Element of T;
then reconsider x9=x as Element of T by A15;
per cases;
suppose
y<=p;
then ex n st n<=p & x9= S1.n by A15;
then x in C;
hence thesis by XBOOLE_0:def 3;
end;
suppose
p<=y;
then ex n st p<=n & x9= S1.n by A15;
then x in B;
hence thesis by XBOOLE_0:def 3;
end;
end;
let x be object;
assume
A16: x in B \/ C;
per cases by A16,XBOOLE_0:def 3;
suppose
x in B;
then consider t1 such that
A17: x = t1 and
A18: ex n st p<=n & t1 = S1.n;
consider n such that
p<=n and
A19: t1 = S1.n by A18;
n in NAT by ORDINAL1:def 12;
then n in dom S1 by FUNCT_2:def 1;
hence thesis by A17,A19,FUNCT_1:def 3;
end;
suppose
x in C;
then consider t1 such that
A20: x = t1 and
A21: ex n st n<=p & t1 = S1.n;
consider n such that
n<=p and
A22: t1 = S1.n by A21;
n in NAT by ORDINAL1:def 12;
then n in dom S1 by FUNCT_2:def 1;
hence thesis by A20,A22,FUNCT_1:def 3;
end;
end;
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 ex t1 st z = t1 & ex n st p<=n & t1 = S1.n;
hence thesis by A1;
end;
hence thesis by Th10;
end;
hence thesis by A2,A13,Th13;
end;