:: Totally Bounded Metric Spaces
:: by Alicia de la Cruz
::
:: Received September 30, 1991
:: Copyright (c) 1991-2016 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 00 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) Element of M means
for r st r>0 ex n st for m st m>=n holds dist(S1.m,it)0 ex n st for m st n<=m holds dist(S1.m,g1)0 ex n st for m st n<=m holds dist(S1.m,g2)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)0 ex p st for n,m st p<=n & p<=m holds dist(S2.n,S2.m)=n and
A7: m9>=n;
A8: dist(S2.m9,g) 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)0 ex p st for n,k st p<=n holds dist(S2
.(n+k),S2.n)0 ex p st for n,k st p<=n holds dist(S2.(n+k),S2.n)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)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)~~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) 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)~~~~=0 by METRIC_1:5;
assume y<>x;
then dist(y,x)<>0 by METRIC_1:2;
then L*dist(y,x) {}
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 00;
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 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 {} & C is bounded implies ex r,w st 0 {};
then reconsider w as Point of N by TARSKI:def 3;
assume C is bounded;
then consider r such that
A2: 0 {};
then reconsider c as Point of T by TARSKI:def 3;
dist(t1,c) bounded;
coherence
proof
per cases;
suppose r<=0;
then Ball(t1,r) = {}T by Th12;
hence thesis;
end;
suppose 0 {};
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~~~~ 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 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 {};
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 {};
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~~