### The Mizar article:

### Totally Bounded Metric Spaces

**by****Alicia de la Cruz**

- Received September 30, 1991
Copyright (c) 1991 Association of Mizar Users

- MML identifier: TBSP_1
- [ MML identifier index ]

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;

Back to top