:: Complete Spaces
:: by Karol P\c{a}k
::
:: Received October 12, 2007
:: Copyright (c) 2007 Association of Mizar Users
environ
vocabularies WELLFND1, FRECHET2, REARRAN1, BOOLE, PRE_TOPC, COMPTS_1,
SETFAM_1, METRIC_1, SUBSET_1, PCOMPS_1, RELAT_1, ORDINAL2, LATTICES,
SEQ_2, PROB_1, SEQ_1, FUNCT_1, FRECHET, ARYTM_3, ARYTM, ARYTM_1,
NORMSP_1, INT_1, ZF_REFLE, RELAT_2, ABSVALUE, FINSET_1, TARSKI, BHSP_3,
TBSP_1, URYSOHN1, CARD_1, RLVECT_3, PARTFUN1, WELLORD1, METRIC_6,
TOPGEN_1, RAT_1, CARD_4, AMI_1, ORDERS_1, WAYBEL23, SQUARE_1, COMPL_SP;
notations BHSP_3, METRIC_6, RELAT_2, BINOP_1, URYSOHN1, TOPMETR, CARD_1,
CANTOR_1, WELLORD1, COMPLEX1, FINSET_1, SEQ_2, TARSKI, XBOOLE_0,
SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, ZFMISC_1, XXREAL_0, XREAL_0,
REAL_1, NAT_1, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1,
RELAT_1, FUNCT_1, SEQ_1, TBSP_1, RELSET_1, PARTFUN1, FUNCT_2, METRIC_1,
PCOMPS_1, CARD_3, PROB_1, SEQM_3, FRECHET, KURATO_2, WELLFND1, WAYBEL23,
ORDERS_2, CARD_4, TOPGEN_1, FLANG_1;
constructors REAL_1, NAT_1, TBSP_1, YELLOW_6, FRECHET, FRECHET2, KURATO_2,
COMPLEX1, SEQ_2, TOPS_2, WELLORD1, CARD_4, CANTOR_1, URYSOHN3, METRIC_6,
REALSET1, WELLFND1, TOPGEN_4, WAYBEL23, TOPGEN_1, FLANG_1;
registrations REALSET1, TOPMETR, PRE_TOPC, PCOMPS_1, NAT_1, TBSP_1, XREAL_0,
RELSET_1, SUBSET_1, STRUCT_0, TOPS_1, METRIC_1, METRIC_3, HAUSDORF,
MEMBERED, ORDINAL1, XXREAL_0, YELLOW13, CARD_1, WAYBEL12, ORDERS_2,
XBOOLE_0;
requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, TOPS_2, SUBSET_1, STRUCT_0, TBSP_1, PCOMPS_1, COMPTS_1,
METRIC_1;
theorems KURATO_2, NAT_1, FUNCT_2, PCOMPS_1, PCOMPS_2, NAGATA_1, SUBSET_1,
METRIC_6, FUNCT_1, METRIC_1, XREAL_0, XCMPLX_1, ABSVALUE, TOPMETR,
XBOOLE_1, TARSKI, SETFAM_1, XBOOLE_0, TOPS_1, TOPS_2, PRE_TOPC, FINSET_1,
CARD_4, ZFMISC_1, BINOP_1, SEQ_2, SEQ_4, SEQ_1, SEQM_3, PARTFUN1,
WELLORD1, WELLORD2, TBSP_1, RELAT_1, RELAT_2, YELLOW_9, XREAL_1,
XXREAL_0, ORDINAL1, RELSET_1, FRECHET2, FRECHET, COMPTS_1, STIRL2_1,
CARD_1, EULER_1, HAUSDORF, TOPMETR3, CARD_3, TOPGEN_4, STRUCT_0, DICKSON,
RELSET_2, TOPGEN_1, YELLOW13, WELLFND1, CARD_FIL, WAYBEL23, UNIFORM1,
CARD_2;
schemes FUNCT_1, WELLFND1, TREES_2, FUNCT_2, NAT_1, FRAENKEL, BINOP_1,
KURATO_2, SEQ_1;
begin :: Preliminaries
reserve i,j,n,m for natural number,
x,y,X,Y for set,
r,s for Real;
definition
let M be non empty MetrStruct;
let S be SetSequence of M;
attr S is bounded means :def1:
for i holds S.i is bounded;
end;
registration
let M be non empty Reflexive MetrStruct;
cluster bounded non-empty SetSequence of M;
existence
proof
consider x such that
A1: x in the carrier of M by XBOOLE_0:def 1;
reconsider x as Point of M by A1;
reconsider X={x} as Subset of M;
A2: now let x1,x2 being Point of M such that A3:x1 in X & x2 in X;
x1=x & x2=x by A3,TARSKI:def 1;
hence dist(x1,x2)<=1 by METRIC_1:1;
end;
deffunc F(set)=X;
consider S being SetSequence of M such that
A3: for n being Element of NAT holds S.n = F(n) from KURATO_2:sch 1;
take S;
A4: now let i;
reconsider i'=i as Element of NAT by ORDINAL1:def 13;
X is bounded & S.i'=F(i) by A2,A3,TBSP_1:def 9;
hence S.i is bounded;
end;
for x st x in dom S holds S.x is non empty by A3;
hence thesis by A4,def1,FUNCT_1:def 15;
end;
end;
definition let M be Reflexive non empty MetrStruct;
let S be SetSequence of M;
func diameter S -> Real_Sequence means :def2:
for i holds it.i = diameter S.i;
existence
proof
defpred P[set,set] means for i st i=$1 holds $2=diameter (S.i);
A1: for x st x in NAT ex y st y in REAL & P[x,y]
proof
let x such that A2:x in NAT;
reconsider i=x as Element of NAT by A2;
take diameter (S.i);
thus thesis by XREAL_0:def 1;
end;
consider f be Function of NAT,REAL such that
A2: for x st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A1);
take f;
let i;
i in NAT by ORDINAL1:def 13;
hence thesis by A2;
end;
uniqueness
proof
let D1,D2 be Real_Sequence such that
A1: for i holds D1.i = diameter S.i and
A2: for i holds D2.i = diameter S.i;
now let x such that A3:x in NAT;
reconsider i=x as Element of NAT by A3;
thus D1.x = diameter S.i by A1
.= D2.x by A2;
end;
hence thesis by SEQ_1:8;
end;
end;
theorem Th1:
for M be Reflexive non empty MetrStruct
for S be bounded SetSequence of M holds
diameter S is bounded_below
proof
let M be Reflexive non empty MetrStruct;
let S be bounded SetSequence of M;set d=diameter S;
now let n be Element of NAT;
S.n is bounded & diameter (S.n)=d.n by def1,def2;
then 0<=d.n by TBSP_1:29;
hence -1 < d.n by XXREAL_0:2;
end;
hence thesis by SEQ_2:def 4;
end;
theorem Th2:
for M be Reflexive non empty MetrStruct
for S be bounded SetSequence of M st S is descending holds
diameter S is bounded_above & diameter S is non-increasing
proof
let M be Reflexive non empty MetrStruct;
let S be bounded SetSequence of M such that
A1:S is descending;
set d=diameter S;
A2:now let n be Element of NAT;
S.n c= S.0 & S.0 is bounded & diameter S.n=d.n & diameter S.0=d.0
by A1,KURATO_2:22,def1,def2;
then d.n<=d.0 & d.0+0=d.m by TBSP_1:32;
end;
hence thesis by SEQM_3:def 3;
end;
theorem Th4:
for M be non empty Reflexive MetrStruct
for S be bounded SetSequence of M st
S is descending & lim diameter S = 0
for F be sequence of M st for i holds F.i in S.i
holds F is Cauchy
proof
let M be non empty Reflexive MetrStruct;
let S be bounded SetSequence of M such that
A1: S is descending & lim diameter S = 0;set d=diameter S;
let F be sequence of M such that
A2: for i holds F.i in S.i;
let r such that
A3: r>0;
d is bounded_below & d is non-increasing by A1,Th1,Th2;
then d is convergent by SEQ_4:52;
then consider n be Element of NAT such that
A4: for m be Element of NAT st n <= m holds abs(d.m-0) < r
by A1,A3,SEQ_2:def 7;
take n;
let m1,m2 be Element of NAT such that
A5:n <= m1 & n <= m2;
S.m1 c= S.n & S.m2 c= S.n & F.m1 in S.m1 & F.m2 in S.m2
by A1,A2,A5,KURATO_2:22;
then F.m1 in S.n & F.m2 in S.n & S.n is bounded & diameter S.n=d.n
by def1,def2;
then A5:dist(F.m1,F.m2)<=d.n & 0 <= d.n & abs(d.n-0){};then
A4: CL<>{} by A2,PCOMPS_1:2;
d >= 0 by A1,TBSP_1:29;then
A5: d+1>0+0 by XREAL_1:10;
A6: now let x,y be Point of M such that
A7: x in CL & y in CL; assume
A8:dist(x,y) > d;
set dxy=dist(x,y);set dd=dxy-d;set dd2=dd/2;
set Bx=Ball(x,dd2);set By=Ball(y,dd2);
reconsider BX=Bx,BY=By as Subset of T;
reconsider X=x,Y=y as Point of T;
dd > d-d by A8,XREAL_1:16;then
A9:dd2>0/2 by XREAL_1:76;
dist(x,x)=0 & dist(y,y)=0 & Bx in Family_open_set M &
By in Family_open_set M by METRIC_1:1,PCOMPS_1:33;
then X in BX & Y in BY & BX is open & BY is open
by A9,METRIC_1:12,PRE_TOPC:def 5;then
A10:BX meets S' & BY meets S' by A2,A7,TOPS_1:39;
then consider x1 be set such that
A11:x1 in BX & x1 in S' by XBOOLE_0:3;
consider y1 be set such that
A12:y1 in BY & y1 in S' by A10,XBOOLE_0:3;
reconsider x1,y1 as Point of M by A11,A12;
A13:dist(x1,y1)<=d & dist(x,x1)= i } & S.i = Cl U
proof
let M be Reflexive symmetric triangle non empty MetrSpace;
set T=TopSpaceMetr(M);
let C be sequence of M;
defpred P[set,set] means for i st i=$1 ex S be Subset of T st
S={C.j where j is Element of NAT: j >= i} & $2=Cl S;
A1:for x st x in NAT ex y st y in bool(the carrier of M) & P[x,y]
proof
let x such that
A2: x in NAT;
reconsider x'=x as Element of NAT by A2;
set S={C.j where j is Element of NAT: j >= x'};
S c= the carrier of T
proof
let y such that A3:y in S;
ex j be Element of NAT st C.j=y & j>=x' by A3;
hence thesis;
end;
then reconsider S as Subset of T;
take CL=Cl S;
thus thesis;
end;
consider S be SetSequence of M such that
A2: for x st x in NAT holds P[x,S.x] from FUNCT_2:sch 1(A1);
A3:now let x such that
A4: x in dom S;
reconsider i=x as Element of NAT by A4;
consider U be Subset of T such that
A5: U={C.j where j is Element of NAT: j >= i} & S.i=Cl U by A2;
C.i in U & U c= S.i by A5,PRE_TOPC:48;
hence S.x is non empty;
end;
A4:now let i;
i in NAT by ORDINAL1:def 13;
then ex U be Subset of T st
U={C.j where j is Element of NAT: j >= i} & S.i=Cl U by A2;
hence S.i is closed by Th7;
end;
reconsider S as non-empty closed SetSequence of M
by A3,A4,def8,FUNCT_1:def 15;
take S;
now let i be Element of NAT;
consider U be Subset of T such that
A6: U={C.j where j is Element of NAT: j >= i} & S.i=Cl U by A2;
consider U1 be Subset of T such that
A7: U1={C.j where j is Element of NAT: j >= i+1} & S.(i+1)=Cl U1 by A2;
U1 c= U
proof
let x such that
A8: x in U1;
consider j be Element of NAT such that
A9: x=C.j & j>=i+1 by A7,A8;
j>= i by A9,NAT_1:13;
hence thesis by A6,A9;
end;
hence S.(i+1) c= S.i by A6,A7,PRE_TOPC:49;
end;
hence A5':S is descending by KURATO_2:def 5;
thus C is Cauchy implies S is bounded & lim diameter S = 0
proof
assume
A6: C is Cauchy;
A7: now let i;
i in NAT by ORDINAL1:def 13;
then consider U be Subset of T such that
A8: U={C.j where j is Element of NAT: j >= i} & S.i=Cl U by A2;
reconsider U'=U as Subset of M;
A9: U c= rng C
proof
let x such that
A10: x in U;
dom C=NAT & ex j be Element of NAT st x=C.j & j>=i
by A8,A10,FUNCT_2:def 1;
hence thesis by FUNCT_1:def 5;
end;
rng C is bounded by A6,TBSP_1:34;
then U' is bounded by A9,TBSP_1:21;
hence S.i is bounded by A8,Th9;
end;
hence S is bounded by def1;
reconsider S'=S as non-empty bounded closed SetSequence of M
by A7,def1;
set d=diameter S';
d is bounded_below & d is non-increasing by A5',Th1,Th2;then
A8: d is convergent by SEQ_4:52;
for r be real number st 00 by A9,XREAL_1:141;
then consider p be Element of NAT such that
A10: for n,m be Element of NAT st p<=n & p<=m holds
dist(C.n,C.m)= m} & S.m=Cl U by A2;
reconsider CL=Cl U,U'=U as Subset of M;
A13: U c= rng C
proof
let x such that
A14: x in U;
dom C=NAT & ex j be Element of NAT st x=C.j & j>=m
by A12,A14,FUNCT_2:def 1;
hence thesis by FUNCT_1:def 5;
end;
rng C is bounded & C.m in U by A6,A12,TBSP_1:34;then
A14:U' is bounded & U' is non empty by A13,TBSP_1:21;
now let x,y being Point of M such that
A15: x in U' & y in U';
consider i be Element of NAT such that
A16: x = C.i & i>=m by A12,A15;
consider j be Element of NAT such that
A17: y=C.j & j>=m by A12,A15;
i>=p & j>=p by A11,A16,A17,XXREAL_0:2;
hence dist(x,y)<=R2 by A10,A16,A17;
end;
then diameter U'<=R2 & diameter U'=diameter S.m
by A12,A14,TBSP_1:def 10,Th9;
then diameter S.m <= R2 & diameter S.m>=0 by A14,TBSP_1:29;
then abs(diameter S.m)<=R2 & R2= i} & S.i = Cl U by Th10;
meet S is non empty by A1,A2,A3,A4;
then consider x such that
A6: x in meet S by XBOOLE_0:def 1;
reconsider x as Point of M by A6;
take x;
let r such that
A7: r>0;
set d=diameter S;
d is bounded_below & d is non-increasing by A2,A3,A4,Th1,Th2;
then d is convergent by SEQ_4:52;
then consider n be Element of NAT such that
A8: for m be Element of NAT st n<=m holds abs(d.m-0)= m } & S.m = Cl U by A5;
F.m in U & U c= Cl U by A10,PRE_TOPC:48;
then x in S.m & F.m in S.m & S.m is bounded by A2,A4,A6,A10,KURATO_2:6,def1;
then dist(F.m,x) <= diameter (S.m) & diameter (S.m)>=0 & diameter (S.m)=d.m
& abs(d.m-0){} by A2,RELAT_1:65;
now let G be set such that
A4: G <> {} & G c= F & G is finite;
defpred P[set,set] means $1=S.$2;
A5:for x st x in G ex y st y in NAT & P[x,y]
proof
let x such that
A6: x in G;
ex y st y in dom S & S.y=x by A2,A4,A6,FUNCT_1:def 5;
hence thesis;
end;
consider f be Function of G,NAT such that
A6: for x st x in G holds P[x,f.x] from FUNCT_2:sch 1(A5);
A7:dom f=G by FUNCT_2:def 1;
then rng f is finite by A4,FINSET_1:26;
then consider i be Element of NAT such that
A8: for j be Element of NAT st j in rng f holds j<=i by STIRL2_1:66;
dom S=NAT by FUNCT_2:def 1;
then S.i<>{} by FUNCT_1:def 15;
then consider x such that
A9: x in S.i by XBOOLE_0:def 1;
now let Y be set;
assume
A10: Y in G;then
A11:f.Y in rng f by A7,FUNCT_1:def 5;
then reconsider fY=f.Y as Element of NAT;
Y=S.fY & fY <= i by A6,A8,A10,A11;
then S.i c= Y by A1,KURATO_2:22;
hence x in Y by A9;
end;
hence meet G<>{} by A4,SETFAM_1:def 1;
end;
hence thesis by A3,COMPTS_1:def 2;
end;
theorem Th13:
for M be non empty MetrStruct
for S be SetSequence of M
for F be Subset-Family of TopSpaceMetr M st F = rng S
holds
( S is open implies F is open ) & ( S is closed implies F is closed )
proof
let M be non empty MetrStruct;
let S be SetSequence of M;
set T=TopSpaceMetr(M);
let F be Subset-Family of T such that
A1: F = rng S;
thus S is open implies F is open
proof
assume
A2: S is open;
let P be Subset of T;
assume P in F;
then consider x such that
A3: x in dom S & S.x=P by A1,FUNCT_1:def 5;
reconsider x as natural number by A3,ORDINAL1:def 13;
S.x is open by A2,def7;
hence thesis by A3,Th7;
end;
assume
A2: S is closed;
let P be Subset of T;
assume P in F;
then consider x such that
A3: x in dom S & S.x=P by A1,FUNCT_1:def 5;
reconsider x as natural number by A3,ORDINAL1:def 13;
S.x is closed by A2,def8;
hence thesis by A3,Th7;
end;
theorem Th14:
for T be non empty TopSpace
for F be Subset-Family of T
for S be SetSequence of T st rng S c= F
ex R be SetSequence of T st
R is descending &
( F is centered implies R is non-empty ) &
( F is open implies R is open ) & ( F is closed implies R is closed ) &
for i holds R.i = meet {S.j where j is Element of NAT: j <= i}
proof
let T be non empty TopSpace;
let F be Subset-Family of T;
let S be SetSequence of T such that
A1: rng S c= F;
A2:for i holds {S.j where j is Element of NAT: j <= i} c= F
proof
let i;
let x such that
A3: x in {S.j where j is Element of NAT : j <= i};
consider j be Element of NAT such that
A4: x=S.j & j<=i by A3;
dom S=NAT by FUNCT_2:def 1;
then x in rng S by A4,FUNCT_1:def 5;
hence thesis by A1;
end;
defpred P[set,set] means
for i st i=$1 holds $2=meet {S.j where j is Element of NAT:j<=i};
A3:for x st x in NAT ex y st y in bool(the carrier of T) & P[x,y]
proof
let x such that
A4: x in NAT;
reconsider i=x as Element of NAT by A4;
set SS={S.j where j is Element of NAT:j<=i};
SS c= F by A2;
then reconsider SS as Subset-Family of T by XBOOLE_1:1;
take meet SS;
thus thesis;
end;
consider R be SetSequence of T such that
A4: for x st x in NAT holds P[x,R.x] from FUNCT_2:sch 1(A3);
A5:for i holds {S.j where j is Element of NAT:j<=i} is finite
proof
let i;
set SS={S.j where j is Element of NAT:j<=i};
reconsider i'=i as Element of NAT by ORDINAL1:def 13;
A6:i+1 is finite;
deffunc F(set)=S.$1;
A7:{F(j)where j is Element of NAT:j in i+1} is finite
from FRAENKEL:sch 21(A6);
SS c= {F(j)where j is Element of NAT:j in i+1}
proof
let x such that
A8: x in SS;
consider j be Element of NAT such that
A9: x=S.j & j<=i by A8;
j*{} by A6,COMPTS_1:def 2;
hence R.x is non empty by A4;
end;
hence thesis by FUNCT_1:def 15;
end;
thus F is open implies R is open
proof
assume
A6: F is open;
let i;
set SS={S.j where j is Element of NAT:j<=i};
A7:SS c= F by A2;
then reconsider SS as Subset-Family of T by XBOOLE_1:1;
SS is open & SS is finite & i in NAT
by A5,A6,A7,TOPS_2:18,ORDINAL1:def 13;
then meet SS is open & R.i=meet SS by A4,TOPS_2:27;
hence thesis;
end;
thus F is closed implies R is closed
proof
assume
A6: F is closed;
let i;
set SS={S.j where j is Element of NAT:j<=i};
A7:SS c= F by A2;
then reconsider SS as Subset-Family of T by XBOOLE_1:1;
SS is closed & i in NAT by A6,A7,TOPS_2:19,ORDINAL1:def 13;
then meet SS is closed & meet SS=R.i by A4,TOPS_2:29;
hence thesis;
end;
let i;
i in NAT by ORDINAL1:def 13;
hence thesis by A4;
end;
theorem
for M be non empty MetrSpace holds
M is complete iff
for F be Subset-Family of TopSpaceMetr M st F is closed & F is centered
& for r be Real st r > 0
ex A be Subset of M st A in F & A is bounded & diameter A < r
holds meet F is non empty
proof
let M be non empty MetrSpace;
set T=TopSpaceMetr(M);
thus M is complete implies
for F be Subset-Family of T st F is closed & F is centered & for r st r>0
ex A be Subset of M st A in F & A is bounded & diameter A < r
holds meet F is non empty
proof
assume
A1: M is complete;
let F be Subset-Family of T such that
A2: F is closed & F is centered and
A3: for r st r>0 ex A be Subset of M st A in F & A is bounded & diameter A 0 by XREAL_1:141;
then consider A be Subset of M such that
A6: A in F & A is bounded & diameter A < 1/(i+1) by A3;
take A;
thus thesis by A6;
end;
consider f be SetSequence of M such that
A5: for x st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A4);
A6:rng f c= F
proof
let x such that
A7: x in rng f;
consider y such that
A8: y in dom f & f.y=x by A7,FUNCT_1:def 5;
reconsider y as Element of NAT by A8;
f.y in F by A5;
hence thesis by A8;
end;
consider R be SetSequence of T such that
A7: R is descending and
B6: F is centered implies R is non-empty and
F is open implies R is open and
A8: F is closed implies R is closed and
A9: for i holds R.i = meet {f.j where j is Element of NAT: j<=i} by A6,Th14;
reconsider R'=R as non-empty SetSequence of M by A2,B6;
now let i;
f.0 in {f.j where j is Element of NAT: j <= i} ;
then meet {f.j where j is Element of NAT: j <= i} c= f.0 by SETFAM_1:4;
then R.i c= f.0 & f.0 is bounded by A5,A9;
hence R'.i is bounded by TBSP_1:21;
end;
then reconsider R' as non-empty bounded SetSequence of M by def1;
A8':R' is closed & R' is descending by A7,A8,A2,Th8;
deffunc F(Element of NAT)=1/(1+$1);
consider seq be Real_Sequence such that
A10:for n be Element of NAT holds seq.n=F(n) from SEQ_1:sch 1;
reconsider NULL=0 as Real;set Ns=NULL(#)seq;
for n be Element of NAT holds seq.n=1/(n+1) by A10;then
A11:seq is convergent & lim seq=0 by SEQ_4:45;then
A12:Ns is convergent & lim Ns=NULL*0 by SEQ_2:21,22;
set dR=diameter R';
now let n be Element of NAT;
set Sn={f.j where j is Element of NAT:j<=n};
f.n in Sn & R.n=meet Sn by A9;
then R.n c= f.n & f.n is bounded by A5,SETFAM_1:4;
then diameter R'.n <= diameter f.n & diameter f.n < F(n)&R'.n is bounded
by A5,TBSP_1:21,32;
then 0<= diameter R'.n & diameter R'.n <= F(n) & Ns.n=NULL*seq.n
& F(n)=seq.n & diameter R'.n=dR.n
by A10,XXREAL_0:2,TBSP_1:29,SEQ_1:13,def2;
hence Ns.n <= dR.n & dR.n<=seq.n;
end;then
B1:dR is convergent & lim dR=0 by A11,A12,SEQ_2:33,34;
then meet R'<>{} by A1,A8',Th11;
then consider x0 be set such that
A13:x0 in meet R' by XBOOLE_0:def 1;
reconsider x0 as Point of M by A13;
A14:now let y;
assume
A15: y in F;
then reconsider Y=y as Subset of T;
defpred P'[set,set] means for i st i=$1 holds $2=R.i/\Y;
A16:for x st x in NAT ex z be set st z in bool(the carrier of M) & P'[x,z]
proof
let x such that
A17: x in NAT;
reconsider i=x as Element of NAT by A17;
take R.i/\Y;
thus thesis;
end;
consider f' be SetSequence of M such that
A17: for x st x in NAT holds P'[x,f'.x] from FUNCT_2:sch 1(A16);
A18:now let x such that
A19: x in dom f';
reconsider i=x as Element of NAT by A19;
set SS={f.j where j is Element of NAT:j<=i};
A20':Y in {Y} & f.i in SS by TARSKI:def 1;
A21:{Y}\/SS c= F
proof
let z be set such that
A22:z in {Y}\/SS;
per cases by A22,XBOOLE_0:def 2;
suppose z in {Y};
hence thesis by A15,TARSKI:def 1;end;
suppose z in SS;
then ex j be Element of NAT st z=f.j & j<=i;
hence thesis by A5;end;
end;
A22:i+1 is finite;
deffunc F(set)=f.$1;
A23:{F(j)where j is Element of NAT:j in i+1} is finite
from FRAENKEL:sch 21(A22);
SS c= {F(j) where j is Element of NAT:j in i+1}
proof
let x such that
A24: x in SS;
consider j be Element of NAT such that
A25: x=f.j & j<=i by A24;
j**{} by A2,A21,COMPTS_1:def 2;
then meet {Y} /\ meet SS <> {} by A20',SETFAM_1:10;
then Y /\meet SS<>{} by SETFAM_1:11;
then Y/\R.i<>{} by A9;
hence f'.x is non empty by A17;
end;
A19:now let i;
i in NAT by ORDINAL1:def 13;
then f'.i=R'.i /\ Y & R'.i is bounded & R.i /\ Y c= R.i
by A17,def1,XBOOLE_1:17;
hence f'.i is bounded by TBSP_1:21;
end;
now let i;
reconsider Ri=R.i as Subset of T;
R'.i is closed by A8',def8;
then Ri is closed & Y is closed & i in NAT
by A2,A15,TOPS_2:def 2,Th7,ORDINAL1:def 13;
then Ri/\Y is closed & f'.i=Ri/\Y by A17,TOPS_1:35;
hence f'.i is closed by Th7;
end;
then reconsider f' as non-empty bounded closed SetSequence of M
by A18,A19,FUNCT_1:def 15,def1,def8;
now let i be Element of NAT;
f'.(i+1) =R.(i+1)/\Y & f'.i = R.i/\Y & R.(i+1) c= R.i
by A7,A17,KURATO_2:def 5;
hence f'.(i+1) c= f'.i by XBOOLE_1:26;
end;then
A20:f' is descending by KURATO_2:def 5;
set df=diameter f';
now let n be Element of NAT;
reconsider Y'=Y as Subset of M;
R'.n is bounded & R.n/\Y c= R.n & R.n/\Y'=f'.n
by A17,def1,XBOOLE_1:17;
then f'.n is bounded & diameter f'.n <= diameter R'.n
by TBSP_1:21,32;
then 0<=diameter f'.n & diameter f'.n <= dR.n &
Ns.n=NULL*seq.n by TBSP_1:29,def2,SEQ_1:13;
hence Ns.n <= df.n & df.n<=dR.n by def2;
end;
then lim df=0 by A12,B1,SEQ_2:34;
then meet f'<>{} by A1,A20,Th11;
then consider z be set such that
A21: z in meet f' by XBOOLE_0:def 1;
reconsider z as Point of M by A21;
A22: x0 = z
proof
assume x0<>z;
then dist(x0,z)<>0 by METRIC_1:2;
then dist(x0,z)>0 by METRIC_1:5;
then consider i be Element of NAT such that
A23: for j be Element of NAT st i<=j holds
abs(dR.j-0)=dist(x0,z) & abs(dR.i-0){} by A2,COMPTS_1:def 2;
hence thesis by A14,SETFAM_1:def 1;
end;
assume
A1:for F be Subset-Family of T st F is closed & F is centered &
for r st r > 0 ex A be Subset of M st A in F & A is bounded&diameter A 0;
set d=diameter S;
d is bounded_below & d is non-increasing by A2,Th1,Th2;
then d is convergent by SEQ_4:52;
then consider n be Element of NAT such that
A5: for m be Element of NAT st n<=m holds abs(d.m-0)=0 & dom S=NAT
by A5,def2,TBSP_1:29,FUNCT_2:def 1;
hence Sn in RS & Sn is bounded & diameter Sn {} & S.i in RS by RELAT_1:65,FUNCT_1:def 5;
hence x in S.i by A4,SETFAM_1:def 1;
end;
hence meet S is non empty by KURATO_2:6;
end;
hence thesis by Th11;
end;
theorem Th16:
for M be non empty MetrSpace,A be non empty Subset of M
for B be Subset of M, B' be Subset of M|A st B = B' holds
B' is bounded iff B is bounded
proof
let M be non empty MetrSpace,A be non empty Subset of M;
let B be Subset of M, B' be Subset of M|A such that
A1: B = B';
thus B' is bounded implies B is bounded
proof
assume
A2: B' is bounded;
B' c= the carrier of (M|A);
then B' c= A by TOPMETR:def 2;
hence thesis by A1,A2,HAUSDORF:19;
end;
assume
A2:B is bounded;
per cases;
suppose B'={}(M|A);
hence thesis;end;
suppose B'<>{}(M|A);
then consider p be set such that
A3: p in B' by XBOOLE_0:def 1;
reconsider p as Point of (M|A) by A3;
diameter B>=0 by A2,TBSP_1:29;then
A4:0+0 < diameter B+1 by XREAL_1:10;
now let q be Point of (M|A) such that
A5: q in B';
reconsider p'=p,q'=q as Point of M by TOPMETR:12;
A6:dist(p,q) = dist(p',q') by TOPMETR:def 1;
dist(p',q')<=diameter B & diameter B+0<=diameter B+1
by A1,A2,A3,A5,TBSP_1:def 10,XREAL_1:10;
hence dist(p,q)<=diameter B+1 by A6,XXREAL_0:2;
end;
hence thesis by A3,A4,TBSP_1:15;end;
end;
theorem Th17:
for M be non empty MetrSpace,A be non empty Subset of M
for B be Subset of M, B' be Subset of M|A st B = B' & B is bounded holds
diameter B' <= diameter B
proof
let M be non empty MetrSpace,A be non empty Subset of M;
let B be Subset of M, B' be Subset of M|A such that
A1: B = B' & B is bounded;
A2:B' is bounded by A1,Th16;
per cases;
suppose B'={}(M|A);
then diameter B'=0 & 0<=diameter B by A1,TBSP_1:def 10;
hence thesis;end;
suppose
A3: B'<>{}(M|A);
now let x,y be Point of (M|A) such that
A4: x in B' & y in B';
reconsider x'=x,y'=y as Point of M by TOPMETR:12;
dist(x,y) = dist(x',y') by TOPMETR:def 1;
hence dist(x,y)<=diameter B by A1,A4,TBSP_1:def 10;
end;
hence thesis by A2,A3,TBSP_1:def 10;end;
end;
theorem Th18:
for M be non empty MetrSpace, A be non empty Subset of M
for S be sequence of (M|A) holds S is sequence of M
proof
let M be non empty MetrSpace, A be non empty Subset of M;
let S be sequence of (M|A);
A c= the carrier of M;
then the carrier of (M|A) c= the carrier of M &
NAT<>{} by TOPMETR:def 2;
hence thesis by FUNCT_2:9;
end;
theorem Th19:
for M be non empty MetrSpace, A be non empty Subset of M
for S be sequence of (M|A),S' be sequence of M st S = S' holds
S' is Cauchy iff S is Cauchy
proof
let M be non empty MetrSpace, A be non empty Subset of M;
let S be sequence of (M|A),S' be sequence of M such that
A1:S = S';
thus S' is Cauchy implies S is Cauchy
proof
assume
A2: S' is Cauchy;
let r such that
A3: r>0;
consider p be Element of NAT such that
A4: for n,m be Element of NAT st p<=n & p<=m holds
dist(S'.n,S'.m)0;
consider p be Element of NAT such that
A4: for n,m be Element of NAT st p<=n & p<=m holds
dist(S.n,S.m)0
by PCOMPS_1:33,XREAL_1:141;
then B is open & p in B by PRE_TOPC:def 5,TBSP_1:16;
then B meets A' by A5,PRE_TOPC:54;
then consider y such that
A10: y in B & y in A' by XBOOLE_0:3;
reconsider y as Point of M by A10;
dist(p,y)< 1/(i+1) by A10,METRIC_1:12;
then y in cl_Ball(p,1/(i+1)) by METRIC_1:13;
then y in A/\cl_Ball(p,1/(i+1)) by A2,A10,XBOOLE_0:def 3;
hence f.x is non empty by A7;
end;
A9:now let i;
set ACL=A/\cl_Ball(p,1/(i+1));
cl_Ball(p,1/(i+1)) is bounded & ACL c= cl_Ball(p,1/(i+1))
by Th5,XBOOLE_1:17;
then A10:ACL is bounded by TBSP_1:21;
i in NAT by ORDINAL1:def 13;
then f.i=ACL by A7;
hence f.i is bounded by A10,Th16;
end;
now let i;
reconsider cB=cl_Ball(p,1/(i+1)) as Subset of T;
cB`=[#]M\cB & [#]M\cB in Family_open_set(M) by NAGATA_1:14;
then cB` is open by PRE_TOPC:def 5;then
A10:cB is closed by TOPS_1:29;
reconsider fi=f.i as Subset of TA;
A11:TA=T|A' by A2,HAUSDORF:18;
then [#](T|A')=A & i in NAT by TOPMETR:def 2,ORDINAL1:def 13;
then fi=cB/\[#](T|A') by A7;
then fi is closed by A10,A11,PRE_TOPC:43;
hence f.i is closed by Th7;
end;
then reconsider f as non-empty bounded closed SetSequence of MA
by A8,A9,FUNCT_1:def 15,def1,def8;
now let i be Element of NAT;set i1=i+1;
cl_Ball(p,1/(i1+1)) c= cl_Ball(p,1/i1)
proof
let x such that
A10: x in cl_Ball(p,1/(i1+1));
reconsider q=x as Point of M by A10;
i1 q;
then dist(p,q)<>0 by METRIC_1:2;
then dist(p,q)>0 by METRIC_1:5;
then consider n be Element of NAT such that
A16:for m be Element of NAT st n<=m holds abs(seq.m-0)= 0
by A11,A7,A14,KURATO_2:6;
then q in cB & abs(seq.n-0)=F(n)
by XBOOLE_0:def 3,ABSVALUE:def 1;
then dist(p,q) <= F(n) & F(n) < dist(p,q) by A16,METRIC_1:13;
hence thesis;
end;
then f.0=A/\cl_Ball(p,1/(0+1)) & p in f.0 by A7,A14,KURATO_2:6;
hence thesis by A2,XBOOLE_0:def 3;
end;
A' c= Cl A' by PRE_TOPC:48;
hence thesis by A4,XBOOLE_0:def 10;
end;
assume
A3: A' is closed;
let S be sequence of MA such that
A4: S is Cauchy;
reconsider S'=S as sequence of M by Th18;
S' is Cauchy by A4,Th19;then
A5: S' is convergent by A1,TBSP_1:def 6;
A6:the carrier of (M|A)=A' by A2,TOPMETR:def 2;
now let n be Element of NAT;
S.n in the carrier of (M|A);
hence S'.n in A' by A2,TOPMETR:def 2;
end;
then reconsider limS=lim S' as Point of (M|A) by A6,A3,A5,TOPMETR3:2;
take limS;
let r such that
A7:r>0;
consider n be Element of NAT such that
A8: for m be Element of NAT st m>=n holds
dist(S'.m,lim S')=n;
dist(S.m,limS) = dist(S'.m,lim S') by TOPMETR:def 1;
hence thesis by A8,A9;
end;
begin :: Countable compact spaces
definition let T be TopStruct;
attr T is countably_compact means :DEF9:
for F being Subset-Family of T st
F is_a_cover_of T & F is open & F is countable
ex G being Subset-Family of T
st G c= F & G is_a_cover_of T & G is finite;
end;
theorem Th21:
for T be TopStruct st T is compact holds T is countably_compact
proof
let T be TopStruct such that
A1: T is compact;
let F being Subset-Family of T such that
A2: F is_a_cover_of T & F is open & F is countable;
thus thesis by A1,A2,COMPTS_1:def 3;
end;
theorem Th22:
for T being non empty TopSpace holds
T is countably_compact iff
for F being Subset-Family of T st
F is centered & F is closed & F is countable
holds meet F <> {}
proof
let T be non empty TopSpace;
thus T is countably_compact implies
for F be Subset-Family of T st F is centered &F is closed &F is countable
holds meet F <> {}
proof assume
A1:T is countably_compact;
let F be Subset-Family of T such that
A2:F is centered & F is closed and
A3:F is countable;assume
A4:meet F = {};
F <> {} by A2,COMPTS_1:def 2;
then union COMPLEMENT(F) = (meet F)` by TOPS_2:12
.= [#] T by A4;
then COMPLEMENT(F) is_a_cover_of T & COMPLEMENT(F) is open &
COMPLEMENT(F) is countable by A3,TOPGEN_4:1,PRE_TOPC:def 8,A2,TOPS_2:16;
then consider G' be Subset-Family of T such that
A5:G' c= COMPLEMENT(F) & G' is_a_cover_of T and
A6:G' is finite by A1,DEF9;
A7:COMPLEMENT(G') c= F
proof
let x such that
A8:x in COMPLEMENT(G');
reconsider x'=x as Subset of T by A8;
x'` in G' by A8,SETFAM_1:def 8;
then x'`` in F by A5,SETFAM_1:def 8;
hence thesis;
end;
A8:G' <> {} by A5,TOPS_2:5;then
A9:meet COMPLEMENT(G') = (union G')` by TOPS_2:11
.= ([#] T) \ ([#] T) by A5,PRE_TOPC:def 8
.= {} by XBOOLE_1:37;
COMPLEMENT(G') <> {} & COMPLEMENT(G') is finite
by A6,A8,TOPS_2:10,13;
hence contradiction by A2,A7,A9,COMPTS_1:def 2;
end;
assume
A1:for F being Subset-Family of T st
F is centered & F is closed & F is countable holds meet F <> {};
let F be Subset-Family of T such that
A2: F is_a_cover_of T & F is open and
A3: F is countable;
A4:COMPLEMENT(F) is countable & COMPLEMENT(F) is closed &
F <> {} by A2,A3,TOPS_2:5,17,TOPGEN_4:1;
then meet COMPLEMENT(F) = (union F)` by TOPS_2:11
.= ([#] T) \ ([#] T) by A2,PRE_TOPC:def 8
.= {} by XBOOLE_1:37;
then COMPLEMENT(F) <> {} & not COMPLEMENT(F) is centered
by A1,A4,TOPS_2:10;
then consider G' being set such that
A5: G' <> {} & G' c= COMPLEMENT(F) and
A6: G' is finite & meet G' = {} by COMPTS_1:def 2;
reconsider G' as Subset-Family of T by A5,XBOOLE_1:1;
take F'=COMPLEMENT(G');
thus F' c= F
proof
let x such that
A7: x in F';
reconsider x'=x as Subset of T by A7;
x'` in G' by A7,SETFAM_1:def 8;
then x'`` in F by A5,SETFAM_1:def 8;
hence x in F;
end;
union F' = (meet G')` by A5,TOPS_2:12
.= [#] T by A6;
hence thesis by A6,TOPS_2:13,PRE_TOPC:def 8;
end;
theorem Th23:
for T being non empty TopSpace holds
T is countably_compact iff
for S be non-empty closed SetSequence of T st S is descending
holds meet S <> {}
proof
let T being non empty TopSpace;
thus T is countably_compact implies
for S be non-empty closed SetSequence of T st
S is descending holds meet S <> {}
proof assume
A1:T is countably_compact;
let S be non-empty closed SetSequence of T such that
A2: S is descending;
reconsider rngS=rng S as Subset-Family of T;
dom S=NAT by FUNCT_2:def 1;then
A4:rngS is centered & rngS is countable by A2,Th12,CARD_4:45;
now let D be Subset of T such that
A5: D in rngS;
consider x such that
A6: x in dom S & S.x=D by A5,FUNCT_1:def 5;
reconsider x as Element of NAT by A6;
S.x is closed by def6;
hence D is closed by A6;
end;
then rngS is closed by TOPS_2:def 2;
then meet rngS<>{} by A1,A4,Th22;
then consider x such that
A5: x in meet rngS by XBOOLE_0:def 1;
now let n be Element of NAT;
dom S=NAT by FUNCT_2:def 1;
then S.n in rngS by FUNCT_1:def 5;
hence x in S.n by A5,SETFAM_1:def 1;
end;
hence thesis by KURATO_2:6;
end;
assume
A1: for S be non-empty closed SetSequence of T st
S is descending holds meet S <> {};
now let F be Subset-Family of T such that
A2: F is centered & F is closed and
A3: F is countable;
A4: Card F <=` alef 0 by A3,CARD_4:def 1;
now per cases by A4,CARD_1:13;
suppose Card F = alef 0;
then NAT,F are_equipotent by CARD_1:21,38;
then consider s be Function such that
A5: s is one-to-one & dom s = NAT & rng s = F by WELLORD2:def 4;
reconsider s as SetSequence of T by A5,FUNCT_2:4;
consider R be SetSequence of T such that
A6: R is descending and
A7: F is centered implies R is non-empty and
F is open implies R is open and
A8: F is closed implies R is closed and
A9: for i holds R.i=meet{s.j where j is Element of NAT:j<=i}by A5,Th14;
meet R<>{} by A1,A2,A6,A7,A8;
then consider x such that
A10:x in meet R by XBOOLE_0:def 1;
A11:F is non empty by A5,RELAT_1:65;
now let y;
assume y in F;
then consider z be set such that
A12: z in dom s & s.z=y by A5,FUNCT_1:def 5;
reconsider z as Element of NAT by A12;
s.z in {s.j where j is Element of NAT:j<=z} &
R.z=meet {s.j where j is Element of NAT:j<=z} by A9;
then R.z c= s.z & x in R.z by A10,SETFAM_1:4,KURATO_2:6;
hence x in y by A12;
end;
hence meet F is non empty by A11,SETFAM_1:def 1;end;
suppose Card F <` alef 0;
then F is finite & F<>{} by CARD_4:2,A2,COMPTS_1:def 2;
hence meet F is non empty by A2,COMPTS_1:def 2;end;
end;
hence meet F<>{};
end;
hence thesis by Th22;
end;
theorem Th24:
for T being non empty TopSpace
for F be Subset-Family of T
for S be SetSequence of T st rng S c= F & S is non-empty
ex R be non-empty closed SetSequence of T st
R is descending &
( F is locally_finite & S is one-to-one implies meet R = {} ) &
for i ex Si be Subset-Family of T st
R.i = Cl union Si &
Si = {S.j where j is Element of NAT: j >= i}
proof
let T being non empty TopSpace;
let F be Subset-Family of T;
let S be SetSequence of T such that
A2: rng S c= F & S is non-empty;
defpred r[set,set] means
for i st i=$1 ex SS be Subset-Family of T st SS c= F &
SS = {S.j where j is Element of NAT:j >= i} & $2=Cl(union SS);
A3:for x st x in NAT ex y st y in bool(the carrier of T) & r[x,y]
proof
let x such that
A4: x in NAT;
reconsider x'=x as Element of NAT by A4;
set SS={S.j where j is Element of NAT:j >= x'};
SS c= bool(the carrier of T)
proof
let y such that
A5: y in SS;
ex j be Element of NAT st S.j=y & j>=x' by A5;
hence thesis;
end;
then reconsider SS as Subset-Family of T;
take Cl union SS;
SS c= F
proof
let y such that
A5: y in SS;
consider j be Element of NAT such that
A6: S.j=y & j>=x' by A5;
dom S=NAT by FUNCT_2:def 1;
then y in rng S by A6,FUNCT_1:def 5;
hence thesis by A2;
end;
hence thesis;
end;
consider R be SetSequence of T such that
A4: for x st x in NAT holds r[x,R.x] from FUNCT_2:sch 1(A3);
A5:now let n be set such that
B6: n in dom R;
reconsider n'=n as Element of NAT by B6;
consider SS be Subset-Family of T such that
SS c= F and
A6: SS = {S.j where j is Element of NAT:j>=n'} & R.n'=Cl(union SS) by A4;
dom S=NAT by FUNCT_2:def 1;then
A7:S.n'<>{} by A2,FUNCT_1:def 15;
S.n' in SS by A6;
then S.n' c= union SS by ZFMISC_1:92;
then S.n' c= Cl(S.n') & Cl(S.n') c= Cl(union SS) by PRE_TOPC:48,49;
then S.n' c= Cl (union SS) by XBOOLE_1:1;
hence R.n is non empty by A6,A7,XBOOLE_1:3;
end;
now let n;
reconsider n'=n as Element of NAT by ORDINAL1:def 13;
ex SS be Subset-Family of T st
SS c= F &
SS = {S.j where j is Element of NAT:j>=n'} & R.n'=Cl(union SS) by A4;
hence R.n is closed;
end;
then reconsider R as non-empty closed SetSequence of T
by A5,FUNCT_1:def 15,def6;
take R;
now let n be Element of NAT;
consider Sn be Subset-Family of T such that
Sn c= F and
A7: Sn = {S.j where j is Element of NAT:j>=n} and
A8: R.n=Cl(union Sn) by A4;
consider Sn1 be Subset-Family of T such that
Sn1 c= F and
A9: Sn1 = {S.j where j is Element of NAT:j>=n+1} and
A10: R.(n+1)=Cl(union Sn1) by A4;
Sn1 c= Sn
proof
let y such that
A11: y in Sn1;
consider j be Element of NAT such that
A12:y=S.j & j>=n+1 by A9,A11;
j>=n by A12,NAT_1:13;
hence thesis by A7,A12;
end;
then union Sn1 c= union Sn by ZFMISC_1:95;
hence R.(n+1) c= R.n by A8,A10,PRE_TOPC:49;
end;
hence R is descending by KURATO_2:def 5;
thus F is locally_finite & S is one-to-one implies meet R = {}
proof
assume
A6: F is locally_finite & S is one-to-one;
assume meet R <> {};
then consider x such that
A7: x in meet R by XBOOLE_0:def 1;
reconsider x as Point of T by A7;
A8:dom S=NAT by FUNCT_2:def 1;
then reconsider rngS=rng S as non empty Subset-Family of T by RELAT_1:65;
rng S is locally_finite by A2,A6,PCOMPS_1:12;
then consider W be Subset of T such that
A9: x in W & W is open and
A10:{ V where V is Subset of T: V in rngS & V meets W } is finite
by PCOMPS_1:def 2;
reconsider S as Function of NAT,rngS by A8,FUNCT_2:3;
reconsider S'=S" as Function;
reconsider S' as Function of rngS,NAT by A6,FUNCT_2:31;
deffunc s'(Element of rngS)=S'.$1;
set X={ V where V is Subset of T: V in rngS & V meets W };
set Y={s'(z) where z is Element of rngS:z in X};
A11:Y is finite from FRAENKEL:sch 21(A10);
Y c= NAT
proof
let y such that
A12:y in Y;
ex z be Element of rngS st
y =s'(z) & z in X by A12;
hence thesis;
end;
then reconsider Y as Subset of NAT;
consider n be Element of NAT such that
A12:for k be Element of NAT st k in Y holds k <= n by A11,STIRL2_1:66;
set n1=n+1;
consider Sn be Subset-Family of T such that
A13:Sn c= F and
A14:Sn ={S.j where j is Element of NAT:j>=n1} and
A15:R.n1=Cl(union Sn) by A4;
Sn is locally_finite by A6,A13,PCOMPS_1:12;
then Cl(union Sn)=union(clf Sn) & x in R.n1 by A7,KURATO_2:6,PCOMPS_1:23;
then consider CLF be set such that
A16:x in CLF & CLF in clf Sn by A15,TARSKI:def 4;
reconsider CLF as Subset of T by A16;
consider U be Subset of T such that
A17:CLF = Cl U & U in Sn by A16,PCOMPS_1:def 3;
consider j be Element of NAT such that
A18:U=S.j & j>=n1 by A14,A17;
S.j in rngS & S.j meets W by A9,A16,A17,A18,TOPS_1:39;
then S.j in X & (S").(S.j) = j by A6,FUNCT_2:32;
then j in Y;
then j <=n by A12;
hence thesis by A18,NAT_1:13;
end;
let i;
i in NAT by ORDINAL1:def 13;
then ex SS be Subset-Family of T st SS c= F &
SS = {S.j where j is Element of NAT:j >= i} & R.i=Cl(union SS) by A4;
hence thesis;
end;
LM1to2:
for T being non empty TopSpace st T is countably_compact
for F be Subset-Family of T st
F is locally_finite & F is with_non-empty_elements
holds F is finite
proof
let T be non empty TopSpace such that A0:T is countably_compact;
given F be Subset-Family of T such that
A1: F is locally_finite and
A2: F is with_non-empty_elements and
A3: F is infinite;
consider f be Function of NAT, F such that
A4: f is one-to-one by A3,DICKSON:3;
A5: rng f c= F;
reconsider f as SetSequence of T by A3,FUNCT_2:9;
now let x such that
A7: x in dom f;
f.x in rng f by A7,FUNCT_1:def 5;
hence f.x is non empty by A2,A5,SETFAM_1:def 9;
end;
then f is non-empty by FUNCT_1:def 15;
then ex R be non-empty closed SetSequence of T st
R is descending &
( F is locally_finite & f is one-to-one implies meet R = {})&
for i ex fi be Subset-Family of T st
R.i = Cl union fi & fi = {f.j where j is Element of NAT: j >= i}
by Th24,A5;
hence thesis by A0,A1,A4,Th23;
end;
LM2to3:
for T be non empty TopSpace st
for F be Subset-Family of T st
F is locally_finite & F is with_non-empty_elements holds F is finite
for F be Subset-Family of T st F is locally_finite &
for A be Subset of T st A in F holds Card A = 1
holds F is finite
proof
let T be non empty TopSpace such that
A1: for F be Subset-Family of T st
F is locally_finite & F is with_non-empty_elements holds F is finite;
let F be Subset-Family of T such that
A2: F is locally_finite and
A3: for A be Subset of T st A in F holds Card A = 1;
not {}T in F by A3,CARD_1:78;
then F is with_non-empty_elements by SETFAM_1:def 9;
hence thesis by A1,A2;
end;
LM3to4:
for T be non empty TopSpace st
for F be Subset-Family of T st F is locally_finite &
for A be Subset of T st A in F holds Card A = 1
holds F is finite
for A be Subset of T st A is infinite holds Der A is non empty
proof
let T be non empty TopSpace such that
A1: for F be Subset-Family of T st F is locally_finite &
for A be Subset of T st A in F holds Card A = 1 holds F is finite;
let A be Subset of T such that A2:A is infinite;
assume
A3: Der A is empty;
set F={{x} where x is Element of T: x in A};
reconsider F as Subset-Family of T by RELSET_2:16;
A4:F is locally_finite
proof
let x be Point of T;
consider U be open Subset of T such that
A5: x in U and
A6: for y being Point of T st y in A /\ U holds x = y by A3,TOPGEN_1:19;
take U;
set M={ V where V is Subset of T: V in F & V meets U};
M c= {{x}}
proof
let v be set such that
A7: v in M;
consider V be Subset of T such that
A8: v=V & V in F & V meets U by A7;
consider y be Point of T such that
A9: V = {y} & y in A by A8;
y in U by A8,A9,ZFMISC_1:56;
then y in A/\U & {x} in {{x}} by TARSKI:def 1,A9,XBOOLE_0:def 3;
hence thesis by A6,A8,A9;
end;
hence thesis by A5,FINSET_1:13;
end;
now let a be Subset of T such that
A5: a in F;
ex y be Point of T st a={y} & y in A by A5;
hence Card a = 1 by CARD_1:50;
end;then
A5: F is finite by A1,A4;
deffunc P(set)=meet $1;
set PP={P(y) where y is Element of bool(the carrier of T):y in F};
A6: PP is finite from FRAENKEL:sch 21(A5);
A c= PP
proof
let y such that
A7: y in A;
reconsider y'=y as Point of T by A7;
{y'} in F & {y'} is Subset of T by A7;
then P({y'}) in PP;
hence thesis by SETFAM_1:11;
end;
hence thesis by A2,A6,FINSET_1:13;
end;
theorem Th25:
for F be Function st dom F is infinite & rng F is finite
ex x st x in rng F & F"{x} is infinite
proof
let F be Function such that
A1: dom F is infinite & rng F is finite;
assume
A2: for x st x in rng F holds F"{x} is finite;
deffunc f(set)=F"{$1};
consider g be Function such that
A3: dom g = rng F & for x st x in rng F holds g.x = f(x) from FUNCT_1:sch 3;
now let x such that
A4: x in dom g;
g.x=F"{x} by A3,A4;
hence g.x is finite by A2,A3,A4;
end;then
A4: Union g is finite by A1,A3,CARD_4:63;
A5:dom F c= Union g
proof
let x such that
A6: x in dom F;
F.x in {F.x} & F.x in rng F by A6,TARSKI:def 1,FUNCT_1:def 5;
then x in F"{F.x} & g.(F.x)=F"{F.x} & g.(F.x) in rng g
by A3,A6,FUNCT_1:def 5,def 13;
then x in union rng g by TARSKI:def 4;
hence thesis by CARD_3:def 4;
end;
Union g c= dom F
proof
let x such that
A6: x in Union g;
x in union rng g by A6,CARD_3:def 4;
then consider y such that
A7: x in y & y in rng g by TARSKI:def 4;
consider z be set such that
A8: z in dom g & y=g.z by A7,FUNCT_1:def 5;
y=F"{z} by A3,A8;
hence thesis by A7,FUNCT_1:def 13;
end;
hence thesis by A1,A4,A5,XBOOLE_0:def 10;
end;
theorem Th26:
for X be non empty set, F be SetSequence of X st F is descending
for S be Function of NAT,X st for n holds S.n in F.n holds
rng S is finite implies meet F is non empty
proof
let X be non empty set, F be SetSequence of X such that
A1: F is descending;
let S be Function of NAT,X such that
A2: for n holds S.n in F.n;
assume
A3: rng S is finite;
dom S=NAT & NAT is infinite by FUNCT_2:def 1,CARD_4:15;
then consider x such that
A5: x in rng S & S"{x} is infinite by A3,Th25;
now let n be Element of NAT;
ex i st x in F.i & i >= n
proof
assume
A6: for i st x in F.i holds i=n;
i in NAT by ORDINAL1:def 13;
then F.i c= F.n by A1,A6,KURATO_2:22;
hence x in F.n by A6;
end;
hence thesis by KURATO_2:6;
end;
LM5to1:
for T be being_T1 non empty TopSpace st
for A be Subset of T st A is infinite countable holds Der A is non empty
holds T is countably_compact
proof
let T be being_T1 non empty TopSpace such that
A1: for A be Subset of T st A is infinite countable holds
Der A is non empty;
assume not T is countably_compact;
then consider S be non-empty closed SetSequence of T such that
A2: S is descending & meet S = {} by Th23;
defpred P[set,set] means $2 in S.$1;
A3:for x st x in NAT ex y st y in the carrier of T & P[x,y]
proof
let x such that
A4: x in NAT;
reconsider x'=x as Element of NAT by A4;
dom S=NAT by FUNCT_2:def 1;
then S.x' is non empty by FUNCT_1:def 15;
then consider y such that
A5: y in S.x' by XBOOLE_0:def 1;
take y;
thus thesis by A5;
end;
consider F be sequence of T such that
A4: for x st x in NAT holds P[x,F.x] from FUNCT_2:sch 1(A3);
reconsider rngF=rng F as Subset of T;
now let n;
n in NAT by ORDINAL1:def 13;
hence F.n in S.n by A4;
end;then
A5:rng F is infinite by A2,Th26;
dom F=NAT by FUNCT_2:def 1;
then rng F is countable by CARD_4:45;
then Der rngF is non empty by A1,A5;
then consider p be set such that
A6: p in Der rngF by XBOOLE_0:def 1;
reconsider p as Point of T by A6;
consider n be Element of NAT such that
A7: not p in S.n by A2,KURATO_2:6;
deffunc f(set)=F.$1;
set F1n={f(i) where i is Element of NAT:i in n+1};
A8:n+1 is finite;
A9:F1n is finite from FRAENKEL:sch 21(A8);
F1n c= the carrier of T
proof
let x such that
A10:x in F1n;
ex i be Element of NAT st x=F.i & i in n+1 by A10;
hence thesis;
end;
then reconsider F1n as Subset of T;
set U=((S.n)`)\(F1n\{p});
reconsider U as Subset of T;
F1n\{p}c=F1n by XBOOLE_1:36;
then F1n\{p} is finite & (S.n) is closed by A9,FINSET_1:13,def6;
then F1n\{p} is closed & (S.n)` is open by YELLOW13:1,TOPS_1:29;then
A10:U is open by FRECHET:4;
p in {p} by TARSKI:def 1;
then not p in F1n\{p} & p in (S.n)` by A7,XBOOLE_0:def 4;
then p in U by XBOOLE_0:def 4;
then consider q be Point of T such that
A11: q in rngF /\ U & q <> p by A6,A10,TOPGEN_1:19;
q in rngF by A11,XBOOLE_0:def 3;
then consider i be set such that
A12: i in dom F & F.i=q by FUNCT_1:def 5;
reconsider i as Element of NAT by A12;
per cases;
suppose i<=n;
then i < n+1 by NAT_1:13;
then i in n+1 by EULER_1:1;
then q in F1n by A12;
then q in F1n\{p} by A11,ZFMISC_1:64;
then not q in U by XBOOLE_0:def 4;
hence contradiction by A11,XBOOLE_0:def 3;end;
suppose i>n;
then q in S.i & S.i c= S.n by A2,A4,A12,KURATO_2:22;
then not q in (S.n)` by XBOOLE_0:def 4;
then not q in U by XBOOLE_0:def 4;
hence contradiction by A11,XBOOLE_0:def 3;end;
end;
LM3to1:
for T being non empty TopSpace st
for F be Subset-Family of T st F is locally_finite &
for A be Subset of T st A in F holds Card A = 1
holds F is finite
holds T is countably_compact
proof
let T being non empty TopSpace such that
A1: for F be Subset-Family of T st F is locally_finite &
for A be Subset of T st A in F holds Card A = 1
holds F is finite;
assume not T is countably_compact;
then consider S be non-empty closed SetSequence of T such that
A2: S is descending & meet S = {} by Th23;
defpred P[set,set] means $2 in S.$1;
A3:for x st x in NAT ex y st y in the carrier of T & P[x,y]
proof
let x such that
A4: x in NAT;
reconsider x'=x as Element of NAT by A4;
dom S=NAT by FUNCT_2:def 1;
then S.x' is non empty by FUNCT_1:def 15;
then consider y such that
A5: y in S.x' by XBOOLE_0:def 1;
take y;
thus thesis by A5;
end;
consider F be sequence of T such that
A4: for x st x in NAT holds P[x,F.x] from FUNCT_2:sch 1(A3);
reconsider rngF=rng F as Subset of T;
now let n;
n in NAT by ORDINAL1:def 13;
hence F.n in S.n by A4;
end;then
A5:rng F is infinite by A2,Th26;
reconsider rngF=rng F as Subset of T;
set A={{x} where x is Element of T: x in rngF};
reconsider A as Subset-Family of T by RELSET_2:16;
A6:A is locally_finite
proof
let x be Point of T;
consider i be Element of NAT such that
A7: not x in S.i by A2,KURATO_2:6;
take Si'=(S.i)`;
S.i is closed by def6;
hence x in Si' & Si' is open by A7,TOPS_1:29,SUBSET_1:50;
deffunc f(set)={F.$1};
A8:i is finite;
set SI={f(j) where j is Element of NAT:j in i};
A9:SI is finite from FRAENKEL:sch 21(A8);
set meetS={ V where V is Subset of T: V in A & V meets Si' };
meetS c= SI
proof
let v be set such that
A10: v in meetS;
consider V be Subset of T such that
A11:V=v & V in A & V meets Si' by A10;
consider y be Point of T such that
A12:V={y} & y in rng F by A11;
consider z be set such that
A13:z in dom F & y=F.z by A12,FUNCT_1:def 5;
reconsider z as Element of NAT by A13;
z in i
proof
assume not z in i;
then z>=i by EULER_1:1;
then y in S.z & S.z c= S.i by A2,A4,A13,KURATO_2:22;
then y in S.i & y in Si' by A11,A12,ZFMISC_1:56;
hence thesis by XBOOLE_0:def 4;
end;
hence thesis by A11,A12,A13;
end;
hence meetS is finite by A9,FINSET_1:13;
end;
now let a be Subset of T such that
A7: a in A;
ex y be Point of T st a={y} & y in rngF by A7;
hence Card a = 1 by CARD_1:50;
end;then
A7: A is finite by A1,A6;
deffunc P(set)=meet $1;
set PP={P(y) where y is Element of bool(the carrier of T):y in A};
A8:PP is finite from FRAENKEL:sch 21(A7);
rngF c= PP
proof
let y such that
A9: y in rngF;
reconsider y'=y as Point of T by A9;
{y'} in A & {y'} is Subset of T by A9;
then P({y'}) in PP;
hence thesis by SETFAM_1:11;
end;
hence thesis by A5,A8,FINSET_1:13;
end;
theorem Th27:
for T be non empty TopSpace holds
T is countably_compact iff
for F be Subset-Family of T st
F is locally_finite & F is with_non-empty_elements
holds F is finite
proof
let T be non empty TopSpace;
thus T is countably_compact implies
for F be Subset-Family of T st
F is locally_finite & F is with_non-empty_elements
holds F is finite by LM1to2;
assume for F be Subset-Family of T st
F is locally_finite & F is with_non-empty_elements
holds F is finite;
then for F be Subset-Family of T st
F is locally_finite &
for A be Subset of T st A in F holds Card A = 1
holds F is finite by LM2to3;
hence thesis by LM3to1;
end;
theorem Th28:
for T be non empty TopSpace holds
T is countably_compact iff
for F be Subset-Family of T st F is locally_finite &
for A be Subset of T st A in F holds Card A = 1
holds F is finite
proof
let T be non empty TopSpace;
thus T is countably_compact implies
for F be Subset-Family of T st F is locally_finite &
for A be Subset of T st A in F holds Card A=1
holds F is finite
proof
assume T is countably_compact;
then for F be Subset-Family of T st
F is locally_finite & F is with_non-empty_elements
holds F is finite by Th27;
hence thesis by LM2to3;
end;
thus thesis by LM3to1;
end;
theorem Th29:
for T be being_T1 non empty TopSpace holds
T is countably_compact iff
for A be Subset of T st A is infinite holds Der A is non empty
proof
let T be being_T1 non empty TopSpace;
thus T is countably_compact implies
for A be Subset of T st A is infinite holds Der A is non empty
proof
assume T is countably_compact;
then for F be Subset-Family of T st F is locally_finite &
for A be Subset of T st A in F holds Card A=1
holds F is finite by Th28;
hence thesis by LM3to4;
end;
assume for A be Subset of T st A is infinite holds Der A is non empty;
then for A be Subset of T st A is infinite countable holds
Der A is non empty;
hence thesis by LM5to1;
end;
theorem
for T be being_T1 non empty TopSpace holds
T is countably_compact iff
for A be Subset of T st A is infinite countable holds
Der A is non empty by Th29,LM5to1;
scheme Th39{X()->non empty set,P[set,set]}:
ex A be Subset of X() st
( for x,y be Element of X() st x in A & y in A & x <> y holds P[x,y] ) &
for x be Element of X() ex y be Element of X() st y in A & not P[x,y]
provided
A1:for x,y be Element of X() holds P[x,y] iff P[y,x]
and
A2:for x be Element of X() holds not P[x,x]
proof
set bX=bool X();
consider R be Relation such that
A3: R well_orders X() by WELLORD2:26;
R/\[:X(),X():]c=[:X(),X():] & R/\[:X(),X():]=R|_2 X()
by WELLORD1:def 6,XBOOLE_1:17;
then reconsider R2=R |_2 X() as Relation of X() by RELSET_1:def 1;
reconsider RS=RelStr(#X(),R2#) as non empty RelStr;
A4:R2 well_orders X() & field R2 = X() by A3,PCOMPS_2:5; then
A5:R2 is_well_founded_in X() & R2 is well-ordering
by WELLORD1:def 5,WELLORD1:8;then
A6:RS is well_founded by WELLFND1:def 2;
set cRS=the carrier of RS;
set IRS=the InternalRel of RS;
defpred H[set,set,set] means
for p be Element of X(), f be PartFunc of cRS,bX st
$1=p & $2=f holds
( (for q be Element of X() st q in union(rng f) holds P[p,q])
implies $3=union (rng f) \/ {p} ) &
( (ex q be Element of X() st q in union (rng f) & not P[p,q])
implies $3=union (rng f) );
A7:for x,y st x in cRS & y in PFuncs(cRS, bX)
ex z be set st z in bX & H[x,y,z]
proof
let x,y such that
A8: x in cRS & y in PFuncs(cRS, bX);
reconsider p=x as Element of X() by A8;
reconsider f=y as PartFunc of cRS,bX by A8,PARTFUN1:120;
per cases;
suppose A9:for q be Element of X() st q in union(rng f) holds P[p,q];
take U=union (rng f) \/ {p};
thus thesis by A9;end;
suppose A9:ex q be Element of X() st q in union (rng f) & not P[p,q];
take U=union (rng f);
thus thesis by A9;end;
end;
consider h be Function of [:cRS,PFuncs(cRS, bX):],bX such that
A8:for x,y st x in cRS & y in PFuncs(cRS, bX) holds H[x,y,h.(x,y)]
from BINOP_1:sch 1(A7);
consider f be Function of cRS, bX such that
A9:f is_recursively_expressed_by h by A6,WELLFND1:12;
reconsider rngf=rng f as Subset of bX;
take A=union rngf;
defpred S[set] means
f.$1 c= (IRS-Seg $1)\/{$1} &
($1 in f.$1 implies
for r be Element of X() st r in union(rng (f|IRS-Seg $1)) holds P[$1,r])&
(not $1 in f.$1 implies
ex r be Element of X() st r in union(rng (f|IRS-Seg $1)) & not P[$1,r]);
A10:for x be Element of RS st
for y be Element of RS st y <> x & [y,x] in IRS holds S[y] holds S[x]
proof
let x be Element of RS such that
A11: for y be Element of RS st y <> x & [y,x] in IRS holds S[y];
set fIx=f|IRS-Seg x;
A12:union rng fIx c= IRS-Seg x
proof
let y be set such that
A13: y in union rng fIx;
consider z be set such that
A14: y in z & z in rng fIx by A13,TARSKI:def 4;
consider t be set such that
A15: t in dom fIx & fIx.t=z by A14,FUNCT_1:def 5;
A16:t in IRS-Seg x & IRS-Seg x c= cRS by A15,RELAT_1:86,WELLFND1:4;
reconsider t as Element of RS by A15;
t<>x & [t,x] in IRS by A16,WELLORD1:def 1;
then f.t c= (IRS-Seg t)\/{t} & fIx.t=f.t & IRS-Seg(t)c=IRS-Seg(x) &
{t} c= IRS-Seg(x)
by A4,A5,A11,A15,A16,FUNCT_1:70,WELLORD1:37,ZFMISC_1:37;
then y in (IRS-Seg t)\/{t} & (IRS-Seg t)\/{t} c= IRS-Seg(x)
by A14,A15,XBOOLE_1:8;
hence thesis;
end;
A13:f.x=h.(x,fIx)&fIx in PFuncs(cRS,bX) by A9,WELLFND1:def 5,PARTFUN1:119;
per cases;
suppose
A14: for q be Element of X() st q in union(rng fIx) holds P[x,q];then
A15: f.x=union(rng fIx)\/{x} by A8,A13;
hence f.x c= IRS-Seg x\/{x} by A12,XBOOLE_1:9;
thus x in f.x implies for r be Element of X() st
r in union(rng (f|IRS-Seg x)) holds P[x,r] by A14;
assume A16:not x in f.x;
x in {x} by TARSKI:def 1;
hence thesis by A15,A16,XBOOLE_0:def 2;end;
suppose
A14: ex q be Element of X() st q in union (rng fIx) & not P[x,q];then
A15: f.x c= IRS-Seg x & IRS-Seg x c= IRS-Seg x\/{x}
by A8,A12,A13,XBOOLE_1:7;
hence f.x c= IRS-Seg x\/{x} by XBOOLE_1:1;
thus thesis by A14,A15,WELLORD1:def 1;end;
end;
A11:for x being Element of RS holds S[x] from WELLFND1:sch 3(A10,A6);
thus for x,y be Element of X() st x in A & y in A & x <> y holds P[x,y]
proof
A12:now let x be Element of X() such that A13:x in A;
consider y such that
A14: x in y & y in rng f by A13,TARSKI:def 4;
consider z be set such that
A15: z in dom f & f.z=y by A14,FUNCT_1:def 5;
reconsider z as Element of RS by A15;
defpred T[set] means x in f.$1;
A16: T[z] by A14,A15;
consider p being Element of RS such that
A17: T[p] and
A18: not ex q being Element of RS st
p <> q & T[q] & [q,p] in IRS from WELLFND1:sch 2(A16,A6);
p = x
proof
assume
A19: p<>x;
set fIp=f|IRS-Seg p;
A20:f.p=h.(p,fIp) & fIp in PFuncs(cRS, bX)
by A9,WELLFND1:def 5,PARTFUN1:119;
now per cases;
suppose for q be Element of X() st q in union(rng fIp)
holds P[p,q];
then f.p=union(rng fIp)\/{p} & not x in {p}
by A8,A19,A20,TARSKI:def 1;
hence x in union(rng fIp) by A17,XBOOLE_0:def 2;end;
suppose ex q be Element of X() st
q in union (rng fIp) & not P[p,q];
hence x in union(rng fIp) by A8,A17,A20;end;end;
then consider y' be set such that
A21: x in y' & y' in rng fIp by TARSKI:def 4;
consider z' be set such that
A22: z' in dom fIp & fIp.z'=y' by A21,FUNCT_1:def 5;
reconsider z' as Point of RS by A22;
z' in IRS-Seg p & f.z'=y' by A22,RELAT_1:86,FUNCT_1:70;
then z'<> p & [z',p] in IRS & T[z'] by A21,WELLORD1:def 1;
hence thesis by A18;
end;
hence x in f.x by A17;
end;
A13:now let x,y be Element of X() such that
A14: x in A & y in A & x <> y & [x,y] in IRS;
set fIy=f|IRS-Seg y;
dom f = cRS & x in IRS-Seg y by A14,FUNCT_2:def 1,WELLORD1:def 1;
then x in dom fIy by RELAT_1:86;
then x in f.x & fIy.x in rng fIy & fIy.x=f.x
by FUNCT_1:def 5,70,A12,A14;
then y in f.y & x in union(rng fIy) by A12,A14,TARSKI:def 4;
then P[y,x] by A11;
hence P[x,y] by A1;
end;
let x,y be Element of X() such that
A14:x in A & y in A & x <> y;
R2 well_orders X() by A3,PCOMPS_2:5;
then R2 is_connected_in X() by WELLORD1:def 5;
then [x,y] in IRS or [y,x] in IRS by A14,RELAT_2:def 6;
then P[x,y] or P[y,x] by A13,A14;
hence thesis by A1;
end;
let x be Element of X();
per cases;
suppose
A12: x in A;
take y=x;
thus thesis by A2,A12;end;
suppose
A12: not x in A;
not x in f.x
proof
assume
A13: x in f.x;
dom f=cRS by FUNCT_2:def 1;
then f.x in rng f by FUNCT_1:def 5;
hence thesis by A12,A13,TARSKI:def 4;
end;
then consider r be Element of X() such that
A13: r in union(rng (f|IRS-Seg x)) & not P[x,r] by A11;
take r;
rng (f|IRS-Seg x) c= rng f by RELAT_1:99;
then union rng (f|IRS-Seg x) c= A by ZFMISC_1:95;
hence thesis by A13;end;
end;
theorem Th31:
for M be Reflexive symmetric non empty MetrStruct
for r be Real st r > 0
ex A be Subset of M st
(for p,q be Point of M st p <> q & p in A & q in A holds
dist(p,q) >= r) &
for p be Point of M ex q be Point of M st q in A & p in Ball(q,r)
proof
let M be Reflexive symmetric non empty MetrStruct;
let r be Real such that
A1: r > 0;
defpred P[set,set] means
for p,q be Point of M st p=$1 & q=$2 holds dist(p,q)>=r;
set cM=the carrier of M;
A2: for x,y be Element of cM holds P[x,y] iff P[y,x];
A3: for x be Element of cM holds not P[x,x]
proof
let x be Element of cM;
dist(x,x)=0 by METRIC_1:1;
hence thesis by A1;
end;
consider A be Subset of cM such that
A4: for x,y be Element of cM st x in A & y in A & x <> y holds P[x,y] and
A5: for x be Element of cM ex y be Element of cM st y in A & not P[x,y]
from Th39(A2,A3);
take A;
thus for p,q be Point of M st p <> q & p in A & q in A holds
dist(p,q) >= r by A4;
let p be Point of M;
consider y be Element of cM such that
A6: y in A & not P[p,y] by A5;
take y;
thus thesis by A6,METRIC_1:12;
end;
theorem Th32:
for M be Reflexive symmetric triangle non empty MetrStruct holds
M is totally_bounded iff
for r be Real,A be Subset of M st r>0 &
for p,q be Point of M st p <> q & p in A & q in A holds
dist(p,q) >= r
holds A is finite
proof
let M be Reflexive symmetric triangle non empty MetrStruct;
thus M is totally_bounded implies
for r be Real,A be Subset of M st r>0 &
for p,q be Point of M st p <> q & p in A & q in A holds dist(p,q) >= r
holds A is finite
proof
assume
A1:M is totally_bounded;
let r be Real,A be Subset of M such that
A2: r>0 and
A3:for p,q be Point of M st p <> q & p in A & q in A holds dist(p,q)>=r;
r/2>0 by A2,XREAL_1:217;
then consider G be Subset-Family of M such that
A4: G is finite and
A5: the carrier of M = union G and
A6: for C be Subset of M st C in G ex w be Point of M st C = Ball(w,r/2)
by A1,TBSP_1:def 1;
defpred f[set,set] means $1 in $2 & $2 in G;
A7:for x st x in A ex y st y in bool(the carrier of M) & f[x,y]
proof
let x such that
A8: x in A;
consider y such that
A9: x in y & y in G by A5,A8,TARSKI:def 4;
reconsider y as Subset of M by A9;
take y;
thus thesis by A9;
end;
consider F be Function of A,bool(the carrier of M) such that
A8: for x st x in A holds f[x,F.x] from FUNCT_2:sch 1(A7);
now let x1,x2 be set such that
A9: x1 in A & x2 in A & F.x1 = F.x2;
reconsider p1=x1,p2=x2 as Point of M by A9;
F.x1 in G by A8,A9;
then consider w be Point of M such that
A10: F.x1 = Ball(w,r/2) by A6;
p1 in Ball(w,r/2) & p2 in Ball(w,r/2) by A8,A9,A10;
then dist(p1,w)0 &
for p,q be Point of M st p <> q & p in A & q in A holds dist(p,q) >= r
holds A is finite;
let r such that
A2: r>0;
consider A be Subset of M such that
A3: for p,q be Point of M st p <> q & p in A & q in A holds dist(p,q) >= r and
A4: for p be Point of M ex q be Point of M st q in A& p in Ball(q,r)
by A2,Th31;
A5: A is finite by A1,A2,A3;
deffunc B(Point of M)=Ball($1,r);
set BA={B(p) where p is Point of M:p in A};
A6:BA is finite from FRAENKEL:sch 21(A5);
BA c= bool the carrier of M
proof
let x such that
A7: x in BA;
ex p be Point of M st x = B(p) & p in A by A7;
hence thesis;
end;
then reconsider BA as Subset-Family of M;
take BA;
union BA = the carrier of M
proof
the carrier of M c= union BA
proof
let x such that
A7: x in the carrier of M;
reconsider p=x as Point of M by A7;
consider q be Point of M such that
A8: q in A & p in B(q) by A4;
B(q) in BA by A8;
hence thesis by A8,TARSKI:def 4;
end;
hence thesis by XBOOLE_0:def 10;
end;
hence BA is finite & union BA = the carrier of M by A6;
let C be Subset of M such that
A7: C in BA;
ex p be Point of M st C=B(p) & p in A by A7;
hence thesis;
end;
LocallyFinite:
for M be Reflexive symmetric triangle non empty MetrStruct
for r be Real, A be Subset of M st
r>0 & for p,q be Point of M st p <> q & p in A & q in A
holds dist(p,q) >= r
for F be Subset-Family of TopSpaceMetr M st
F={{x} where x is Element of TopSpaceMetr M: x in A}
holds F is locally_finite
proof
let M be Reflexive symmetric triangle non empty MetrStruct;
set T=TopSpaceMetr M;
let r be Real, A be Subset of M such that
A1: r>0 and
A2: for p,q be Point of M st p <> q & p in A & q in A holds dist(p,q) >= r;
let F be Subset-Family of T such that
A3: F={{x} where x is Element of T: x in A};
let x be Point of T;
reconsider x'=x as Point of M;
reconsider B=Ball(x',r/2) as Subset of T;
take B;
B in Family_open_set M & dist(x',x')=0 & r/2>0
by A1,PCOMPS_1:33,METRIC_1:1,XREAL_1:217;
hence x in B & B is open by PRE_TOPC:def 5,METRIC_1:12;
set VV={ V where V is Subset of T: V in F & V meets B};
per cases;
suppose A6:for p be Point of M st p in A holds dist(p,x') >= r/2;
VV is empty
proof
assume VV is non empty;
then consider v be set such that
A7: v in VV by XBOOLE_0:def 1;
consider V be Subset of T such that
A8: v=V & V in F & V meets B by A7;
consider y be Point of T such that
A9: V = {y} & y in A by A3,A8;
reconsider y as Point of M;
y in B by A8,A9,ZFMISC_1:56;
then dist(x',y)0 and
A3: for p,q be Point of M st p <> q & p in A & q in A holds dist(p,q) >= r and
A4: A is infinite by Th32;
reconsider A as Subset of T;
set F={{x} where x is Element of T: x in A};
reconsider F as Subset-Family of T by RELSET_2:16;
A5:F is locally_finite by A2,A3,LocallyFinite;
now let a be Subset of T such that
A6: a in F;
ex y be Point of T st a={y} & y in A by A6;
hence Card a = 1 by CARD_1:50;
end;then
A6: F is finite by A1,A5,Th28;
deffunc P(set)=meet $1;
set PP={P(y) where y is Subset of T:y in F};
A7: PP is finite from FRAENKEL:sch 21(A6);
A c= PP
proof
let y such that
A8: y in A;
reconsider y'=y as Point of T by A8;
{y'} in F & {y'} is Subset of T by A8;
then P({y'}) in PP;
hence thesis by SETFAM_1:11;
end;
hence thesis by A4,A7,FINSET_1:13;
end;
theorem Th34:
for M be non empty MetrSpace st M is totally_bounded
holds TopSpaceMetr M is second-countable
proof
let M be non empty MetrSpace such that
A1:M is totally_bounded;
set T=TopSpaceMetr M;
defpred F[set,set] means
for i st i=$1 for G be Subset-Family of T st $2=G holds
G is finite & the carrier of M = union G &
for C be Subset of M st C in G ex w be Point of M st C = Ball(w,1/(i+1));
A2: for x st x in NAT ex y st y in bool bool(the carrier of T) & F[x,y]
proof
let x such that
A3: x in NAT;
reconsider i=x as Element of NAT by A3;
1/(i+1)>0 by XREAL_1:141;
then consider G be Subset-Family of T such that
A4: G is finite & the carrier of M = union G &
for C be Subset of M st C in G ex w be Point of M st C=Ball(w,1/(i+1))
by A1,TBSP_1:def 1;
take G;
thus thesis by A4;
end;
consider f be Function of NAT,bool bool(the carrier of T) such that
A3: for x st x in NAT holds F[x,f.x] from FUNCT_2:sch 1(A2);
A4: dom f=NAT by FUNCT_2:def 1;
set U = Union f;
A5:U c= the topology of T
proof
let x such that
A6: x in U;
x in union rng f by A6,CARD_3:def 4;
then consider y such that
A7: x in y & y in rng f by TARSKI:def 4;
consider z be set such that
A8: z in dom f & f.z=y by A7,FUNCT_1:def 5;
reconsider z as Element of NAT by A8;
reconsider fz=f.z as Subset-Family of T;
reconsider X=x as Subset of T by A7;
consider w be Point of M such that
A9: X=Ball(w,1/(z+1)) by A3,A7,A8;
thus thesis by A9,PCOMPS_1:33;
end;
for A be Subset of T st A is open
for p be Point of T st p in A
ex a be Subset of T st a in U & p in a & a c= A
proof
let A be Subset of T such that
A6: A is open;
let p be Point of T such that
A7: p in A;
reconsider p'=p as Point of M;
consider r be real number such that
A8: r>0 & Ball(p',r) c= A by A6,A7,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
r/2 >0 by A8,XREAL_1:217;
then consider n be Element of NAT such that
A9: n>0 & 1/n{} by A8,A6,A9,ZFMISC_1:64;
hence thesis by A9;
end;
thus RNG is_a_cover_of T
proof
the carrier of T c= union RNG
proof
let y such that
A8: y in the carrier of T;
reconsider q=y as Point of T by A8;
consider W be Subset of T such that
A9: q in W & W in F by A2,PCOMPS_1:5;
W is open by A3,A9,TOPS_2:def 1;
then consider U be Subset of T such that
A10: U in B & q in U & U c= W by A9,YELLOW_9:31;
A11:p.U in rng p by A7,A10,FUNCT_1:def 5;
then reconsider pU=p.U as Subset of T;
A12: pU in F & U c= pU by A6,A9,A10;
then pU in RNG by A10,A11,ZFMISC_1:64;
hence thesis by A10,A12,TARSKI:def 4;
end;
then [#]T=union RNG by XBOOLE_0:def 10;
hence thesis by PRE_TOPC:def 8;
end;
Card rng p c= Card B & Card B c= omega
by CARD_4:def 1,CARD_1:83,A4,A7,CARD_2:80;
then Card rng p c= alef 0 by XBOOLE_1:1,CARD_1:83;
then rng p is countable by CARD_4:def 1;
hence thesis by CARD_4:49;
end;
begin :: The main theorem
theorem Th36:
for M be non empty MetrSpace holds
TopSpaceMetr M is compact iff TopSpaceMetr M is countably_compact
proof
let M be non empty MetrSpace;
set T=TopSpaceMetr M;
thus T is compact implies T is countably_compact by Th21;
assume
A1: T is countably_compact;
then M is totally_bounded by Th33;then
A2: T is second-countable by Th34;
let F be Subset-Family of T such that
A3: F is_a_cover_of T & F is open;
consider G be Subset-Family of T such that
A4: G c= F & G is_a_cover_of T & G is countable by A2,A3,Th35;
G is open by A3,A4,TOPS_2:18;
then consider H be Subset-Family of T such that
A5: H c= G & H is_a_cover_of T & H is finite by A1,A4,DEF9;
H c= F by A4,A5,XBOOLE_1:1;
hence thesis by A5;
end;
theorem Th37:
for X be set, F be Subset-Family of X st F is finite
for A be Subset of X st A is infinite & A c= union F
ex Y be Subset of X st Y in F & Y /\ A is infinite
proof
let X be set, F be Subset-Family of X such that
A1: F is finite;
let A be Subset of X such that
A2: A is infinite & A c= union F;
set I=INTERSECTION (F,{A});
Card [:F,{A}:] =Card F by CARD_2:13;
then Card I<=` Card F by TOPGEN_4:25;then
A3: I is finite by A1,CARD_2:68;
defpred P[set,set] means $1 in $2;
A4:for x st x in A ex y st y in I & P[x,y]
proof
let x such that
A5: x in A;
consider y such that
A6: x in y & y in F by A2,A5,TARSKI:def 4;
take y/\A;
A in {A} by TARSKI:def 1;
hence thesis by A5,A6,SETFAM_1:def 5,XBOOLE_0:def 3;
end;
consider p be Function of A,I such that
A5: for x st x in A holds P[x,p.x] from FUNCT_2:sch 1(A4);
consider x such that
A6: x in A by A2,XBOOLE_0:def 1;
consider y such that
A7: y in I & P[x,y] by A4,A6;
dom p=A & rng p is finite by A3,A7,FUNCT_2:def 1,FINSET_1:13;
then consider t be set such that
A8: t in rng p & p"{t} is infinite by A2,Th25;
consider Y,Z be set such that
A9: Y in F & Z in {A} & t=Y/\Z by A8,SETFAM_1:def 5;
reconsider Y as Subset of X by A9;
take Y;
A10: Z = A by A9,TARSKI:def 1;
p"{t} c= Y/\A
proof
let z be set such that
A11: z in p"{t};
z in dom p & p.z in {t} by A11,FUNCT_1:def 13;
then z in A & p.z=t by TARSKI:def 1;
hence thesis by A5,A9,A10;
end;
hence thesis by A8,A9,FINSET_1:13;
end;
theorem
for M be non empty MetrSpace holds
TopSpaceMetr M is compact iff M is totally_bounded & M is complete
proof
let M be non empty MetrSpace;
set T=TopSpaceMetr M;
thus T is compact implies M is totally_bounded & M is complete
by TBSP_1:10,12;
assume that
A1: M is totally_bounded and
A2: M is complete;
now let A be Subset of T such that A3:A is infinite;
consider G be Subset-Family of M such that
A4: G is finite and
A5: the carrier of M = union G and
A6: for C be Subset of M st C in G ex w be Point of M st C = Ball(w,1/2)
by A1,TBSP_1:def 1;
consider X be Subset of M such that
A7: X in G & X /\ A is infinite by A3,A4,A5,Th37;
defpred Q[set] means for a be Subset of M st
a=$1 holds a is bounded & a is infinite & a is closed;
defpred P[set,set] means for a,b be Subset of M st $1=a & $2=b holds
b c= a & diameter b <= (diameter a)/2;
reconsider XA=X/\A as Subset of M;
A8: XA is bounded & diameter XA <=1
proof
consider w be Point of M such that
A9: X = Ball(w,1/2) by A6,A7;
X is bounded & XA c= X by A9,TBSP_1:19,XBOOLE_1:17;
then XA is bounded & diameter XA <=diameter X & diameter X<=2*(1/2)
by A9,TBSP_1:21,31,32;
hence thesis by XXREAL_0:2;
end;
reconsider xa=XA as Subset of T;
reconsider CXA=Cl xa as Subset of M;
set cM=the carrier of M;
xa c= Cl xa by PRE_TOPC:48;then
A9: CXA in bool cM & Q[CXA] by A7,A8,FINSET_1:13,Th9,Th7;
A10:for x st x in bool cM & Q[x] ex y st y in bool cM & P[x,y] & Q[y]
proof
let x such that
A11: x in bool cM & Q[x];
reconsider X=x as Subset of M by A11;
reconsider X'=X as Subset of T;
set d=diameter X;
A12:X is bounded by A11;
per cases by A12,TBSP_1:29;
suppose
A13: d=0;
take Y=X;
thus thesis by A11,A13;end;
suppose d>0;then
A14: d/4>0 by XREAL_1:226;
then consider F be Subset-Family of M such that
A15: F is finite and
A16: cM = union F and
A17: for C be Subset of M st C in F ex w be Point of M st
C = Ball(w,d/4) by A1,TBSP_1:def 1;
X is infinite by A11;
then consider Y be Subset of M such that
A18: Y in F & Y /\ X is infinite by A15,A16,Th37;
set YX=Y/\X;
consider w be Point of M such that
A19: Y = Ball(w,d/4) by A17,A18;
Y is bounded & YX c= Y by A19,TBSP_1:19,XBOOLE_1:17;then
A20: YX is bounded & diameter YX <=diameter Y & diameter Y<=2*(d/4)
by A14,A19,TBSP_1:21,31,32;then
A21: diameter YX<=d/2 by XXREAL_0:2;
reconsider yx=YX as Subset of T;
reconsider CYX=Cl yx as Subset of M;
take CYX;
A22: yx c= Cl yx by PRE_TOPC:48;
X is closed by A11;
then X' is closed & yx c= X' by XBOOLE_1:17,Th7;
hence thesis by A22,TOPS_1:31,A20,A21,A18,FINSET_1:13,Th7,Th9;end;
end;
consider f be Function such that
A11: dom f = NAT & rng f c= bool cM and
A12: f.0 = CXA and
A13: for k be Element of NAT
holds P[f.k,f.(k+1)] & Q[f.k] from TREES_2:sch 5(A9,A10);
reconsider f as SetSequence of M by A11,FUNCT_2:4;
A14:now let x such that
A15: x in dom f;
reconsider i=x as Element of NAT by A15;
f.i is infinite by A13;
hence f.x is non empty;
end;
A15:now let n;
n in NAT by ORDINAL1:def 13;
hence f.n is bounded by A13;
end;
now let n;
n in NAT by ORDINAL1:def 13;
hence f.n is closed by A13;
end;
then reconsider f as non-empty bounded closed SetSequence of M
by A14,A15,def1,def8,FUNCT_1:def 15;
for n be Element of NAT holds f.(n+1) c= f.n by A13;then
A16:f is descending by KURATO_2:def 5;
deffunc F(Element of NAT)=1/(1+$1);
consider seq be Real_Sequence such that
A17:for n be Element of NAT holds seq.n=F(n) from SEQ_1:sch 1;
reconsider NULL=0 as Real;
set Ns=NULL(#)seq;
for n be Element of NAT holds seq.n=1/(n+1) by A17;then
A18: seq is convergent & lim seq=0 by SEQ_4:45;then
A19: Ns is convergent & lim Ns=NULL*0 by SEQ_2:21,22;
set df=diameter f;
defpred N[Element of NAT] means Ns.$1 <= df.$1 & df.$1<=seq.$1;
CXA is bounded by A8,Th9;
then 0<=diameter CXA & diameter CXA <= 1&seq.0=1/(1+0)&Ns.0=NULL*seq.0
by A8,A17,Th9,TBSP_1:29,SEQ_1:13;then
A20:N[0] by A12,def2;
A21:for n be Element of NAT st N[n] holds N[n+1]
proof
let n be Element of NAT such that
A22: N[n];set n1=n+1;
df.n<=F(n) & diameter (f.n1)<=(diameter (f.n))/2& diameter (f.n)=df.n
by A13,A17,A22,def2;
then (df.n)/2<=F(n)/2 & df.n1<=(df.n)/2 by XREAL_1:74,def2;then
A23:df.n1<=F(n)/2 by XXREAL_0:2;
n1+1<=(n1+1)+n by NAT_1:11;
then F(n1)>=1/(2*n1) & 1/(2*n1)=F(n)/2 by XREAL_1:120,XCMPLX_1:79;
then
A24:F(n1)>=df.n1 by A23,XXREAL_0:2;
f.n1 is bounded by def1;
then 0<= diameter (f.n1) & Ns.n1=NULL*seq.n1 by TBSP_1:29,SEQ_1:13;
hence thesis by A17,A24,def2;
end;
A22:for n be Element of NAT holds N[n] from NAT_1:sch 1(A20,A21);then
A23:lim df = 0 & df is convergent by A18,A19,SEQ_2:33,34;
then meet f is non empty by A2,A16,Th11;
then consider p be set such that
A24: p in meet f by XBOOLE_0:def 1;
reconsider p as Point of T by A24;
reconsider p'=p as Point of M;
now let U be open Subset of T such that
A25: p in U;
consider r be real number such that
A26: r>0 & Ball(p',r) c= U by A25,TOPMETR:22;
r/2 >0 by A26,XREAL_1:217;
then consider n be Element of NAT such that
A27: for m be Element of NAT st n<=m holds abs(df.m-0)f.n & {p} c= f.n by ZFMISC_1:37;
then {p} c{} by XBOOLE_1:105;
then consider q be set such that
A28: q in f.n\{p} by XBOOLE_0:def 1;
reconsider q as Point of T by A28;
reconsider q'=q as Point of M;
reconsider B=Ball(q',dist(p',q')) as Subset of T;
q<>p by A28,ZFMISC_1:64;
then Ball(q',dist(p',q')) in Family_open_set M & dist(q',q')=0 &
dist(p',q')<>0 & dist(p',q')>=0 by PCOMPS_1:33,METRIC_1:1,2,5;
then B is open & q in B & f.n c= Cl xa & q in f.n
by A12,A16,A28,KURATO_2:22,ZFMISC_1:64,PRE_TOPC:def 5,METRIC_1:12;
then B meets xa by PRE_TOPC:54;
then consider s be set such that
A29: s in B & s in xa by XBOOLE_0:3;
reconsider s as Point of M by A29;
reconsider s'=s as Point of T;
take s';
df.n>=Ns.n & Ns.n=NULL*seq.n & abs(df.n-0)p by XBOOLE_0:def 3,A29,METRIC_1:12;
end;
hence Der A is non empty by TOPGEN_1:19;
end;
then T is countably_compact by Th29;
hence thesis by Th36;
end;
begin :: Well spaces
definition let T be set;
let S be Function of NAT,T;
let i be natural number;
redefine func S.i -> Element of T;
coherence
proof
reconsider i'=i as Element of NAT by ORDINAL1:def 13;
S.i'=S.i;
hence thesis;
end;
end;
theorem Th39:
for M be MetrStruct, a be Point of M,x holds
x in [:X,(the carrier of M)\{a}:]\/{[X,a]} iff
ex y be set,b be Point of M st
x=[y,b] & (y in X & b<>a or y = X & b = a)
proof
let M be MetrStruct,a be Point of M, x;
thus x in [:X,(the carrier of M)\{a}:]\/{[X,a]} implies
ex y be set,b be Point of M st
x=[y,b] & (y in X & b<>a or y = X & b = a)
proof
assume
A1: x in [:X,(the carrier of M)\{a}:]\/{[X,a]};
per cases by A1,XBOOLE_0:def 2;
suppose x in [:X,(the carrier of M)\{a}:];
then consider x1,x2 be set such that
A2: x1 in X & x2 in (the carrier of M)\{a} & x=[x1,x2]
by ZFMISC_1:def 2;
reconsider x2 as Point of M by A2;
take x1,x2;
thus thesis by A2,ZFMISC_1:64;end;
suppose x in {[X,a]};
then x=[X,a] by TARSKI:def 1;
hence thesis;end;
end;
given y be set,b be Point of M such that
A1: x=[y,b] & (y in X & b<>a or y = X & b = a);
per cases by A1;
suppose
A2: y in X & b<>a;
the carrier of M is non empty
proof
assume the carrier of M is empty;
then a={} & b={} by SUBSET_1:def 2;
hence thesis by A2;
end;
then b in (the carrier of M)\{a} by A2,ZFMISC_1:64;
then x in [:X,(the carrier of M)\{a}:] by A1,A2,ZFMISC_1:106;
hence thesis by XBOOLE_0:def 2;end;
suppose y = X & b = a;
then x in {[X,a]} by A1,TARSKI:def 1;
hence thesis by XBOOLE_0:def 2;end;
end;
definition
let M be MetrStruct;
let a be Point of M;
let X be set;
func well_dist(a,X) -> Function of
[:[:X,(the carrier of M)\{a}:]\/{[X,a]},
[:X,(the carrier of M)\{a}:]\/{[X,a]}:],REAL means :def10:
for x,y be Element of [:X,(the carrier of M)\{a}:]\/{[X,a]}
for x1,y1 be set,x2,y2 be Point of M st x = [x1,x2] & y = [y1,y2] holds
(x1 = y1 implies it.(x,y) = dist(x2,y2) ) &
(x1 <> y1 implies it.(x,y) = dist(x2,a)+dist(a,y2) );
existence
proof
set XX=[:X,(the carrier of M)\{a}:]\/{[X,a]};
defpred P[set,set,set] means
for x,y be Element of XX st x=$1 & y=$2
for x1,y1 be set, x2,y2 be Point of M st x=[x1,x2] & y=[y1,y2] holds
(x1=y1 implies $3=dist(x2,y2))&(x1<>y1 implies $3=dist(x2,a)+dist(a,y2));
A1: for x,y st x in XX & y in XX ex z be set st z in REAL & P[x,y,z]
proof
let x,y such that
A2: x in XX & y in XX;
consider x1 be set,x2 be Point of M such that
A3: x=[x1,x2] & (x1 in X & x2<>a or x1 = X & x2 = a)
by A2,Th39;
consider y1 be set,y2 be Point of M such that
A4: y=[y1,y2] & (y1 in X & y2<>a or y1 = X & y2 = a)
by A2,Th39;
now per cases;
suppose
A5: x1 = y1;
take d=dist(x2,y2);
thus d in REAL by XREAL_0:def 1;
let x',y' be Element of XX such that
A6: x' = x & y' = y;
let x1',y1' be set, x2',y2' be Point of M such that
A7: x' = [x1',x2'] & y' = [y1',y2'];
x1'=x1 & x2'=x2 & y1'=y1 & y2'=y2 by A3,A4,A6,A7,ZFMISC_1:33;
hence(x1' = y1' implies d = dist(x2',y2') ) &
(x1' <> y1' implies d = dist(x2',a)+dist(a,y2')) by A5;end;
suppose
A5: x1<>y1;
take d=dist(x2,a)+dist(a,y2);
thus d in REAL by XREAL_0:def 1;
let x',y' be Element of XX such that
A6: x'=x & y'=y;
let x1',y1' be set, x2',y2' be Point of M such that
A7: x' = [x1',x2'] & y' = [y1',y2'];
x1'=x1 & x2'=x2 & y1'=y1 & y2'=y2 by A3,A4,A6,A7,ZFMISC_1:33;
hence (x1' = y1' implies d = dist(x2',y2') ) &
(x1' <> y1' implies d = dist(x2',a)+dist(a,y2')) by A5;end;
end;
hence thesis;
end;
consider f being Function of [:XX,XX:],REAL such that
A2: for x,y st x in XX & y in XX holds P[x,y,f.(x,y)] from BINOP_1:sch 1(A1);
take f;
thus thesis by A2;
end;
uniqueness
proof
set XX=[:X,(the carrier of M)\{a}:]\/{[X,a]};
let w1,w2 be Function of [:XX,XX:],REAL such that
A1: for x,y be Element of XX
for x1,y1 be set, x2,y2 be Point of M st x = [x1,x2] & y = [y1,y2] holds
(x1 = y1 implies w1.(x,y) = dist(x2,y2) ) &
(x1 <> y1 implies w1.(x,y) = dist(x2,a)+dist(a,y2) ) and
A2: for x,y be Element of XX
for x1,y1 be set, x2,y2 be Point of M st x = [x1,x2] & y = [y1,y2] holds
(x1 = y1 implies w2.(x,y) = dist(x2,y2) ) &
(x1 <> y1 implies w2.(x,y) = dist(x2,a)+dist(a,y2) );
now let x,y such that
A3: x in XX & y in XX;
consider x1 be set,x2 be Point of M such that
A4: x=[x1,x2] & (x1 in X & x2<>a or x1 = X & x2 = a)
by A3,Th39;
consider y1 be set,y2 be Point of M such that
A5: y=[y1,y2] & (y1 in X & y2<>a or y1 = X & y2 = a)
by A3,Th39;
reconsider x2,y2 as Point of M;
x1=y1 or x1<>y1;
then (w1.(x,y)=dist(x2,y2) & w2.(x,y)=dist(x2,y2)) or
(w1.(x,y)=dist(x2,a)+dist(a,y2) & w2.(x,y)=dist(x2,a)+dist(a,y2))
by A1,A2,A3,A4,A5;
hence w1.(x,y)=w2.(x,y);
end;
hence thesis by BINOP_1:1;
end;
end;
theorem
for M be MetrStruct,a be Point of M
for X be non empty set holds
( well_dist(a,X) is Reflexive implies M is Reflexive ) &
( well_dist(a,X) is symmetric implies M is symmetric ) &
( well_dist(a,X) is triangle Reflexive implies M is triangle ) &
(well_dist(a,X) is discerning Reflexive implies M is discerning )
proof
let M be MetrStruct,A be Point of M;
let X be non empty set;
consider x0 be set such that
A0: x0 in X by XBOOLE_0:def 1;
set XX=[:X,(the carrier of M)\{A}:]\/{[X,A]};
set w=well_dist(A,X);thus
W1:w is Reflexive implies M is Reflexive
proof
assume
A3: w is Reflexive;
now let a be Element of M;
now per cases;
suppose a=A; then
A4: [X,a] in XX by Th39;
hence dist(a,a) = w.([X,a],[X,a]) by def10
.= 0 by A3,A4,METRIC_1:def 3;end;
suppose a<>A; then
A4: [x0,a] in XX by A0,Th39;
hence dist(a,a) = w.([x0,a],[x0,a]) by def10
.= 0 by A3,A4,METRIC_1:def 3;end;
end;
hence dist(a,a) = 0;
end;
hence thesis by METRIC_1:1;
end;
thus w is symmetric implies M is symmetric
proof
assume
A3:w is symmetric;
now let a,b be Element of M;
now per cases;
suppose a=A & b=A;
hence dist(a,b)=dist(b,a);end;
suppose
A4: a=A & b<>A;then
A5: [X,A] in XX & [x0,b] in XX by A0,Th39;
A6: X<>x0 by A0;
then dist(A,A)+dist(A,b) = w.([X,A],[x0,b]) by A5,def10
.= w.([x0,b],[X,A]) by A3,A5,METRIC_1:def 5
.= dist(b,A)+dist(A,A) by A5,A6,def10;
hence dist(a,b)=dist(b,a) by A4;end;
suppose
A4: a<>A & b=A;then
A5: [X,A] in XX & [x0,a] in XX by A0,Th39;
A6: X<>x0 by A0;
then dist(A,A)+dist(A,a) = w.([X,A],[x0,a]) by A5,def10
.= w.([x0,a],[X,A]) by A3,A5,METRIC_1:def 5
.= dist(a,A)+dist(A,A) by A5,A6,def10;
hence dist(a,b)=dist(b,a) by A4;end;
suppose a<>A & b<>A;then
A5: [x0,a] in XX & [x0,b] in XX by A0,Th39;
hence dist(a,b) = w.([x0,a],[x0,b]) by def10
.= w.([x0,b],[x0,a]) by A3,A5,METRIC_1:def 5
.= dist(b,a) by A5,def10;end;
end;
hence dist(a,b) = dist(b,a);
end;
hence thesis by METRIC_1:3;
end;
thus w is triangle Reflexive implies M is triangle
proof
assume
A3: w is triangle Reflexive;
now let a,b,c be Point of M;
now per cases;
suppose a=A & b=A & c =A;
then reconsider Xa=[X,a],Xb=[X,b],Xc =[X,c] as Element of XX
by Th39;
w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc) & dist(a,c)=w.(Xa,Xc) &
dist(a,b)=w.(Xa,Xb) & dist(b,c)=w.(Xb,Xc)
by A3,def10,METRIC_1:def 6;
hence dist(a,c)<=dist(a,b)+dist(b,c);end;
suppose
A4: a=A & b=A & c <> A;
then reconsider Xa=[X,a],Xb=[X,b],Xc =[x0,c] as Element of XX
by A0,Th39;
x0<>X by A0;
then w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc) & dist(a,b)=w.(Xa,Xb) &
dist(a,a)+dist(a,c)=w.(Xa,Xc) & dist(a,a)+dist(b,c)=w.(Xb,Xc)&
dist(a,a)=0 by A3,W1,A4,def10,METRIC_1:def 6,METRIC_1:1;
hence dist(a,c)<=dist(a,b)+dist(b,c);end;
suppose
A4: a=A & b<>A & c = A;
then reconsider Xa=[X,a],Xb=[x0,b],Xc =[X,c] as Element of XX
by A0,Th39;
x0<>X by A0;
then w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc) & dist(a,c)=w.(Xa,Xc) &
dist(a,a)+dist(a,b)=w.(Xa,Xb) & dist(b,c)+dist(a,a)=w.(Xb,Xc) &
dist(a,a)=0 by A3,W1,A4,def10,METRIC_1:1,def 6;
hence dist(a,c)<=dist(a,b)+dist(b,c);end;
suppose
A4: a=A & b<>A & c <> A;
then reconsider Xa=[X,a],Xb=[x0,b],Xc =[x0,c] as Element of XX
by A0,Th39;
x0<>X by A0;
then w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc)&dist(a,a)+dist(a,c)=w.(Xa,Xc)&
dist(a,a)+dist(a,b)=w.(Xa,Xb)&dist(b,c)=w.(Xb,Xc)&dist(a,a)=0
by A3,W1,A4,def10,METRIC_1:def 6,1;
hence dist(a,c)<=dist(a,b)+dist(b,c);end;
suppose
A4: a<>A & b=A & c =A;
then reconsider Xa=[x0,a],Xb=[X,b],Xc =[X,c] as Element of XX
by A0,Th39;
x0<>X by A0;
then w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc)&dist(a,c)+dist(c,c)=w.(Xa,Xc)&
dist(a,b)+dist(c,c)=w.(Xa,Xb) & dist(b,c)=w.(Xb,Xc)&dist(c,c)=0
by A3,W1,A4,def10,METRIC_1:1,def 6;
hence dist(a,c)<=dist(a,b)+dist(b,c);end;
suppose
A4: a<>A & b=A & c <>A;
then reconsider Xa=[x0,a],Xb=[X,b],Xc =[x0,c] as Element of XX
by A0,Th39;
x0<>X by A0;
then w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc) & dist(a,c)=w.(Xa,Xc) &
dist(a,b)+dist(b,b)=w.(Xa,Xb) & dist(b,b)+dist(b,c)=w.(Xb,Xc)&
dist(b,b)=0 by W1,A3,A4,def10,METRIC_1:1,def 6;
hence dist(a,c)<=dist(a,b)+dist(b,c);end;
suppose A4:a<>A & b<>A & c = A;
then reconsider Xa=[x0,a],Xb=[x0,b],Xc =[X,c] as Element of XX
by A0,Th39;
x0<>X by A0;
then w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc)&dist(a,c)+dist(c,c)=w.(Xa,Xc)&
dist(a,b)=w.(Xa,Xb) & dist(b,c)+dist(c,c)=w.(Xb,Xc) &
dist(c,c)=0 by A3,W1,A4,def10,METRIC_1:def 6,1;
hence dist(a,c)<=dist(a,b)+dist(b,c);end;
suppose a<>A & b<>A & c <> A;
then reconsider Xa=[x0,a],Xb=[x0,b],Xc =[x0,c] as Element of XX
by A0,Th39;
w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc) & dist(a,c)=w.(Xa,Xc) &
dist(a,b)=w.(Xa,Xb) & dist(b,c)=w.(Xb,Xc)
by A3,def10,METRIC_1:def 6;
hence dist(a,c)<=dist(a,b)+dist(b,c);end;
end;
hence dist(a,c)<=dist(a,b)+dist(b,c);
end;
hence thesis by METRIC_1:4;
end;
assume
A3:w is discerning Reflexive;
now let a,b be Point of M;
assume
A4: dist(a,b)=0;
now per cases;
suppose a=A & b=A;
hence a=b;end;
suppose A5:a=A & b<>A;
then reconsider Xa=[X,a],Xb=[x0,b] as Element of XX by A0,Th39;
x0<>X by A0;
then dist(a,a)+dist(a,b)=w.(Xa,Xb) & dist(a,a)=0
by A3,W1,A5,def10,METRIC_1:1;
then Xa=Xb by A3,A4,METRIC_1:def 4;
hence a=b by ZFMISC_1:33;end;
suppose A5:a<>A & b=A;
then reconsider Xa=[x0,a],Xb=[X,b] as Element of XX by A0,Th39;
x0<>X by A0;
then dist(a,b)+dist(b,b)=w.(Xa,Xb) & dist(b,b)=0
by A3,W1,A5,def10,METRIC_1:1;
then Xa=Xb by A3,A4,METRIC_1:def 4;
hence a=b by ZFMISC_1:33;end;
suppose a<>A & b<>A;
then reconsider Xa=[x0,a],Xb=[x0,b] as Element of XX by A0,Th39;
dist(a,b)=w.(Xa,Xb) by def10;
then Xa=Xb by A3,A4,METRIC_1:def 4;
hence a=b by ZFMISC_1:33;end;
end;
hence a=b;
end;
hence thesis by METRIC_1:2;
end;
definition
let M be MetrStruct;
let a be Point of M;
let X be set;
func WellSpace(a,X) -> strict MetrStruct equals
MetrStruct (#[:X,(the carrier of M)\{a}:]\/{[X,a]},well_dist(a,X)#);
coherence;
end;
registration
let M be MetrStruct;
let a be Point of M;
let X be set;
cluster WellSpace(a,X) -> non empty;
coherence;
end;
PPP1:for M be MetrStruct,a be Point of M,X holds
(M is Reflexive implies WellSpace(a,X) is Reflexive) &
(M is symmetric implies WellSpace(a,X) is symmetric) &
(M is triangle symmetric Reflexive implies WellSpace(a,X) is triangle)&
(M is triangle symmetric Reflexive discerning implies
WellSpace(a,X) is discerning)
proof
let M be MetrStruct,a be Point of M,X;
set XX=[:X,(the carrier of M)\{a}:]\/{[X,a]};
set w=well_dist(a,X);
set W=WellSpace(a,X);
thus M is Reflexive implies W is Reflexive
proof
assume
A1: M is Reflexive;
now let A be Element of XX;
consider y be set,b be Point of M such that
A2: A=[y,b] & (y in X & b<>a or y = X & b = a) by Th39;
thus w.(A,A) = dist(b,b) by A2,def10
.= 0 by A1,METRIC_1:1;
end;
then w is Reflexive by METRIC_1:def 3;
hence thesis by METRIC_1:def 7;
end;
thus M is symmetric implies W is symmetric
proof
assume
A1: M is symmetric;
now let A,B be Element of XX;
consider y1 be set,b1 be Point of M such that
A2: A=[y1,b1] & (y1 in X & b1<>a or y1 = X & b1 = a) by Th39;
consider y2 be set,b2 be Point of M such that
A3: B=[y2,b2] & (y2 in X & b2<>a or y2 = X & b2 = a) by Th39;
now per cases by A2,A3;
suppose b1=a & y1=X & b2=a & y2=X;
hence w.(A,B)=w.(B,A) by A2,A3;end;
suppose
A4: y1 <>y2;
hence w.(A,B) = dist(b1,a)+dist(a,b2) by A2,A3,def10
.= dist(a,b1)+dist(a,b2) by A1,METRIC_1:3
.= dist(a,b1)+dist(b2,a) by A1,METRIC_1:3
.= w.(B,A) by A2,A3,A4,def10;end;
suppose
A4: b1<>a & b2<>a & y1=y2;
hence w.(A,B) = dist(b1,b2) by A2,A3,def10
.= dist(b2,b1) by A1,METRIC_1:3
.=w.(B,A) by A2,A3,A4,def10;end;
end;
hence w.(A,B)=w.(B,A);
end;
then w is symmetric by METRIC_1:def 5;
hence thesis by METRIC_1:def 9;
end;
thus M is triangle symmetric Reflexive implies WellSpace(a,X) is triangle
proof
assume
A1: M is triangle symmetric Reflexive;
now let A,B,C be Element of XX;
consider y1 be set,b1 be Point of M such that
A2: A=[y1,b1] & (y1 in X & b1<>a or y1 = X & b1 = a) by Th39;
consider y2 be set,b2 be Point of M such that
A3: B=[y2,b2] & (y2 in X & b2<>a or y2 = X & b2 = a) by Th39;
consider y3 be set,b3 be Point of M such that
A4: C=[y3,b3] & (y3 in X & b3<>a or y3 = X & b3 = a) by Th39;
now per cases;
suppose y1=y2 & y1=y3;
then dist(b1,b3)=w.(A,C)&dist(b1,b2)=w.(A,B)&dist(b2,b3)=w.(B,C)&
dist(b1,b3)<=dist(b1,b2)+dist(b2,b3)
by A1,A2,A3,A4,def10,METRIC_1:4;
hence w.(A,C)<=w.(A,B)+w.(B,C);end;
suppose y1<>y2 & y1=y3;then
A5: dist(b1,b3)=w.(A,C) & dist(b1,a)+dist(a,b2)=w.(A,B) &
dist(b2,a)+dist(a,b3)=w.(B,C)&dist(b1,b2)<=dist(b1,a)+dist(a,b2)
& dist(b2,b3)<=dist(b2,a)+dist(a,b3)
by A1,A2,A3,A4,def10,METRIC_1:4;
then dist(b1,b2)+dist(b2,b3)<=w.(A,B)+w.(B,C) & dist(b1,b3)<=
dist(b1,b2)+dist(b2,b3) by XREAL_1:9,A1,METRIC_1:4;
hence w.(A,C)<=w.(A,B)+w.(B,C) by A5,XXREAL_0:2;end;
suppose y1=y2 & y1<>y3;then
A5: dist(b1,a)+dist(a,b3)=w.(A,C) & dist(b1,b2)=w.(A,B) &
dist(b2,a)+dist(a,b3)=w.(B,C) & dist(b1,a)<=dist(b1,b2) +
dist(b2,a) by A1,A2,A3,A4,def10,METRIC_1:4;
then w.(A,C)<=dist(b1,b2)+dist(b2,a)+dist(a,b3)by XREAL_1:8;
hence w.(A,C)<=w.(A,B)+w.(B,C) by A5;end;
suppose y1<>y2 & y1<>y3 & y2<>y3;then
A5: dist(b1,a)+dist(a,b3)=w.(A,C) & dist(b1,a)+dist(a,b2)=w.(A,B) &
dist(b2,a)+dist(a,b3)=w.(B,C) by A2,A3,A4,def10;
0<=dist(a,b2) & 0<=dist(b2,a) by A1,METRIC_1:5;
then dist(b1,a)+0<=w.(A,B)&0+dist(a,b3)<=w.(B,C) by A5,XREAL_1:8;
hence w.(A,C)<=w.(A,B)+w.(B,C) by A5,XREAL_1:9;end;
suppose y1<>y2 & y1<>y3 & y2=y3;then
A5: dist(b1,a)+dist(a,b3)=w.(A,C) & dist(b1,a)+dist(a,b2)=w.(A,B)&
dist(b2,b3)=w.(B,C) & dist(a,b3)<=dist(a,b2)+dist(b2,b3)
by A1,A2,A3,A4,def10,METRIC_1:4;
then w.(A,C)<=dist(b1,a)+(dist(a,b2)+dist(b2,b3)) by XREAL_1:9;
hence w.(A,C)<=w.(A,B)+w.(B,C) by A5;end;
end;
hence w.(A,C)<=w.(A,B)+w.(B,C);
end;
then w is triangle by METRIC_1:def 6;
hence thesis by METRIC_1:def 10;
end;
assume
A1: M is triangle symmetric Reflexive discerning;
now let A,B be Element of XX;
assume
A2: w.(A,B)=0;
consider y1 be set,b1 be Point of M such that
A3: A=[y1,b1] & (y1 in X & b1<>a or y1 = X & b1 = a) by Th39;
consider y2 be set,b2 be Point of M such that
A4: B=[y2,b2] & (y2 in X & b2<>a or y2 = X & b2 = a) by Th39;
now per cases;
suppose
A5: y1=y2;
then w.(A,B)=dist(b1,b2) by A3,A4,def10;
hence A=B by A1,A2,METRIC_1:2,A3,A4,A5;end;
suppose y1<>y2;
then w.(A,B)=dist(b1,a)+dist(a,b2) & dist(a,b2)>=0 & dist(b1,a)>=0
by A1,A3,A4,def10,METRIC_1:5;
then dist(b1,a)=0 & dist(a,b2)=0 by A2,XREAL_1:29;
hence A=B by A1,METRIC_1:2,A3,A4;end;
end;
hence A=B;
end;
then w is discerning by METRIC_1:def 4;
hence thesis by METRIC_1:def 8;
end;
registration
let M be Reflexive MetrStruct;
let a be Point of M;
let X be set;
cluster WellSpace(a,X) -> Reflexive;
coherence by PPP1;
end;
registration
let M be symmetric MetrStruct;
let a be Point of M;
let X be set;
cluster WellSpace(a,X) -> symmetric;
coherence by PPP1;
end;
registration
let M be symmetric triangle Reflexive MetrStruct;
let a be Point of M;
let X be set;
cluster WellSpace(a,X) -> triangle;
coherence by PPP1;
end;
registration
let M be MetrSpace;
let a be Point of M;
let X be set;
cluster WellSpace(a,X) -> discerning;
coherence by PPP1;
end;
theorem
for M be triangle Reflexive non empty MetrStruct
for a be Point of M
for X be non empty set holds
WellSpace(a,X) is complete implies M is complete
proof
let M be triangle Reflexive non empty MetrStruct;
let a be Point of M;
let X be non empty set;
consider x0 be set such that
A0: x0 in X by XBOOLE_0:def 1;
assume
A1: WellSpace(a,X) is complete;
set W=WellSpace(a,X);
set XX=[:X,(the carrier of M)\{a}:]\/{[X,a]};
let S be sequence of M such that
A2: S is Cauchy;
defpred P[set,set] means
(S.$1<>a implies $2=[x0,S.$1]) & (S.$1=a implies $2=[X,S.$1]);
A3:for x st x in NAT ex y st y in the carrier of W & P[x,y]
proof
let x such that
A4: x in NAT;
reconsider i=x as Element of NAT by A4;
per cases;
suppose
A5: S.i<>a;
take xS=[x0,S.i];
thus thesis by A0,A5,Th39;end;
suppose
A5: S.x=a;
take xS=[X,a];
thus thesis by A5,Th39;end;
end;
consider S' be sequence of W such that
A4: for x st x in NAT holds P[x,S'.x] from FUNCT_2:sch 1(A3);
S' is Cauchy
proof
let r such that
A5: r>0;
consider p be Element of NAT such that
A6: for n,m be Element of NAT st p<=n & p<=m holds dist(S.n,S.m)a & S.m=a;
then [x0,S.n]=S'.n & [X,S.m]=S'.m & X<>x0 by A0,A4;
then dist(S'.n,S'.m)=dist(S.n,S.m)+dist(S.m,S.m) & dist(S.m,S.m)=0
by A8,def10,METRIC_1:1;
hence thesis by A6,A7;end;
suppose
A8: S.n=a & S.m<>a;
then [X,S.n]=S'.n & [x0,S.m]=S'.m & X<>x0 by A0,A4;
then dist(S'.n,S'.m)=dist(S.n,S.n)+dist(S.n,S.m) & dist(S.n,S.n)=0
by A8,def10,METRIC_1:1;
hence thesis by A6,A7;end;
suppose S.n<>a & S.m<>a;
then [x0,S.n]=S'.n & [x0,S.m]=S'.m by A4;
then dist(S'.n,S'.m)=dist(S.n,S.m) by def10;
hence thesis by A6,A7;end;
end;
then S' is convergent by A1,TBSP_1:def 6;
then consider L being Element of W such that
A6: for r st r>0 ex n be Element of NAT st
for m be Element of NAT st n<=m holds dist(S'.m,L)a or L1 = X & L2 = a) by Th39;
take L2;
let r such that
A8: r>0;
consider n be Element of NAT such that
A9: for m be Element of NAT st n<=m holds dist(S'.m,L)X;
then S'.m=[X,a] by A4;
then dist(S'.m,L)=dist(S.m,S.m)+dist(S.m,L2) & dist(S.m,S.m)=0
by A7,A12,def10,METRIC_1:1;
hence thesis by A10,A9;end;
suppose
A12: S.m <> a & L1=x0;
then S'.m=[x0,S.m] by A4;
then dist(S'.m,L)=dist(S.m,L2) by A7,A12,def10;
hence thesis by A10,A9;end;
suppose
A12: S.m <> a & L1<>x0;
then S'.m=[x0,S.m] by A4;
then dist(S'.m,L)=dist(S.m,a)+dist(a,L2) & dist(S.m,a)+dist(a,L2)>=
dist(S.m,L2) & dist(S'.m,L) 0 ex n st for m st m >= n holds dist(S.m,Xa) < r)
or
ex n,Y st for m st m >= n ex p be Point of M st S.m = [Y,p]
proof
let M be symmetric triangle Reflexive non empty MetrStruct;
let a be Point of M;
set W=WellSpace(a,X);
set XX=[:X,(the carrier of M)\{a}:]\/{[X,a]};
set w=well_dist(a,X);
let S be sequence of W such that
A1: S is Cauchy;
reconsider Xa=[X,a] as Point of W by Th39;
per cases;
suppose for r st r > 0 ex n st for m st m >= n holds
dist(S.m,Xa) < r;
hence thesis;end;
suppose ex r st r > 0 & for n ex m st m >= n & dist(S.m,Xa) >= r;
then consider r be Real such that
A3: r > 0 and
A4: for n ex m st m >= n & dist(S.m,Xa) >= r;
consider p be Element of NAT such that
A5: for n,m be Element of NAT st n>=p & m>=p holds dist(S.n,S.m)= p & dist(S.p',Xa) >= r by A4;
consider Y be set,y be Point of M such that
A8:S.p'=[Y,y] & (Y in X & y<>a or Y = X & y = a) by Th39;
ex n,Y st for m st m >= n ex p be Point of M st S.m = [Y,p]
proof
take p',Y;
let m such that
A9: m >= p';
consider Z be set,z be Point of M such that
A10:S.m=[Z,z] & (Z in X & z<>a or Z = X & z = a) by Th39;
Y = Z
proof
assume
A11: Y<>Z;
(X=Y or X<>Y) & dist(a,a)=0 by METRIC_1:1;
then dist(S.p',Xa)=dist(y,a) or dist(S.p',Xa)=dist(y,a)+0
by A8,def10;
then dist(y,a)>=r & dist(a,z) >=0 by A6,METRIC_1:5;
then dist(y,a)+dist(a,z)>=r+0 & m>=p & m in NAT & p' in NAT
by A6,A9,XREAL_1:9,XXREAL_0:2,ORDINAL1:def 13;
then dist(S.p',S.m)>=r &dist(S.p',S.m)a or s1 = X & s2 = a) by Th39;
take s2;
thus thesis by A5;
end;
consider S be sequence of M such that
A4: for x st x in NAT holds P[x,S.x] from FUNCT_2:sch 1(A3);
S is Cauchy
proof
let r such that
A5: r>0;
consider p be Element of NAT such that
A6: for n,m be Element of NAT st p<=n & p<=m holds dist(S'.n,S'.m)y;
then dist(S'.n,S'.m)=dist(S.n,a)+dist(a,S.m) &
dist(S.n,S.m) <= dist(S.n,a)+dist(a,S.m) & dist(S'.n,S'.m)0 ex n be Element of NAT st
for m be Element of NAT st n<=m holds dist(S.m,L) 0;
consider n be Element of NAT such that
A8: for m be Element of NAT st n<=m holds dist(S.m,L)=n;
consider x such that
A10: S'.m=[x,S.m] by A4;
(x=X or x<>X)& dist(a,a)=0 by METRIC_1:1;
then dist(S'.m,Xa)=dist(S.m,L) or dist(S'.m,Xa)=dist(S.m,L)+0
by A10,B2,def10;
hence dist(S'.m,Xa) 0 ex n st for m st m >= n holds dist(S'.m,Xa) < r;
take Xa;
let r such that
A8: r > 0;
consider n such that
A9: for m st m >= n holds dist(S'.m,Xa) < r by A7,A8;
reconsider n as Element of NAT by ORDINAL1:def 13;
take n;
let m be Element of NAT such that
A10: m >= n;
thus dist(S'.m,Xa) < r by A9,A10;end;
suppose
A7: a<>L & ex n,Y st for m st m >= n
ex p be Point of M st S'.m = [Y,p];
then consider n,Y such that
A9: for m st m >= n ex p be Point of M st S'.m = [Y,p];
consider s1 be set,s2 be Point of M such that
D1: S'.n=[s1,s2] & (s1 in X & s2<>a or s1 = X & s2 = a) by Th39;
consider s3 be Point of M such that
D2:S'.n = [Y,s3] by A9;
per cases by D1,D2,ZFMISC_1:33;
suppose Y in X;
then reconsider YL=[Y,L] as Point of W by A7,Th39;
take YL;
let r such that
A10: r > 0;
consider p be Element of NAT such that
A11: for m be Element of NAT st p<=m holds dist(S.m,L)= mm;
mm >= n by XXREAL_0:25;
then m >= n by A12,XXREAL_0:2;
then consider pm be Point of M such that
A13: S'.m = [Y,pm] by A9;
consider x such that
A14:S'.m=[x,S.m] by A4;
mm >= p by XXREAL_0:25;then
A15:m>=p by A12,XXREAL_0:2;
x=Y by A13,A14,ZFMISC_1:33;
then dist(S'.m,YL)=dist(S.m,L) by A14,def10;
hence dist(S'.m,YL) 0;
reconsider n as Element of NAT by ORDINAL1:def 13;
take n;
let m be Element of NAT such that
A12: m >= n;
consider t1 be set,t2 be Point of M such that
A13: S'.m=[t1,t2] & (t1 in X & t2<>a or t1 = X & t2 = a) by Th39;
consider t3 be Point of M such that
A14:S'.m = [Y,t3] by A9,A12;
Y=t1 & t2=t3 by A13,A14,ZFMISC_1:33;
hence dist(S'.m,Xa)0
for X be infinite set holds
WellSpace(a,X) is complete &
ex S be non-empty bounded SetSequence of WellSpace(a,X) st
S is closed & S is descending & meet S is empty
proof
let M be symmetric triangle Reflexive non empty MetrStruct such that
A1: M is complete;
let a be Point of M such that
A2: ex b be Point of M st dist(a,b) <> 0;
consider b be Point of M such that
A3: dist(a,b)<>0 by A2;
A3':b<>a by A3,METRIC_1:1;
let X be infinite set;
set W=WellSpace(a,X);
thus W is complete by A1,Th43;
set TW=TopSpaceMetr W;
consider f being Function of NAT, X such that
A4: f is one-to-one by DICKSON:3;
defpred p[set,set] means $2=[f.$1,b];
A5:for x st x in NAT ex y st y in the carrier of TW & p[x,y]
proof
let x such that
A6: x in NAT;
take [f.x,b];
x in dom f by A6,FUNCT_2:def 1;
then f.x in rng f by FUNCT_1:def 5;
hence thesis by A3',Th39;
end;
consider s be Function of NAT, the carrier of TW such that
A6: for x st x in NAT holds p[x,s.x] from FUNCT_2:sch 1(A5);
deffunc P(set)={s.$1};
A7:for x st x in NAT holds P(x) in bool(the carrier of TW)
proof
let x such that
A8: x in NAT;
dom s=NAT by FUNCT_2:def 1;
then s.x in rng s by A8,FUNCT_1:def 5;
then P(x) is Subset of W by SUBSET_1:55;
hence thesis;
end;
consider S be SetSequence of TW such that
A8: for x st x in NAT holds S.x=P(x) from FUNCT_2:sch 2(A7);
now let x be set such that
A9: x in dom S;
S.x={s.x} by A8,A9;
hence S.x is non empty;
end;then
A10:S is non-empty by FUNCT_1:def 15;
reconsider rngs=rng s as Subset of TW;
set F={{x} where x is Element of TW: x in rngs};
reconsider F as Subset-Family of TW by RELSET_2:16;
rng S c= F
proof
let x such that
A11: x in rng S;
consider y such that
A12: y in dom S & S.y=x by A11,FUNCT_1:def 5;
dom S=NAT & dom s=NAT by FUNCT_2:def 1;
then x={s.y} & s.y in rngs by A8,A12,FUNCT_1:def 5;
hence thesis;
end;
then consider R be non-empty closed SetSequence of TW such that
A11: R is descending and
A12: F is locally_finite & S is one-to-one implies meet R = {} and
A13: for i ex Si be Subset-Family of TW st
R.i = Cl union Si &
Si = {S.j where j is Element of NAT: j >= i} by A10,Th24;
reconsider R'=R as non-empty SetSequence of W;
dist(a,b)>0 by A3,METRIC_1:5;then
A15: 2*dist(a,b)>0 by XREAL_1:131;
A16:now let x,y be Point of W such that A17:x in rngs & y in rngs & x <> y;
consider x1 be set such that
A18: x1 in dom s & s.x1=x by A17,FUNCT_1:def 5;
consider y1 be set such that
A19: y1 in dom s & s.y1=y by A17,FUNCT_1:def 5;
x=[f.x1,b] & y=[f.y1,b] by A6,A18,A19;
then well_dist(a,X).(x,y)=dist(b,a)+dist(a,b) by A17,def10;
hence dist(x,y)=2*dist(a,b);
end;
now let i;
consider Si be Subset-Family of TW such that
A17: R.i = Cl union Si and
A18: Si = {S.j where j is Element of NAT: j >= i} by A13;
reconsider SI=union Si,CLR=Cl union Si as Subset of W;
now let x,y being Point of W such that
A19: x in SI & y in SI;
consider xS be set such that
A20: x in xS & xS in Si by A19,TARSKI:def 4;
consider yS be set such that
A21: y in yS & yS in Si by A19,TARSKI:def 4;
consider j1 be Element of NAT such that
A22: xS=S.j1 & j1 >= i by A18,A20;
consider j2 be Element of NAT such that
A23: yS=S.j2 & j2 >= i by A18,A21;
dom s=NAT & dom S=NAT by FUNCT_2:def 1;
then s.j1 in rngs & S.j1={s.j1} & s.j2 in rngs & S.j2={s.j2}
by A8,FUNCT_1:def 5;
then x in rngs & y in rngs & (x=y or x<>y)
by A20,A21,A22,A23,TARSKI:def 1;
hence dist(x,y)<=2*dist(a,b) by A15,A16,METRIC_1:1;
end;
then SI is bounded by A15,TBSP_1:def 9;
hence R'.i is bounded by A17,Th9;
end;
then reconsider R' as non-empty bounded SetSequence of W by def1;
take R';
thus R' is closed & R' is descending by A11,Th8;
A17:for x,y be Point of W st x<>y & x in rngs & y in rngs holds
dist(x,y)>=2*dist(a,b) by A16;
now let x1,x2 be set such that
A18: x1 in NAT & x2 in NAT & S.x1 = S.x2;
S.x1={s.x1} & S.x2={s.x2} & s.x1 in {s.x1} by A8,A18,TARSKI:def 1;
then s.x1=s.x2 & s.x1=[f.x1,b] & s.x2=[f.x2,b] by A6,A18,TARSKI:def 1;
then f.x1=f.x2 by ZFMISC_1:33;
hence x1 = x2 by A4,A18,FUNCT_2:25;
end;
hence thesis by A12,A17,FUNCT_2:25,A15,LocallyFinite;
end;
theorem
ex M be non empty MetrSpace st
M is complete &
ex S be non-empty bounded SetSequence of M st
S is closed & S is descending & meet S is empty
proof
reconsider D=DiscreteSpace 2 as non empty MetrSpace;
reconsider a=0,b=1 as Point of D by EULER_1:1;
A1:1=dist(a,b) by METRIC_1:def 11;
TopSpaceMetr D is compact by COMPTS_1:27;
then D is complete & NAT is infinite by TBSP_1:10,CARD_4:15;
then WellSpace(a,NAT) is complete &
ex S be non-empty bounded SetSequence of WellSpace(a,NAT) st
S is closed & S is descending & meet S is empty by A1,Th44;
hence thesis;
end;*