:: Complete Spaces
:: by Karol P\c{a}k
::
:: Received October 12, 2007
:: Copyright (c) 2007-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ORDINAL1, REAL_1, XBOOLE_0, METRIC_1, PROB_1, XXREAL_2,
FUNCT_1, RELAT_1, STRUCT_0, PRE_TOPC, SUBSET_1, FUNCOP_1, XXREAL_0,
MEASURE5, SEQ_1, CARD_1, ARYTM_1, ARYTM_3, VALUED_0, TARSKI, ORDINAL2,
NAT_1, BHSP_3, COMPLEX1, RELAT_2, RCOMP_1, PCOMPS_1, ZFMISC_1, REWRITE1,
SETFAM_1, SEQ_2, METRIC_6, FRECHET, FINSET_1, VALUED_1, CARD_3, TOPGEN_1,
WELLORD1, ORDERS_2, PARTFUN1, WELLFND1, TBSP_1, WAYBEL23, RLVECT_3,
COMPL_SP;
notations METRIC_6, RELAT_2, BINOP_1, TOPMETR, CARD_1, FUNCOP_1, CANTOR_1,
WELLORD1, XCMPLX_0, COMPLEX1, FINSET_1, SEQ_2, TARSKI, XBOOLE_0,
SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, ZFMISC_1, XXREAL_0, XREAL_0,
REAL_1, SETFAM_1, DOMAIN_1, TOPS_2, FUNCT_1, VALUED_1, NAT_1, VALUED_0,
STRUCT_0, PRE_TOPC, COMPTS_1, SEQ_1, TBSP_1, RELSET_1, PARTFUN1, FUNCT_2,
METRIC_1, PCOMPS_1, CARD_3, PROB_1, FRECHET, KURATO_0, KURATO_2,
WELLFND1, WAYBEL23, ORDERS_2, TOPGEN_1;
constructors REAL_1, TBSP_1, FRECHET, COMPLEX1, SEQ_2, TOPS_2, WELLORD1,
CANTOR_1, URYSOHN3, METRIC_6, WELLFND1, TOPGEN_4, WAYBEL23, TOPGEN_1,
COMPTS_1, BINOP_2, KURATO_0, COMSEQ_2, BINOP_1;
registrations TOPMETR, PRE_TOPC, PCOMPS_1, NAT_1, TBSP_1, XREAL_0, RELSET_1,
SUBSET_1, STRUCT_0, TOPS_1, METRIC_1, HAUSDORF, MEMBERED, YELLOW13,
CARD_1, XBOOLE_0, VALUED_1, FUNCT_2, NUMBERS, FINSET_1, SEQ_4, WELLFND1,
VALUED_0, ORDINAL1;
requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, TOPS_2, TBSP_1, PCOMPS_1, COMPTS_1;
equalities TARSKI, SUBSET_1, STRUCT_0, PCOMPS_1, METRIC_1, ORDINAL1;
expansions TARSKI, TOPS_2, TBSP_1, PCOMPS_1, COMPTS_1, METRIC_1;
theorems 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, 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,
FRECHET2, FRECHET, STIRL2_1, CARD_1, HAUSDORF, TOPMETR3, CARD_3,
TOPGEN_4, DICKSON, RELSET_2, TOPGEN_1, WELLFND1, WAYBEL23, UNIFORM1,
CARD_2, TOPREAL6, FINSET_1, PROB_1, FUNCOP_1, KURATO_0, XTUPLE_0;
schemes WELLFND1, TREES_2, FUNCT_2, NAT_1, FRAENKEL, BINOP_1, SEQ_1;
begin :: Preliminaries
reserve i,n,m for Nat,
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 pointwise_bounded means
:Def1:
for i holds S.i is bounded;
end;
registration
let M be non empty Reflexive MetrStruct;
cluster pointwise_bounded non-empty for SetSequence of M;
existence
proof
consider x being object 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;
take S = NAT --> X;
A2: now
let x1,x2 being Point of M such that
A3: x1 in X and
A4: x2 in X;
A5: x2=x by A4,TARSKI:def 1;
x1=x by A3,TARSKI:def 1;
hence dist(x1,x2)<=1 by A5,METRIC_1:1;
end;
A6: now
let i;
reconsider i9=i as Element of NAT by ORDINAL1:def 12;
S.i9= X by FUNCOP_1:7;
hence S.i is bounded by A2;
end;
for x being object st x in dom S holds S.x is non empty by FUNCOP_1:7;
hence thesis by A6,FUNCT_1:def 9;
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[object,object] means for i st i=$1 holds $2=diameter (S.i);
A1: for x being object st x in NAT ex y being object st y in REAL & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider i=x as Nat;
take diameter (S.i);
thus thesis by XREAL_0:def 1 ;
end;
consider f be sequence of REAL such that
A2: for x being object 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 12;
hence thesis by A2;
end;
uniqueness
proof
let D1,D2 be Real_Sequence such that
A3: for i holds D1.i = diameter S.i and
A4: for i holds D2.i = diameter S.i;
now
let x be Element of NAT;
thus D1.x = diameter S.x by A3
.= D2.x by A4;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th1:
for M be Reflexive non empty MetrStruct for S be pointwise_bounded
SetSequence of M holds diameter S is bounded_below
proof
let M be Reflexive non empty MetrStruct;
let S be pointwise_bounded SetSequence of M;
set d=diameter S;
now
let n be Nat;
A1: diameter (S.n)=d.n by Def2;
S.n is bounded by Def1;
then 0<=d.n by A1,TBSP_1:21;
hence -1 < d.n by XXREAL_0:2;
end;
hence thesis by SEQ_2:def 4;
end;
registration
let M be Reflexive non empty MetrStruct,
S be SetSequence of M;
cluster diameter S -> real-valued;
coherence;
end;
theorem Th2:
for M be Reflexive non empty MetrStruct for S be pointwise_bounded
SetSequence of M st S is non-ascending holds diameter S is bounded_above &
diameter S is non-increasing
proof
let M be Reflexive non empty MetrStruct;
let S be pointwise_bounded SetSequence of M such that
A1: S is non-ascending;
set d=diameter S;
A2: now
let n be Nat;
A3: d.0+0<d.0+1 by XREAL_1:8;
A4: diameter S.n=d.n by Def2;
A5: diameter S.0=d.0 by Def2;
A6: S.0 is bounded by Def1;
S.n c= S.0 by A1,PROB_1:def 4;
then d.n<=d.0 by A6,A4,A5,TBSP_1:24;
hence d.n<d.0+1 by A3,XXREAL_0:2;
end;
now
let m,n be Nat such that
m in dom d and
n in dom d and
A7: m <= n;
A8: S.m is bounded by Def1;
A9: diameter S.m=d.m by Def2;
A10: diameter S.n=d.n by Def2;
S.n c= S.m by A1,A7,PROB_1:def 4;
hence d.n<=d.m by A8,A10,A9,TBSP_1:24;
end;
hence thesis by A2,SEQM_3:def 4,SEQ_2:def 3;
end;
theorem
for M be Reflexive non empty MetrStruct
for S be pointwise_bounded SetSequence of M st
S is non-descending holds diameter S is non-decreasing
proof
let M be Reflexive non empty MetrStruct;
let S be pointwise_bounded SetSequence of M such that
A1: S is non-descending;
set d=diameter S;
now
let m,n be Nat such that
m in dom d and
n in dom d and
A2: m <= n;
A3: S.n is bounded by Def1;
A4: diameter S.m=d.m by Def2;
A5: diameter S.n=d.n by Def2;
S.m c= S.n by A1,A2,PROB_1:def 5;
hence d.n>=d.m by A3,A5,A4,TBSP_1:24;
end;
hence thesis by SEQM_3:def 3;
end;
theorem Th4:
for M be non empty Reflexive MetrStruct for S be pointwise_bounded
SetSequence of M st S is non-ascending & 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 pointwise_bounded SetSequence of M such that
A1: S is non-ascending and
A2: lim diameter S = 0;
set d=diameter S;
A3: d is non-increasing by A1,Th2;
A4: d is bounded_below by Th1;
let F be sequence of M such that
A5: for i holds F.i in S.i;
let r;
assume r>0;
then consider n be Nat such that
A6: for m be Nat st n <= m holds |.d.m-0 .| < r by A2,A4,A3,
SEQ_2:def 7;
take n;
let m1,m2 be Nat such that
A7: n <= m1 and
A8: n <= m2;
A9: S.m2 c= S.n by A1,A8,PROB_1:def 4;
A10: F.m2 in S.m2 by A5;
A11: F.m1 in S.m1 by A5;
A12: |.d.n-0 .|<r by A6;
A13: diameter S.n=d.n by Def2;
A14: S.n is bounded by Def1;
then 0 <= d.n by A13,TBSP_1:21;
then
A15: d.n < r by A12,ABSVALUE:def 1;
S.m1 c= S.n by A1,A7,PROB_1:def 4;
then dist(F.m1,F.m2)<=d.n by A9,A11,A10,A14,A13,TBSP_1:def 8;
hence thesis by A15,XXREAL_0:2;
end;
theorem Th5:
for M be Reflexive symmetric triangle non empty MetrStruct for p
be Point of M holds 0 <= r implies diameter cl_Ball(p,r) <= 2*r
proof
let M be Reflexive symmetric triangle non empty MetrStruct;
let p be Point of M;
A1: dist(p,p)=0 by METRIC_1:1;
assume 0 <= r;
then
A2: p in cl_Ball(p,r) by A1,METRIC_1:12;
A3: now
let x,y be Point of M such that
A4: x in cl_Ball(p,r) and
A5: y in cl_Ball(p,r);
A6: dist(x,p)<=r by A4,METRIC_1:12;
A7: dist(x,y)<=dist(x,p)+dist(p,y) by METRIC_1:4;
dist(p,y)<=r by A5,METRIC_1:12;
then dist(x,p)+dist(p,y)<=r+r by A6,XREAL_1:7;
hence dist(x,y)<=2*r by A7,XXREAL_0:2;
end;
cl_Ball(p,r) is bounded by TOPREAL6:59;
hence thesis by A2,A3,TBSP_1:def 8;
end;
definition
let M be MetrStruct;
let U be Subset of M;
attr U is open means
U in Family_open_set M;
end;
definition
let M be MetrStruct;
let A be Subset of M;
attr A is closed means
A` is open;
end;
registration
let M be MetrStruct;
cluster empty -> open for Subset of M;
coherence
proof
let S be Subset of M;
A1: TopSpaceMetr(M) = TopStruct (#the carrier of M,Family_open_set M#);
assume S is empty;
then S in Family_open_set M by A1,PRE_TOPC:1;
hence thesis;
end;
cluster empty -> closed for Subset of M;
coherence
proof
let S be Subset of M;
assume S is empty;
then
A2: [#]M = S`;
[#]M in Family_open_set M by PCOMPS_1:30;
then [#]M is open;
hence thesis by A2;
end;
end;
registration
let M be non empty MetrStruct;
cluster open non empty for Subset of M;
existence
proof
[#]M in Family_open_set M by PCOMPS_1:30;
then [#]M is open;
hence thesis;
end;
cluster closed non empty for Subset of M;
existence
proof
({}M)` is closed;
hence thesis;
end;
end;
theorem Th6:
for M be MetrStruct for A be Subset of M, A9 be Subset of
TopSpaceMetr M st A9 = A holds ( A is open iff A9 is open ) & ( A is closed iff
A9 is closed )
proof
let M be MetrStruct;
let A be Subset of M, A9 be Subset of TopSpaceMetr M such that
A1: A9 = A;
thus A is open implies A9 is open
by A1,PRE_TOPC:def 2;
thus A9 is open implies A is open
by PRE_TOPC:def 2,A1;
thus A is closed implies A9 is closed
proof
assume A is closed;
then A` is open;
then A` in Family_open_set M;
then A9` is open by A1,PRE_TOPC:def 2;
hence thesis by TOPS_1:3;
end;
assume A9 is closed;
then A` in Family_open_set M by A1,PRE_TOPC:def 2;
then A` is open;
hence thesis;
end;
definition
let T be TopStruct;
let S be SetSequence of T;
attr S is open means
for i holds S.i is open;
attr S is closed means
:Def6:
for i holds S.i is closed;
end;
Lm1: for T be TopSpace ex S be SetSequence of T st S is open & S is closed & (
T is non empty implies S is non-empty)
proof
let T be TopSpace;
take S = NAT --> [#]T;
A1: for i holds S.i is closed by FUNCOP_1:7,ORDINAL1:def 12;
for i holds S.i is open by FUNCOP_1:7,ORDINAL1:def 12;
hence S is open & S is closed by A1;
assume T is non empty;
then for x being object st x in dom S holds S.x is non empty by FUNCOP_1:7;
hence thesis by FUNCT_1:def 9;
end;
registration
let T be TopSpace;
cluster open for SetSequence of T;
existence
proof
ex S be SetSequence of T st S is open & S is closed & (T is non empty
implies S is non-empty) by Lm1;
hence thesis;
end;
cluster closed for SetSequence of T;
existence
proof
ex S be SetSequence of T st S is open & S is closed & (T is non empty
implies S is non-empty) by Lm1;
hence thesis;
end;
end;
registration
let T be non empty TopSpace;
cluster open non-empty for SetSequence of T;
existence
proof
ex S be SetSequence of T st S is open & S is closed & (T is non empty
implies S is non-empty) by Lm1;
hence thesis;
end;
cluster closed non-empty for SetSequence of T;
existence
proof
ex S be SetSequence of T st S is open & S is closed & (T is non empty
implies S is non-empty) by Lm1;
hence thesis;
end;
end;
definition
let M be MetrStruct;
let S be SetSequence of M;
attr S is open means
for i holds S.i is open;
attr S is closed means
:Def8:
for i holds S.i is closed;
end;
registration
let M be non empty MetrSpace;
cluster non-empty pointwise_bounded open for SetSequence of M;
existence
proof
consider x being object such that
A1: x in the carrier of M by XBOOLE_0:def 1;
reconsider x as Point of M by A1;
set B=Ball(x,1);
take S = NAT --> B;
A2: now
let y be object;
assume y in dom S;
then reconsider n=y as Element of NAT;
A3: B=S.n by FUNCOP_1:7;
dist(x,x)=0 by METRIC_1:1;
hence S.y is non empty by A3,METRIC_1:11;
end;
A4: now
let i;
i in NAT by ORDINAL1:def 12;
then
A5: S.i=B by FUNCOP_1:7;
B in Family_open_set(M) by PCOMPS_1:29;
hence S.i is open by A5;
end;
for i holds S.i is bounded by FUNCOP_1:7,ORDINAL1:def 12;
hence thesis by A2,A4,FUNCT_1:def 9;
end;
cluster non-empty pointwise_bounded closed for SetSequence of M;
existence
proof
consider x being object such that
A6: x in the carrier of M by XBOOLE_0:def 1;
reconsider x as Point of M by A6;
set B=cl_Ball(x,1);
take S = NAT --> B;
A7: now
let y be object;
assume y in dom S;
then reconsider n=y as Element of NAT;
A8: B=S.n by FUNCOP_1:7;
dist(x,x)=0 by METRIC_1:1;
hence S.y is non empty by A8,METRIC_1:12;
end;
A9: now
let i;
i in NAT by ORDINAL1:def 12;
then
A10: S.i=B by FUNCOP_1:7;
[#]M\B in Family_open_set(M) by NAGATA_1:14;
then B` is open;
hence S.i is closed by A10;
end;
now
let i;
A11: i in NAT by ORDINAL1:def 12;
B is bounded by TOPREAL6:59;
hence S.i is bounded by A11,FUNCOP_1:7;
end;
hence thesis by A7,A9,FUNCT_1:def 9;
end;
end;
theorem Th7:
for M be MetrStruct for S be SetSequence of M, S9 be SetSequence
of TopSpaceMetr M st S9 = S holds ( S is open iff S9 is open ) & ( S is closed
iff S9 is closed )
proof
let M be MetrStruct;
let S be SetSequence of M, S9 be SetSequence of TopSpaceMetr M such that
A1: S9 = S;
thus S is open implies S9 is open
proof
assume
A2: S is open;
let i;
S.i is open by A2;
hence thesis by A1,Th6;
end;
thus S9 is open implies S is open
proof
assume
A3: S9 is open;
let i;
S9.i is open by A3;
hence thesis by A1,Th6;
end;
thus S is closed implies S9 is closed
proof
assume
A4: S is closed;
let i;
S.i is closed by A4;
hence thesis by A1,Th6;
end;
assume
A5: S9 is closed;
let i;
S9.i is closed by A5;
hence thesis by A1,Th6;
end;
theorem Th8:
for M be Reflexive symmetric triangle non empty MetrStruct for S,
CL be Subset of M st S is bounded for S9 be Subset of TopSpaceMetr M st S = S9
& CL = Cl S9 holds CL is bounded & diameter S = diameter CL
proof
let M be Reflexive symmetric triangle non empty MetrStruct;
let S,CL be Subset of M such that
A1: S is bounded;
set d=diameter S;
set T=TopSpaceMetr M;
let S9 be Subset of T such that
A2: S = S9 and
A3: CL = Cl S9;
per cases;
suppose
A4: S<>{};
A5: now
let x,y be Point of M such that
A6: x in CL and
A7: y in CL;
reconsider X=x,Y=y as Point of T;
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;
assume dist(x,y) > d;
then dd > d-d by XREAL_1:14;
then
A8: dd2>0/2 by XREAL_1:74;
By in Family_open_set M by PCOMPS_1:29;
then
A9: BY is open by PRE_TOPC:def 2;
Bx in Family_open_set M by PCOMPS_1:29;
then
A10: BX is open by PRE_TOPC:def 2;
dist(y,y)=0 by METRIC_1:1;
then Y in BY by A8,METRIC_1:11;
then BY meets S9 by A3,A7,A9,TOPS_1:12;
then consider y1 be object such that
A11: y1 in BY and
A12: y1 in S9 by XBOOLE_0:3;
dist(x,x)=0 by METRIC_1:1;
then X in BX by A8,METRIC_1:11;
then BX meets S9 by A3,A6,A10,TOPS_1:12;
then consider x1 be object such that
A13: x1 in BX and
A14: x1 in S9 by XBOOLE_0:3;
reconsider x1,y1 as Point of M by A13,A11;
A15: dist(x,x1)<dd2 by A13,METRIC_1:11;
dist(x1,y1)<=d by A1,A2,A14,A12,TBSP_1:def 8;
then
A16: dist(x,x1)+dist(x1,y1)<dd2+ d by A15,XREAL_1:8;
A17: dist(y,y1)<dd2 by A11,METRIC_1:11;
dist(x,y1)<=dist(x,x1)+dist(x1,y1) by METRIC_1:4;
then dist(x,y1)<dd2+d by A16,XXREAL_0:2;
then dist(x,y1)+dist(y1,y)< dd2+d+ dd2 by A17,XREAL_1:8;
hence contradiction by METRIC_1:4;
end;
A18: now
A19: d+0<d+1 by XREAL_1:8;
let x,y be Point of M such that
A20: x in CL and
A21: y in CL;
dist(x,y)<=d by A5,A20,A21;
hence dist(x,y) <= d+1 by A19,XXREAL_0:2;
end;
A22: now
let s such that
A23: for x,y be Point of M st x in CL & y in CL holds dist(x,y)<=s;
now
let x,y be Point of M such that
A24: x in S and
A25: y in S;
S c= CL by A2,A3,PRE_TOPC:18;
hence dist(x,y)<=s by A23,A24,A25;
end;
hence d <= s by A1,A4,TBSP_1:def 8;
end;
A26: CL<>{} by A2,A3,A4,PCOMPS_1:2;
d+1>0+0 by A1,TBSP_1:21,XREAL_1:8;
then CL is bounded by A18;
hence thesis by A26,A5,A22,TBSP_1:def 8;
end;
suppose
S={};
hence thesis by A2,A3,PCOMPS_1:2;
end;
end;
begin :: Cantor's theorem on complete spaces
theorem Th9:
for M be non empty MetrSpace for C be sequence of M ex S be
non-empty closed SetSequence of M st S is non-ascending & ( C is Cauchy implies
S is pointwise_bounded & lim diameter S = 0 ) &
for i ex U be Subset of TopSpaceMetr M st
U = { C.j where j is Nat: j >= 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[object,object] means
for i st i=$1 ex S be Subset of T st S={C.j where j
is Nat: j >= i} & $2=Cl S;
A1: for x being object st x in NAT
ex y being object st y in bool the carrier of M & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider x9=x as Nat;
set S={C.j where j is Nat: j >= x9};
S c= the carrier of T
proof
let y be object;
assume y in S;
then ex j be Nat st C.j=y & j>=x9;
hence thesis;
end;
then reconsider S as Subset of T;
take Cl S;
thus thesis;
end;
consider S be SetSequence of M such that
A2: for x being object st x in NAT holds P[x,S.x] from FUNCT_2:sch 1(A1);
A3: now
let x be object;
assume x in dom S;
then reconsider i=x as Element of NAT;
consider U be Subset of T such that
A4: U={C.j where j is Nat: j >= i} and
A5: S.i=Cl U by A2;
A6: U c= S.i by A5,PRE_TOPC:18;
C.i in U by A4;
hence S.x is non empty by A6;
end;
now
let i;
i in NAT by ORDINAL1:def 12;
then
ex U be Subset of T st U={C.j where j is Nat: j >= i} & S.
i=Cl U by A2;
hence S.i is closed by Th6;
end;
then reconsider S as non-empty closed SetSequence of M by A3,Def8,
FUNCT_1:def 9;
take S;
now
let i be Nat;
i in NAT by ORDINAL1:def 12;
then consider U be Subset of T such that
A7: U={C.j where j is Nat: j >= i} and
A8: S.i=Cl U by A2;
consider U1 be Subset of T such that
A9: U1={C.j where j is Nat: j >= i+1} and
A10: S.(i+1)=Cl U1 by A2;
U1 c= U
proof
let x be object;
assume x in U1;
then consider j be Nat such that
A11: x=C.j and
A12: j>=i+1 by A9;
j>= i by A12,NAT_1:13;
hence thesis by A7,A11;
end;
hence S.(i+1) c= S.i by A8,A10,PRE_TOPC:19;
end;
hence
A13: S is non-ascending by KURATO_0:def 3;
thus C is Cauchy implies S is pointwise_bounded & lim diameter S = 0
proof
assume
A14: C is Cauchy;
A15: now
let i;
i in NAT by ORDINAL1:def 12;
then consider U be Subset of T such that
A16: U={C.j where j is Nat: j >= i} and
A17: S.i=Cl U by A2;
reconsider U9=U as Subset of M;
U c= rng C
proof
let x be object;
assume x in U;
then consider j be Nat such that
A18: x=C.j & j>=i by A16;
A19: j in NAT by ORDINAL1:def 12;
dom C=NAT by FUNCT_2:def 1;
hence thesis by A18,FUNCT_1:def 3,A19;
end;
then U9 is bounded by A14,TBSP_1:14,26;
hence S.i is bounded by A17,Th8;
end;
then reconsider S9=S as non-empty pointwise_bounded closed SetSequence of M
by Def1;
set d=diameter S9;
A20: for r be Real st 0<r ex n be Nat st for m be
Nat st n<=m holds |.d.m-0 .|<r
proof
let r be Real such that
A21: 0<r;
reconsider R=r as Real;
set R2=R/2;
R2>0 by A21,XREAL_1:139;
then consider p be Nat such that
A22: for n,m be Nat st p<=n & p<=m holds dist(C.n,C.m)<R2
by A14;
take p;
let m be Nat such that
A23: p<=m;
m in NAT by ORDINAL1:def 12;
then consider U be Subset of T such that
A24: U={C.j where j is Nat: j >= m} and
A25: S.m=Cl U by A2;
reconsider U9=U as Subset of M;
A26: now
let x,y being Point of M such that
A27: x in U9 and
A28: y in U9;
consider j be Nat such that
A29: y=C.j and
A30: j>=m by A24,A28;
A31: j>=p by A23,A30,XXREAL_0:2;
consider i be Nat such that
A32: x = C.i and
A33: i>=m by A24,A27;
i>=p by A23,A33,XXREAL_0:2;
hence dist(x,y)<=R2 by A22,A32,A29,A31;
end;
A34: U c= rng C
proof
let x be object;
assume x in U;
then consider j be Nat such that
A35: x=C.j & j>=m by A24;
A36: j in NAT by ORDINAL1:def 12;
dom C=NAT by FUNCT_2:def 1;
hence thesis by A35,FUNCT_1:def 3,A36;
end;
then
A37: U9 is bounded by A14,TBSP_1:14,26;
then
A38: diameter U9=diameter S.m by A25,Th8;
C.m in U by A24;
then
A39: diameter U9<=R2 by A37,A26,TBSP_1:def 8;
rng C is bounded by A14,TBSP_1:26;
then diameter S.m>=0 by A34,A38,TBSP_1:14,21;
then
A40: |.diameter S.m.|<=R2 by A39,A38,ABSVALUE:def 1;
R2<R by A21,XREAL_1:216;
then |.diameter S.m.|<R by A40,XXREAL_0:2;
hence thesis by Def2;
end;
thus S is pointwise_bounded by A15;
A41: d is bounded_below by Th1;
d is non-increasing by A13,Th2;
hence thesis by A41,A20,SEQ_2:def 7;
end;
let i;
i in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
theorem Th10:
for M be non empty MetrSpace holds M is complete iff for S be
non-empty pointwise_bounded closed SetSequence of M st S is non-ascending &
lim diameter S = 0 holds meet S is non empty
proof
let M be non empty MetrSpace;
set T=TopSpaceMetr(M);
thus M is complete implies
for S be non-empty pointwise_bounded closed SetSequence of
M st S is non-ascending & lim diameter S = 0 holds meet S is non empty
proof
assume
A1: M is complete;
let S be non-empty pointwise_bounded closed SetSequence of M such that
A2: S is non-ascending and
A3: lim diameter S = 0;
defpred P[object,object] means $2 in S.$1;
:: Funkcja Kuratowskiego !!!
A4: for x being object st x in NAT
ex y being object st y in the carrier of M & P[x,y]
proof
A5: dom S=NAT by FUNCT_2:def 1;
let x being object such that
A6: x in NAT;
S.x is non empty by A6,A5,FUNCT_1:def 9;
then
A7: ex y being object st y in S.x by XBOOLE_0:def 1;
S.x in rng S by A6,A5,FUNCT_1:def 3;
hence thesis by A7;
end;
consider F be sequence of the carrier of M such that
A8: for x being object st x in NAT holds P[x,F.x] from FUNCT_2:sch 1(A4);
for i holds F.i in S.i by A8,ORDINAL1:def 12;
then F is Cauchy by A2,A3,Th4;
then F is convergent by A1;
then consider x be Point of M such that
A9: F is_convergent_in_metrspace_to x by METRIC_6:10;
reconsider F9 = F as sequence of T;
reconsider x9 = x as Point of T;
now
let i be Nat;
set F1=F9^\i;
reconsider Si=S.i as Subset of T;
A10: rng F1 c= Si
proof
let x be object;
assume x in rng F1;
then consider y being object such that
A11: y in dom F1 and
A12: F1.y=x by FUNCT_1:def 3;
reconsider y as Element of NAT by A11;
i<=y+i by NAT_1:11;
then
A13: S.(y+i) c= S.i by A2,PROB_1:def 4;
A14: y+i in NAT by ORDINAL1:def 12;
x=F.(y+i) by A12,NAT_1:def 3;
then x in S.(y+i) by A8,A14;
hence thesis by A13;
end;
F9 is_convergent_to x9 by A9,FRECHET2:28;
then F1 is_convergent_to x9 by FRECHET2:15;
then
A15: x in Lim F1 by FRECHET:def 5;
S.i is closed by Def8;
then Si is closed by Th6;
then Lim F1 c= Si by A10,FRECHET2:9;
hence x in S.i by A15;
end;
hence thesis by KURATO_0:3;
end;
assume
A16: for S be non-empty pointwise_bounded closed SetSequence of M st S is
non-ascending & lim diameter S = 0 holds meet S is non empty;
let F be sequence of M such that
A17: F is Cauchy;
consider S be non-empty closed SetSequence of M such that
A18: S is non-ascending and
A19: F is Cauchy implies S is pointwise_bounded & lim diameter S = 0 and
A20: for i ex U be Subset of T st U={ F.j where j is Nat:j >=
i} & S.i = Cl U by Th9;
set d=diameter S;
A21: d is non-increasing by A17,A18,A19,Th2;
meet S is non empty by A16,A17,A18,A19;
then consider x being object such that
A22: x in meet S by XBOOLE_0:def 1;
A23: d is bounded_below by A17,A19,Th1;
reconsider x as Point of M by A22;
take x;
let r;
assume r>0;
then consider n be Nat such that
A24: for m be Nat st n<=m holds |.d.m-0 .|<r by A17,A19,A23,A21,
SEQ_2:def 7;
take n;
let m be Nat;
assume n<=m;
then
A25: |.d.m-0 .|<r by A24;
A26: S.m is bounded by A17,A19;
A27: x in S.m by A22,KURATO_0:3;
A28: diameter (S.m)=d.m by Def2;
consider U be Subset of T such that
A29: U = { F.j where j is Nat: j >= m } and
A30: S.m = Cl U by A20;
A31: U c= Cl U by PRE_TOPC:18;
F.m in U by A29;
then
A32: dist(F.m,x) <= diameter (S.m) by A30,A31,A27,A26,TBSP_1:def 8;
diameter (S.m)>=0 by A26,TBSP_1:21;
then d.m <r by A28,A25,ABSVALUE:def 1;
hence thesis by A32,A28,XXREAL_0:2;
end;
theorem Th11:
for T be non empty TopSpace for S be non-empty SetSequence of T
st S is non-ascending for F be Subset-Family of T st F = rng S holds F is
centered
proof
let T be non empty TopSpace;
let S be non-empty SetSequence of T such that
A1: S is non-ascending;
let F be Subset-Family of T such that
A2: F = rng S;
A3: now
defpred P[object,object] means $1=S.$2;
:: !!!
let G be set such that
A4: G <> {} and
A5: G c= F and
A6: G is finite;
A7: for x being object st x in G ex y being object st y in NAT & P[x,y]
proof
let x be object;
assume x in G;
then ex y being object st y in dom S & S.y=x by A2,A5,FUNCT_1:def 3;
hence thesis;
end;
consider f be Function of G,NAT such that
A8: for x being object st x in G holds P[x,f.x] from FUNCT_2:sch 1(A7);
consider i be Nat such that
A9: for j be Nat st j in rng f holds j<=i by A6,STIRL2_1:56;
A10: i in NAT by ORDINAL1:def 12;
dom S=NAT by FUNCT_2:def 1;
then S.i<>{} by A10,FUNCT_1:def 9;
then consider x being object such that
A11: x in S.i by XBOOLE_0:def 1;
A12: dom f=G by FUNCT_2:def 1;
now
let Y be set;
assume
A13: Y in G;
then
A14: f.Y in rng f by A12,FUNCT_1:def 3;
reconsider fY=f.Y as Nat;
A15: fY <= i by A9,A14;
Y=S.fY by A8,A13;
then S.i c= Y by A1,A15,PROB_1:def 4;
hence x in Y by A11;
end;
hence meet G<>{} by A4,SETFAM_1:def 1;
end;
dom S=NAT by FUNCT_2:def 1;
then F<>{} by A2,RELAT_1:42;
hence thesis by A3,FINSET_1:def 3;
end;
theorem Th12:
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 being object such that
A3: x in dom S and
A4: S.x=P by A1,FUNCT_1:def 3;
reconsider x as Nat by A3;
S.x is open by A2;
hence thesis by A4,Th6;
end;
assume
A5: S is closed;
let P be Subset of T;
assume P in F;
then consider x being object such that
A6: x in dom S and
A7: S.x=P by A1,FUNCT_1:def 3;
reconsider x as Nat by A6;
S.x is closed by A5;
hence thesis by A7,Th6;
end;
theorem Th13:
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 non-ascending &
( 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 be object;
assume x in {S.j where j is Element of NAT : j <= i};
then consider j be Element of NAT such that
A3: x=S.j & j<=i;
dom S=NAT by FUNCT_2:def 1;
then x in rng S by A3,FUNCT_1:def 3;
hence thesis by A1;
end;
defpred P[object,object] means
for i st i=$1 holds $2=meet {S.j where j is Element
of NAT:j<=i};
A4: for x being object st x in NAT
ex y being object st y in bool(the carrier of T) & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider i=x as Element of NAT;
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
A5: for x being object st x in NAT holds P[x,R.x] from FUNCT_2:sch 1(A4);
take R;
now
let i be Nat;
A6: i in NAT by ORDINAL1:def 12;
set SS={S.j where j is Element of NAT:j<=i};
set S1={S.j where j is Element of NAT:j<=i+1};
A7: SS c= S1
proof
let x be object;
assume x in SS;
then consider j be Element of NAT such that
A8: x=S.j and
A9: j<=i;
j<=i+1 by A9,NAT_1:13;
hence thesis by A8;
end;
A10: meet SS=R.i by A5,A6;
S.0 in SS;
then meet S1 c= meet SS by A7,SETFAM_1:6;
hence R.(i+1) c= R.i by A5,A10;
end;
hence R is non-ascending by KURATO_0:def 3;
A11: for i holds {S.j where j is Element of NAT:j<=i} is finite
proof
deffunc F(set)=S.$1;
let i;
set SS={S.j where j is Element of NAT:j<=i};
A12: SS c= {F(j)where j is Element of NAT:j in i+1}
proof
let x be object;
assume x in SS;
then consider j be Element of NAT such that
A13: x=S.j and
A14: j<=i;
j<i+1 by A14,NAT_1:13;
then j in Segm(i+1) by NAT_1:44;
hence thesis by A13;
end;
A15: i+1 is finite;
{F(j)where j is Element of NAT:j in i+1} is finite from FRAENKEL:sch
21(A15);
hence thesis by A12;
end;
thus F is centered implies R is non-empty
proof
assume
A16: F is centered;
now
let x be object;
assume x in dom R;
then reconsider i=x as Element of NAT;
set SS={S.j where j is Element of NAT:j<=i};
A17: S.0 in SS;
A18: SS c= F by A2;
SS is finite by A11;
then meet SS<>{} by A16,A17,A18,FINSET_1:def 3;
hence R.x is non empty by A5;
end;
hence thesis by FUNCT_1:def 9;
end;
thus F is open implies R is open
proof
assume
A19: F is open;
let i;
set SS={S.j where j is Element of NAT:j<=i};
A20: SS c= F by A2;
then reconsider SS as Subset-Family of T by XBOOLE_1:1;
SS is finite by A11;
then
A21: meet SS is open by A19,A20,TOPS_2:11,20;
i in NAT by ORDINAL1:def 12;
hence thesis by A5,A21;
end;
thus F is closed implies R is closed
proof
assume
A22: F is closed;
let i;
set SS={S.j where j is Element of NAT:j<=i};
A23: i in NAT by ORDINAL1:def 12;
A24: SS c= F by A2;
then reconsider SS as Subset-Family of T by XBOOLE_1:1;
meet SS is closed by A22,A24,TOPS_2:12,22;
hence thesis by A5,A23;
end;
let i;
i in NAT by ORDINAL1:def 12;
hence thesis by A5;
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
reconsider NULL=0 as Real;
deffunc F(Nat)=1/(1+$1);
assume
A1: M is complete;
consider seq be Real_Sequence such that
A2: for n be Nat holds seq.n=F(n) from SEQ_1:sch 1;
set Ns=NULL(#)seq;
let F be Subset-Family of T such that
A3: F is closed and
A4: F is centered and
A5: for r st r>0 ex A be Subset of M st A in F & A is bounded & diameter A<r;
A6: for n be Nat holds seq.n=1/(n+1) by A2;
then
A7: Ns is convergent by SEQ_2:7,SEQ_4:31;
defpred P[object,object] means
for i st i=$1 for A be Subset of M st A=$2 holds
A in F & A is bounded & diameter A <1/(i+1);
A8: for x being object st x in NAT
ex y being object st y in bool(the carrier of M) & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider i=x as Nat;
consider A be Subset of M such that
A9: A in F and
A10: A is bounded and
A11: diameter A < 1/(i+1) by A5,XREAL_1:139;
take A;
thus thesis by A9,A10,A11;
end;
consider f be SetSequence of M such that
A12: for x being object st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A8);
rng f c= F
proof
let x be object;
assume x in rng f;
then consider y being object such that
A13: y in dom f and
A14: f.y=x by FUNCT_1:def 3;
reconsider y as Element of NAT by A13;
f.y in F by A12;
hence thesis by A14;
end;
then consider R be SetSequence of T such that
A15: R is non-ascending and
A16: F is centered implies R is non-empty and
F is open implies R is open and
A17: F is closed implies R is closed and
A18: for i holds R.i = meet {f.j where j is Element of NAT: j<=i} by Th13;
reconsider R9=R as non-empty SetSequence of M by A4,A16;
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:3;
then R.i c= f.0 by A18;
hence R9.i is bounded by A12,TBSP_1:14;
end;
then reconsider R9 as non-empty pointwise_bounded SetSequence of M by Def1;
set dR=diameter R9;
A19: now
let n be Nat;
A20: n in NAT by ORDINAL1:def 12;
set Sn={f.j where j is Element of NAT:j<=n};
A21: f.n in Sn by A20;
R.n=meet Sn by A18;
then
A22: R.n c= f.n by A21,SETFAM_1:3;
then diameter R9.n <= diameter f.n by A12,TBSP_1:24,A20;
then
A23: diameter R9.n <= F(n) by A12,XXREAL_0:2,A20;
f.n is bounded by A12,A20;
then
A24: 0<= diameter R9.n by A22,TBSP_1:14,21;
A25: Ns.n=NULL*seq.n by SEQ_1:9;
F(n)=seq.n by A2;
hence Ns.n <= dR.n & dR.n<=seq.n by A24,A23,A25,Def2;
end;
A26: lim seq=0 by A6,SEQ_4:31;
then
A27: lim Ns=NULL*0 by A6,SEQ_2:8,SEQ_4:31;
A28: seq is convergent by A6,SEQ_4:31;
then
A29: lim dR=0 by A26,A7,A27,A19,SEQ_2:20;
A30: R9 is closed by A3,A17,Th7;
then meet R9<>{} by A1,A15,A29,Th10;
then consider x0 be object such that
A31: x0 in meet R9 by XBOOLE_0:def 1;
reconsider x0 as Point of M by A31;
A32: dR is convergent by A28,A26,A7,A27,A19,SEQ_2:19;
A33: now
let y;
assume
A34: y in F;
then reconsider Y=y as Subset of T;
defpred P9[object,object] means
for i st i=$1 holds $2=R.i/\Y;
A35: for x being object st x in NAT
ex z be object st z in bool(the carrier of M) & P9[x ,z]
proof
let x be object;
assume x in NAT;
then reconsider i=x as Nat;
take R.i/\Y;
thus thesis;
end;
consider f9 be SetSequence of M such that
A36: for x being object st x in NAT holds P9[x,f9.x] from FUNCT_2:sch 1(A35);
A37: now
deffunc F(object)=f.$1;
let x be object;
assume x in dom f9;
then reconsider i=x as Element of NAT;
set SS={f.j where j is Element of NAT:j<=i};
A38: f.i in SS;
A39: SS c= {F(j) where j is Element of NAT:j in i+1}
proof
let x be object;
assume x in SS;
then consider j be Element of NAT such that
A40: x=f.j and
A41: j<=i;
j<i+1 by A41,NAT_1:13;
then j in Segm(i+1) by NAT_1:44;
hence thesis by A40;
end;
A42: {Y}\/SS c= F
proof
let z be object such that
A43: z in {Y}\/SS;
per cases by A43,XBOOLE_0:def 3;
suppose
z in {Y};
hence thesis by A34,TARSKI:def 1;
end;
suppose
z in SS;
then ex j be Element of NAT st z=f.j & j<=i;
hence thesis by A12;
end;
end;
A44: i+1 is finite;
{F(j)where j is Element of NAT:j in i+1} is finite from FRAENKEL:
sch 21(A44);
then meet({Y}\/SS)<>{} by A4,A42,A39,FINSET_1:def 3;
then meet {Y} /\ meet SS <> {} by A38,SETFAM_1:9;
then Y /\meet SS<>{} by SETFAM_1:10;
then Y/\R.i<>{} by A18;
hence f9.x is non empty by A36;
end;
A45: now
let i;
reconsider Ri=R.i as Subset of T;
i in NAT by ORDINAL1:def 12;
then
A46: f9.i=Ri/\Y by A36;
R9.i is closed by A30;
then
A47: Ri is closed by Th6;
Y is closed by A3,A34;
hence f9.i is closed by A47,A46,Th6;
end;
now
let i;
i in NAT by ORDINAL1:def 12;
then
A48: f9.i=R9.i /\ Y by A36;
R9.i is bounded by Def1;
hence f9.i is bounded by A48,TBSP_1:14,XBOOLE_1:17;
end;
then reconsider f9 as non-empty pointwise_bounded closed SetSequence of M
by A37,A45,Def1,Def8,FUNCT_1:def 9;
A49: f9.0=R.0/\Y by A36;
set df=diameter f9;
now
reconsider Y9=Y as Subset of M;
let n be Nat;
A50: Ns.n=NULL*seq.n by SEQ_1:9;
n in NAT by ORDINAL1:def 12;
then
A51: R.n/\Y9=f9.n by A36;
A52: R9.n is bounded by Def1;
then diameter f9.n <= diameter R9.n by A51,TBSP_1:24,XBOOLE_1:17;
then
A53: diameter f9.n <= dR.n by Def2;
R.n/\Y c= R.n by XBOOLE_1:17;
then 0<=diameter f9.n by A52,A51,TBSP_1:14,21;
hence Ns.n <= df.n & df.n<=dR.n by A53,A50,Def2;
end;
then
A54: lim df=0 by A7,A27,A32,A29,SEQ_2:20;
now
let i be Nat;
i in NAT by ORDINAL1:def 12;
then
A55: f9.i = R.i/\Y by A36;
A56: R.(i+1) c= R.i by A15,KURATO_0:def 3;
f9.(i+1) =R.(i+1)/\Y by A36;
hence f9.(i+1) c= f9.i by A55,A56,XBOOLE_1:26;
end;
then f9 is non-ascending by KURATO_0:def 3;
then meet f9<>{} by A1,A54,Th10;
then consider z be object such that
A57: z in meet f9 by XBOOLE_0:def 1;
reconsider z as Point of M by A57;
A58: 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 Nat such that
A59: for j be Nat st i<=j holds |.dR.j-0.|<dist(x0,z)
by A32,A29,SEQ_2:def 7;
A60: i in NAT by ORDINAL1:def 12;
A61: f9.i=R.i/\Y by A36,A60;
z in f9.i by A57,KURATO_0:3;
then
A62: z in R.i by A61,XBOOLE_0:def 4;
A63: R9.i is bounded by Def1;
then
A64: 0<=diameter (R9.i) by TBSP_1:21;
x0 in R.i by A31,KURATO_0:3;
then dist(x0,z)<=diameter (R9.i) by A62,A63,TBSP_1:def 8;
then
A65: |.diameter (R9.i).|>=dist(x0,z) by A64,ABSVALUE:def 1;
|.dR.i-0.|<dist(x0,z) by A59;
hence thesis by A65,Def2;
end;
z in f9.0 by A57,KURATO_0:3;
hence x0 in y by A58,A49,XBOOLE_0:def 4;
end;
F<>{} by A4,FINSET_1:def 3;
hence thesis by A33,SETFAM_1:def 1;
end;
assume
A66: 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;
now
let S be non-empty pointwise_bounded closed SetSequence of M such that
A67: S is non-ascending and
A68: lim diameter S = 0;
reconsider RS=rng S as Subset-Family of T;
A69: now
set d=diameter S;
A70: dom S=NAT by FUNCT_2:def 1;
A71: d is bounded_below by Th1;
A72: d is non-increasing by A67,Th2;
let r;
assume r > 0;
then consider n be Nat such that
A73: for m be Nat st n<=m holds |.d.m-0 .|<r by A68,A71,A72,
SEQ_2:def 7;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
take Sn=S.nn;
A74: d.n=diameter Sn by Def2;
Sn is bounded by Def1;
then
A75: diameter Sn>=0 by TBSP_1:21;
|.d.n-0 .|<r by A73;
hence Sn in RS & Sn is bounded & diameter Sn <r by A74,A75,A70,Def1,
ABSVALUE:def 1,FUNCT_1:def 3;
end;
RS is closed by Th12;
then meet RS is non empty by A66,A67,A69,Th11;
then consider x being object such that
A76: x in meet RS by XBOOLE_0:def 1;
now
let i be Nat;
A77: i in NAT by ORDINAL1:def 12;
dom S=NAT by FUNCT_2:def 1;
then S.i in RS by FUNCT_1:def 3,A77;
hence x in S.i by A76,SETFAM_1:def 1;
end;
hence meet S is non empty by KURATO_0:3;
end;
hence thesis by Th10;
end;
theorem Th15:
for M be non empty MetrSpace,A be non empty Subset of M for B be
Subset of M, B9 be Subset of M|A st B = B9 holds B9 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, B9 be Subset of M|A such that
A1: B = B9;
thus B9 is bounded implies B is bounded by A1,HAUSDORF:17;
assume
A2: B is bounded;
per cases;
suppose
B9={}(M|A);
hence thesis;
end;
suppose
B9<>{}(M|A);
then consider p be object such that
A3: p in B9 by XBOOLE_0:def 1;
reconsider p as Point of (M|A) by A3;
A4: now
let q be Point of (M|A) such that
A5: q in B9;
reconsider p9=p,q9=q as Point of M by TOPMETR:8;
A6: dist(p,q) = dist(p9,q9) by TOPMETR:def 1;
A7: diameter B+0<=diameter B+1 by XREAL_1:8;
dist(p9,q9)<=diameter B by A1,A2,A3,A5,TBSP_1:def 8;
hence dist(p,q)<=diameter B+1 by A6,A7,XXREAL_0:2;
end;
0+0 < diameter B+1 by A2,TBSP_1:21,XREAL_1:8;
hence thesis by A4,TBSP_1:10;
end;
end;
theorem Th16:
for M be non empty MetrSpace,A be non empty Subset of M for B be
Subset of M, B9 be Subset of M|A st B = B9 & B is bounded holds diameter B9 <=
diameter B
proof
let M be non empty MetrSpace,A be non empty Subset of M;
let B be Subset of M, B9 be Subset of M|A such that
A1: B = B9 and
A2: B is bounded;
A3: B9 is bounded by A1,A2,Th15;
per cases;
suppose
A4: B9={}(M|A);
then diameter B9=0 by TBSP_1:def 8;
hence thesis by A1,A4,TBSP_1:def 8;
end;
suppose
A5: B9<>{}(M|A);
now
let x,y be Point of (M|A) such that
A6: x in B9 and
A7: y in B9;
reconsider x9=x,y9=y as Point of M by TOPMETR:8;
dist(x,y) = dist(x9,y9) by TOPMETR:def 1;
hence dist(x,y)<=diameter B by A1,A2,A6,A7,TBSP_1:def 8;
end;
hence thesis by A3,A5,TBSP_1:def 8;
end;
end;
theorem Th17:
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 by TOPMETR:def 2;
hence thesis by FUNCT_2:7;
end;
theorem Th18:
for M be non empty MetrSpace, A be non empty Subset of M for S
be sequence of (M|A),S9 be sequence of M st S = S9 holds S9 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),S9 be sequence of M such that
A1: S = S9;
thus S9 is Cauchy implies S is Cauchy
proof
assume
A2: S9 is Cauchy;
let r;
assume r>0;
then consider p be Nat such that
A3: for n,m be Nat st p<=n & p<=m holds dist(S9.n,S9.m)<r
by A2;
take p;
let n,m be Nat such that
A4: p<=n and
A5: p<=m;
dist(S.n,S.m) = dist(S9.n,S9.m) by A1,TOPMETR:def 1;
hence thesis by A3,A4,A5;
end;
assume
A6: S is Cauchy;
let r;
assume r>0;
then consider p be Nat such that
A7: for n,m be Nat st p<=n & p<=m holds dist(S.n,S.m)<r by A6;
take p;
let n,m be Nat such that
A8: p <= n and
A9: p <= m;
dist(S.n,S.m) = dist(S9.n,S9.m) by A1,TOPMETR:def 1;
hence thesis by A7,A8,A9;
end;
theorem
for M be non empty MetrSpace st M is complete for A be non empty
Subset of M, A9 be Subset of TopSpaceMetr M st A = A9 holds M|A is complete iff
A9 is closed
proof
let M be non empty MetrSpace such that
A1: M is complete;
set T=TopSpaceMetr(M);
let A be non empty Subset of M, A9 be Subset of TopSpaceMetr(M) such that
A2: A = A9;
set MA=M|A;
set TA=TopSpaceMetr(MA);
thus MA is complete implies A9 is closed
proof
assume
A3: MA is complete;
A4: Cl A9 c= A9
proof
let p be object such that
A5: p in Cl A9;
reconsider p as Point of M by A5;
defpred P[object,object] means
for i st i=$1 holds $2=A /\ cl_Ball(p,1/(i+1));
A6: for x being object st x in NAT
ex y being object st y in bool(the carrier of MA) & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider i=x as Nat;
take A/\cl_Ball(p,1/(i+1));
A/\cl_Ball(p,1/(i+1)) c= A by XBOOLE_1:17;
then A/\cl_Ball(p,1/(i+1)) c= the carrier of MA by TOPMETR:def 2;
hence thesis;
end;
consider f be SetSequence of MA such that
A7: for x being object st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A6);
A8: now
let x be object;
assume x in dom f;
then reconsider i=x as Element of NAT;
reconsider B=Ball(p,1/(i+1)) as Subset of T;
Ball(p,1/(i+1)) in Family_open_set M by PCOMPS_1:29;
then
A9: B is open by PRE_TOPC:def 2;
p in B by TBSP_1:11,XREAL_1:139;
then B meets A9 by A5,A9,PRE_TOPC:24;
then consider y being object such that
A10: y in B and
A11: y in A9 by XBOOLE_0:3;
reconsider y as Point of M by A10;
dist(p,y)< 1/(i+1) by A10,METRIC_1:11;
then y in cl_Ball(p,1/(i+1)) by METRIC_1:12;
then y in A/\cl_Ball(p,1/(i+1)) by A2,A11,XBOOLE_0:def 4;
hence f.x is non empty by A7;
end;
A12: now
let i;
reconsider cB=cl_Ball(p,1/(i+1)) as Subset of T;
reconsider fi=f.i as Subset of TA;
A13: i in NAT by ORDINAL1:def 12;
[#]M\cB in Family_open_set(M) by NAGATA_1:14;
then cB` is open by PRE_TOPC:def 2;
then
A14: cB is closed by TOPS_1:3;
A15: TA=T|A9 by A2,HAUSDORF:16;
then [#](T|A9)=A by TOPMETR:def 2;
then fi=cB/\[#](T|A9) by A7,A13;
then fi is closed by A14,A15,PRE_TOPC:13;
hence f.i is closed by Th6;
end;
now
let i;
set ACL=A/\cl_Ball(p,1/(i+1));
cl_Ball(p,1/(i+1)) is bounded by TOPREAL6:59;
then
A16: ACL is bounded by TBSP_1:14,XBOOLE_1:17;
i in NAT by ORDINAL1:def 12;
then f.i=ACL by A7;
hence f.i is bounded by A16,Th15;
end;
then reconsider f as non-empty pointwise_bounded closed SetSequence of MA
by A8,A12,Def1,Def8,FUNCT_1:def 9;
set df=diameter f;
reconsider NULL=0,TWO=2 as Real;
deffunc F(Nat)=1/(1+$1);
consider seq be Real_Sequence such that
A17: for n be Nat holds seq.n=F(n) from SEQ_1:sch 1;
now
let i be Nat;
set i1=i+1;
cl_Ball(p,1/(i1+1)) c= cl_Ball(p,1/i1)
proof
let x be object such that
A18: x in cl_Ball(p,1/(i1+1));
reconsider q=x as Point of M by A18;
i1<i1+1 by NAT_1:13;
then
A19: 1/(i1+1)<1/i1 by XREAL_1:76;
dist(p,q)<=1/(i1+1) by A18,METRIC_1:12;
then dist(p,q)<=1/i1 by A19,XXREAL_0:2;
hence thesis by METRIC_1:12;
end;
then
A20: A/\cl_Ball(p,1/(i1+1)) c= A/\cl_Ball(p,1/i1) by XBOOLE_1:26;
i in NAT by ORDINAL1:def 12;
then f.i=A/\cl_Ball(p,1/i1) by A7;
hence f.(i+1) c= f.i by A7,A20;
end;
then
A21: f is non-ascending by KURATO_0:def 3;
set Ts=TWO(#)seq;
set Ns=NULL(#)seq;
A22: for n be Nat holds seq.n=1/(n+1) by A17;
then
A23: Ns is convergent by SEQ_2:7,SEQ_4:31;
A24: now
let n be Nat;
set cB=cl_Ball(p,1/(n+1));
A25: Ns.n=NULL*seq.n by SEQ_1:9;
A26: Ts.n=TWO*seq.n by SEQ_1:9;
A27: cB is bounded by TOPREAL6:59;
then
A28: A/\cB is bounded by TBSP_1:14,XBOOLE_1:17;
A29: diameter(A/\cB)<= diameter cB by A27,TBSP_1:24,XBOOLE_1:17;
diameter cB <= 2*F(n) by Th5;
then
A30: diameter(A/\cB)<=2*F(n) by A29,XXREAL_0:2;
n in NAT by ORDINAL1:def 12;
then
A31: f.n=A/\cB by A7;
then f.n is bounded by A28,Th15;
then
A32: 0<= diameter f.n by TBSP_1:21;
diameter (f.n) <= diameter(A/\cB) by A28,A31,Th16;
then
A33: diameter f.n <= 2*F(n) by A30,XXREAL_0:2;
F(n)=seq.n by A17;
hence Ns.n <= df.n & df.n<=Ts.n by A32,A33,A25,A26,Def2;
end;
A34: Ts is convergent by A22,SEQ_2:7,SEQ_4:31;
A35: lim seq=0 by A22,SEQ_4:31;
then
A36: lim Ts= TWO*0 by A22,SEQ_2:8,SEQ_4:31;
lim Ns=NULL*0 by A22,A35,SEQ_2:8,SEQ_4:31;
then lim df = 0 by A23,A34,A36,A24,SEQ_2:20;
then meet f is non empty by A3,A21,Th10;
then consider q be object such that
A37: q in meet f by XBOOLE_0:def 1;
reconsider q as Point of M by A37,TOPMETR:8;
A38: seq is convergent by A22,SEQ_4:31;
p = q
proof
assume p <> q;
then dist(p,q)<>0 by METRIC_1:2;
then dist(p,q)>0 by METRIC_1:5;
then consider n be Nat such that
A39: for m be Nat st n<=m holds |.seq.m-0.|<dist(p,q)
by A38,A35,SEQ_2:def 7;
set cB=cl_Ball(p,1/(n+1));
A40: q in f.n by A37,KURATO_0:3;
n in NAT by ORDINAL1:def 12;
then f.n = A/\cB by A7;
then q in cB by A40,XBOOLE_0:def 4;
then
A41: dist(p,q) <= F(n) by METRIC_1:12;
seq.n = F(n) by A17;
then |.seq.n-0.|=F(n) by ABSVALUE:def 1;
hence thesis by A39,A41;
end;
then
A42: p in f.0 by A37,KURATO_0:3;
f.0=A/\cl_Ball(p,1/(0+1)) by A7;
hence thesis by A2,A42,XBOOLE_0:def 4;
end;
A9 c= Cl A9 by PRE_TOPC:18;
hence thesis by A4,XBOOLE_0:def 10;
end;
assume
A43: A9 is closed;
let S be sequence of MA such that
A44: S is Cauchy;
reconsider S9=S as sequence of M by Th17;
S9 is Cauchy by A44,Th18;
then
A45: S9 is convergent by A1;
A46: now
let n be Nat;
S.n in the carrier of (M|A);
hence S9.n in A9 by A2,TOPMETR:def 2;
end;
the carrier of (M|A)=A9 by A2,TOPMETR:def 2;
then reconsider limS=lim S9 as Point of (M|A) by A43,A45,A46,TOPMETR3:1;
take limS;
let r;
assume r>0;
then consider n be Nat such that
A47: for m be Nat st m>=n holds dist(S9.m,lim S9)<r by A45,
TBSP_1:def 3;
take n;
let m be Nat such that
A48: m>=n;
dist(S.m,limS) = dist(S9.m,lim S9) by TOPMETR:def 1;
hence thesis by A47,A48;
end;
begin :: Countable compact spaces
definition
let T be TopStruct;
attr T is countably_compact means
for F being Subset-Family of T st F
is Cover of T & F is open & F is countable ex G being Subset-Family of T st G
c= F & G is Cover of T & G is finite;
end;
theorem
for T be TopStruct st T is compact holds T is countably_compact;
theorem Th21:
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 and
A3: F is closed and
A4: F is countable;
assume
A5: meet F = {};
F <> {} by A2,FINSET_1:def 3;
then union COMPLEMENT(F) = (meet F)` by TOPS_2:7
.= [#] T by A5;
then
A6: COMPLEMENT(F) is Cover of T by SETFAM_1:45;
A7: COMPLEMENT(F) is countable by A4,TOPGEN_4:1;
COMPLEMENT(F) is open by A3,TOPS_2:9;
then consider G9 be Subset-Family of T such that
A8: G9 c= COMPLEMENT(F) and
A9: G9 is Cover of T and
A10: G9 is finite by A1,A6,A7;
A11: COMPLEMENT(G9) is finite by A10,TOPS_2:8;
A12: COMPLEMENT(G9) c= F
proof
let x be object such that
A13: x in COMPLEMENT(G9);
reconsider x9=x as Subset of T by A13;
x9` in G9 by A13,SETFAM_1:def 7;
then x9`` in F by A8,SETFAM_1:def 7;
hence thesis;
end;
G9 <> {} by A9,TOPS_2:3;
then
A14: COMPLEMENT(G9) <> {} by TOPS_2:5;
meet COMPLEMENT(G9) = (union G9)` by A9,TOPS_2:3,6
.= ([#] T) \ ([#] T) by A9,SETFAM_1:45
.= {} by XBOOLE_1:37;
hence contradiction by A2,A12,A14,A11,FINSET_1:def 3;
end;
assume
A15: 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
A16: F is Cover of T and
A17: F is open and
A18: F is countable;
A19: COMPLEMENT(F) is countable by A18,TOPGEN_4:1;
F <> {} by A16,TOPS_2:3;
then
A20: COMPLEMENT(F) <> {} by TOPS_2:5;
A21: COMPLEMENT(F) is closed by A17,TOPS_2:10;
meet COMPLEMENT(F) = (union F)` by A16,TOPS_2:3,6
.= ([#] T) \ ([#] T) by A16,SETFAM_1:45
.= {} by XBOOLE_1:37;
then not COMPLEMENT(F) is centered by A15,A19,A21;
then consider G9 being set such that
A22: G9 <> {} and
A23: G9 c= COMPLEMENT(F) and
A24: G9 is finite and
A25: meet G9 = {} by A20,FINSET_1:def 3;
reconsider G9 as Subset-Family of T by A23,XBOOLE_1:1;
take F9=COMPLEMENT(G9);
thus F9 c= F
proof
let x be object such that
A26: x in F9;
reconsider x9=x as Subset of T by A26;
x9` in G9 by A26,SETFAM_1:def 7;
then x9`` in F by A23,SETFAM_1:def 7;
hence thesis;
end;
union F9 = (meet G9)` by A22,TOPS_2:7
.= [#] T by A25;
hence thesis by A24,SETFAM_1:45,TOPS_2:8;
end;
theorem Th22:
for T being non empty TopSpace holds T is countably_compact iff
for S be non-empty closed SetSequence of T st S is non-ascending 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 non-ascending holds meet S <> {}
proof
assume
A1: T is countably_compact;
let S be non-empty closed SetSequence of T such that
A2: S is non-ascending;
reconsider rngS=rng S as Subset-Family of T;
dom S=NAT by FUNCT_2:def 1;
then
A3: rngS is countable by CARD_3:93;
now
let D be Subset of T;
assume D in rngS;
then ex x being object st x in dom S & S.x=D by FUNCT_1:def 3;
hence D is closed by Def6;
end;
then
A4: rngS is closed;
rngS is centered by A2,Th11;
then meet rngS<>{} by A1,A3,A4,Th21;
then consider x being object such that
A5: x in meet rngS by XBOOLE_0:def 1;
now
let n be Nat;
A6: n in NAT by ORDINAL1:def 12;
dom S=NAT by FUNCT_2:def 1;
then S.n in rngS by FUNCT_1:def 3,A6;
hence x in S.n by A5,SETFAM_1:def 1;
end;
hence thesis by KURATO_0:3;
end;
assume
A7: for S be non-empty closed SetSequence of T st S is non-ascending
holds meet S <> {};
now
let F be Subset-Family of T such that
A8: F is centered and
A9: F is closed and
A10: F is countable;
A11: card F c= omega by A10,CARD_3:def 14;
now
per cases by A11,CARD_1:3;
suppose
card F = omega;
then NAT,F are_equipotent by CARD_1:5,47;
then consider s be Function such that
s is one-to-one and
A12: dom s = NAT and
A13: rng s = F by WELLORD2:def 4;
reconsider s as SetSequence of T by A12,A13,FUNCT_2:2;
consider R be SetSequence of T such that
A14: R is non-ascending and
A15: F is centered implies R is non-empty and
F is open implies R is open and
A16: F is closed implies R is closed and
A17: for i holds R.i=meet{s.j where j is Element of NAT:j<=i}by A13,Th13;
meet R<>{} by A7,A8,A9,A14,A15,A16;
then consider x being object such that
A18: x in meet R by XBOOLE_0:def 1;
A19: now
let y;
assume y in F;
then consider z be object such that
A20: z in dom s and
A21: s.z=y by A13,FUNCT_1:def 3;
reconsider z as Element of NAT by A20;
A22: s.z in {s.j where j is Element of NAT:j<=z};
A23: x in R.z by A18,KURATO_0:3;
R.z=meet {s.j where j is Element of NAT:j<=z} by A17;
then R.z c= s.z by A22,SETFAM_1:3;
hence x in y by A21,A23;
end;
F is non empty by A12,A13,RELAT_1:42;
hence meet F is non empty by A19,SETFAM_1:def 1;
end;
suppose
A24: card F in omega;
F is finite by A24;
hence meet F is non empty by A8,FINSET_1:def 3;
end;
end;
hence meet F<>{};
end;
hence thesis by Th21;
end;
theorem Th23:
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 non-ascending & ( 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
A1: rng S c= F and
A2: S is non-empty;
defpred r[object,object] 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 being object st x in NAT
ex y being object st y in bool(the carrier of T) & r[x,y]
proof
let x be object;
assume x in NAT;
then reconsider x9=x as Nat;
set SS={S.j where j is Element of NAT:j >= x9};
SS c= bool(the carrier of T)
proof
let y be object;
assume y in SS;
then ex j be Element of NAT st S.j=y & j>=x9;
hence thesis;
end;
then reconsider SS as Subset-Family of T;
take Cl union SS;
SS c= F
proof
let y be object;
assume y in SS;
then consider j be Element of NAT such that
A4: S.j=y & j>=x9;
dom S=NAT by FUNCT_2:def 1;
then y in rng S by A4,FUNCT_1:def 3;
hence thesis by A1;
end;
hence thesis;
end;
consider R be SetSequence of T such that
A5: for x being object st x in NAT holds r[x,R.x] from FUNCT_2:sch 1(A3);
A6: now
let n be object;
assume n in dom R;
then reconsider n9=n as Element of NAT;
A7: S.n9 c= Cl(S.n9) by PRE_TOPC:18;
consider SS be Subset-Family of T such that
SS c= F and
A8: SS = {S.j where j is Element of NAT:j>=n9} and
A9: R.n9=Cl(union SS) by A5;
S.n9 in SS by A8;
then
A10: Cl(S.n9) c= Cl(union SS) by PRE_TOPC:19,ZFMISC_1:74;
dom S=NAT by FUNCT_2:def 1;
hence R.n is non empty by A2,A9,A7,A10,FUNCT_1:def 9;
end;
now
let n;
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
ex SS be Subset-Family of T st SS c= F & SS = {S.j where j is Element
of NAT:j>=n9} & R.n9=Cl(union SS) by A5;
hence R.n is closed;
end;
then reconsider R as non-empty closed SetSequence of T by A6,Def6,
FUNCT_1:def 9;
take R;
now
let n be Nat;
A11: n in NAT by ORDINAL1:def 12;
consider Sn be Subset-Family of T such that
Sn c= F and
A12: Sn = {S.j where j is Element of NAT:j>=n} and
A13: R.n=Cl(union Sn) by A5,A11;
consider Sn1 be Subset-Family of T such that
Sn1 c= F and
A14: Sn1 = {S.j where j is Element of NAT:j>=n+1} and
A15: R.(n+1)=Cl(union Sn1) by A5;
Sn1 c= Sn
proof
let y be object;
assume y in Sn1;
then consider j be Element of NAT such that
A16: y=S.j and
A17: j>=n+1 by A14;
j>=n by A17,NAT_1:13;
hence thesis by A12,A16;
end;
then union Sn1 c= union Sn by ZFMISC_1:77;
hence R.(n+1) c= R.n by A13,A15,PRE_TOPC:19;
end;
hence R is non-ascending by KURATO_0:def 3;
thus F is locally_finite & S is one-to-one implies meet R = {}
proof
A18: dom S=NAT by FUNCT_2:def 1;
then reconsider rngS=rng S as non empty Subset-Family of T by RELAT_1:42;
reconsider Sp=S as sequence of rngS by A18,FUNCT_2:1;
assume that
A19: F is locally_finite and
A20: S is one-to-one;
reconsider S9=Sp" as Function;
reconsider S9 as Function of rngS,NAT by A20,FUNCT_2:25;
deffunc s9(Element of rngS)=S9.$1;
assume meet R <> {};
then consider x being object such that
A21: x in meet R by XBOOLE_0:def 1;
reconsider x as Point of T by A21;
rng S is locally_finite by A1,A19,PCOMPS_1:9;
then consider W be Subset of T such that
A22: x in W and
A23: W is open and
A24: { V where V is Subset of T: V in rngS & V meets W } is finite;
set X={ V where V is Subset of T: V in rngS & V meets W };
set Y={s9(z) where z is Element of rngS:z in X};
A25: Y is finite from FRAENKEL:sch 21(A24);
Y c= NAT
proof
let y be object;
assume y in Y;
then ex z be Element of rngS st y =s9(z) & z in X;
hence thesis;
end;
then reconsider Y as Subset of NAT;
consider n be Nat such that
A26: for k be Nat st k in Y holds k <= n by A25,STIRL2_1:56;
set n1=n+1;
A27: x in R.n1 by A21,KURATO_0:3;
consider Sn be Subset-Family of T such that
A28: Sn c= F and
A29: Sn ={S.j where j is Element of NAT:j>=n1} and
A30: R.n1=Cl(union Sn) by A5;
Cl(union Sn)=union(clf Sn) by A19,A28,PCOMPS_1:9,20;
then consider CLF be set such that
A31: x in CLF and
A32: CLF in clf Sn by A30,A27,TARSKI:def 4;
reconsider CLF as Subset of T by A32;
consider U be Subset of T such that
A33: CLF = Cl U and
A34: U in Sn by A32,PCOMPS_1:def 2;
consider j be Element of NAT such that
A35: U=S.j and
A36: j>=n1 by A29,A34;
A37: Sp.j in rngS;
Sp.j meets W by A22,A23,A31,A33,A35,TOPS_1:12;
then
A38: Sp.j in X by A37;
(S").(S.j) = j by A20,FUNCT_2:26;
then j in Y by A38;
then j <=n by A26;
hence thesis by A36,NAT_1:13;
end;
let i;
i in NAT by ORDINAL1:def 12;
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 A5;
hence thesis;
end;
Lm2: 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
A1: T is countably_compact;
given F be Subset-Family of T such that
A2: F is locally_finite and
A3: F is with_non-empty_elements and
A4: F is infinite;
consider f be sequence of F such that
A5: f is one-to-one by A4,DICKSON:3;
A6: rng f c= F;
reconsider f as SetSequence of T by A4,FUNCT_2:7;
now
let x be object;
assume x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence f.x is non empty by A3,A6;
end;
then f is non-empty by FUNCT_1:def 9;
then ex R be non-empty closed SetSequence of T st R is non-ascending & ( 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 A6,Th23;
hence thesis by A1,A2,A5,Th22;
end;
Lm3: 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:27;
then F is with_non-empty_elements by SETFAM_1:def 8;
hence thesis by A1,A2;
end;
Lm4: 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
deffunc P(set)=meet $1;
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;
set F={{x} where x is Element of T: x in A};
reconsider F as Subset-Family of T by RELSET_2:16;
set PP={P(y) where y is Element of bool(the carrier of T):y in F};
A3: A c= PP
proof
let y be object such that
A4: y in A;
reconsider y9=y as Point of T by A4;
{y9} in F by A4;
then P({y9}) in PP;
hence thesis by SETFAM_1:10;
end;
assume
A5: Der A is empty;
A6: F is locally_finite
proof
let x be Point of T;
consider U be open Subset of T such that
A7: x in U and
A8: for y being Point of T st y in A /\ U holds x = y by A5,TOPGEN_1:17;
set M={ V where V is Subset of T: V in F & V meets U};
take U;
M c= {{x}}
proof
A9: {x} in {{x}} by TARSKI:def 1;
let v be object;
assume v in M;
then consider V be Subset of T such that
A10: v=V and
A11: V in F and
A12: V meets U;
consider y be Point of T such that
A13: V = {y} and
A14: y in A by A11;
y in U by A12,A13,ZFMISC_1:50;
then y in A/\U by A14,XBOOLE_0:def 4;
hence thesis by A8,A10,A13,A9;
end;
hence thesis by A7;
end;
now
let a be Subset of T;
assume a in F;
then ex y be Point of T st a={y} & y in A;
hence card a = 1 by CARD_1:30;
end;
then
A15: F is finite by A1,A6;
PP is finite from FRAENKEL:sch 21(A15);
hence thesis by A2,A3;
end;
::$CT
theorem Th24:
for X be non empty set, F be SetSequence of X st F is
non-ascending for S be sequence of 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 non-ascending;
let S be sequence of X such that
A2: for n holds S.n in F.n;
A3: dom S=NAT by FUNCT_2:def 1;
assume rng S is finite;
then consider x being object such that
x in rng S and
A4: S"{x} is infinite by A3,CARD_2:101;
now
let n be Nat;
ex i st x in F.i & i >= n
proof
assume
A5: for i st x in F.i holds i<n;
S"{x} c= Segm n
proof
let y be object such that
A6: y in S"{x};
reconsider i=y as Nat by A6;
S.i in {x} by A6,FUNCT_1:def 7;
then
A7: S.i=x by TARSKI:def 1;
S.i in F.i by A2;
then i<n by A5,A7;
hence thesis by NAT_1:44;
end;
hence thesis by A4;
end;
then consider i such that
A8: x in F.i and
A9: i>=n;
F.i c= F.n by A1,A9,PROB_1:def 4;
hence x in F.n by A8;
end;
hence thesis by KURATO_0:3;
end;
Lm5: for T be T_1 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 T_1 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 non-ascending and
A3: meet S = {} by Th22;
defpred P[object,object] means $2 in S.$1;
:: Funkcja Kuratowskiego
A4: for x being object st x in NAT
ex y being object st y in the carrier of T & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider x9=x as Element of NAT;
dom S=NAT by FUNCT_2:def 1;
then S.x9 is non empty by FUNCT_1:def 9;
then consider y being object such that
A5: y in S.x9 by XBOOLE_0:def 1;
take y;
thus thesis by A5;
end;
consider F be sequence of T such that
A6: for x being object st x in NAT holds P[x,F.x] from FUNCT_2:sch 1(A4);
reconsider rngF=rng F as Subset of T;
A7: for n holds F.n in S.n by A6,ORDINAL1:def 12;
dom F=NAT by FUNCT_2:def 1;
then rng F is countable by CARD_3:93;
then Der rngF is non empty by A1,A2,A3,A7,Th24;
then consider p be object such that
A8: p in Der rngF by XBOOLE_0:def 1;
reconsider p as Point of T by A8;
consider n be Nat such that
A9: not p in S.n by A3,KURATO_0:3;
A10: p in (S.n)` by A9,XBOOLE_0:def 5;
deffunc f(set)=F.$1;
set F1n={f(i) where i is Element of NAT:i in n+1};
A11: F1n c= the carrier of T
proof
let x be object;
assume x in F1n;
then ex i be Element of NAT st x=F.i & i in n+1;
hence thesis;
end;
A12: n+1 is finite;
A13: F1n is finite from FRAENKEL:sch 21(A12);
reconsider F1n as Subset of T by A11;
set U=((S.n)`)\(F1n\{p});
reconsider U as Subset of T;
p in {p} by TARSKI:def 1;
then not p in F1n\{p} by XBOOLE_0:def 5;
then
A14: p in U by A10,XBOOLE_0:def 5;
(S.n) is closed by Def6;
then U is open by A13,FRECHET:4;
then consider q be Point of T such that
A15: q in rngF /\ U and
A16: q <> p by A8,A14,TOPGEN_1:17;
q in rngF by A15,XBOOLE_0:def 4;
then consider i be object such that
A17: i in dom F and
A18: F.i=q by FUNCT_1:def 3;
reconsider i as Element of NAT by A17;
per cases;
suppose
i<=n;
then i < n+1 by NAT_1:13;
then i in Segm(n+1) by NAT_1:44;
then q in F1n by A18;
then q in F1n\{p} by A16,ZFMISC_1:56;
then not q in U by XBOOLE_0:def 5;
hence contradiction by A15,XBOOLE_0:def 4;
end;
suppose
i>n;
then
A19: S.i c= S.n by A2,PROB_1:def 4;
q in S.i by A6,A18;
then not q in (S.n)` by A19,XBOOLE_0:def 5;
then not q in U by XBOOLE_0:def 5;
hence contradiction by A15,XBOOLE_0:def 4;
end;
end;
Lm6: 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
deffunc P(set)=meet $1;
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 non-ascending and
A3: meet S = {} by Th22;
defpred P[object,object] means $2 in S.$1;
:: Funkcja Kuratowskiego !!!
A4: for x being object st x in NAT
ex y being object st y in the carrier of T & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider x9=x as Element of NAT;
dom S=NAT by FUNCT_2:def 1;
then S.x9 is non empty by FUNCT_1:def 9;
then consider y being object such that
A5: y in S.x9 by XBOOLE_0:def 1;
take y;
thus thesis by A5;
end;
consider F be sequence of T such that
A6: for x being object st x in NAT holds P[x,F.x] from FUNCT_2:sch 1(A4);
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;
A7: A is locally_finite
proof
deffunc f(set)={F.$1};
let x be Point of T;
consider i be Nat such that
A8: not x in S.i by A3,KURATO_0:3;
take Si9=(S.i)`;
S.i is closed by Def6;
hence x in Si9 & Si9 is open by A8,SUBSET_1:29;
set meetS={ V where V is Subset of T: V in A & V meets Si9 };
set SI={f(j) where j is Element of NAT:j in i};
A9: meetS c= SI
proof
let v be object;
assume v in meetS;
then consider V be Subset of T such that
A10: V=v and
A11: V in A and
A12: V meets Si9;
consider y be Point of T such that
A13: V={y} and
A14: y in rng F by A11;
consider z be object such that
A15: z in dom F and
A16: y=F.z by A14,FUNCT_1:def 3;
reconsider z as Element of NAT by A15;
z in Segm i
proof
assume not z in Segm i;
then z>=i by NAT_1:44;
then
A17: S.z c= S.i by A2,PROB_1:def 4;
A18: y in Si9 by A12,A13,ZFMISC_1:50;
y in S.z by A6,A16;
hence thesis by A17,A18,XBOOLE_0:def 5;
end;
hence thesis by A10,A13,A16;
end;
A19: i is finite;
SI is finite from FRAENKEL:sch 21(A19);
hence thesis by A9;
end;
set PP={P(y) where y is Element of bool(the carrier of T):y in A};
A20: rngF c= PP
proof
let y be object such that
A21: y in rngF;
reconsider y9=y as Point of T by A21;
{y9} in A by A21;
then P({y9}) in PP;
hence thesis by SETFAM_1:10;
end;
A22: for n holds F.n in S.n by A6,ORDINAL1:def 12;
now
let a be Subset of T;
assume a in A;
then ex y be Point of T st a={y} & y in rngF;
hence card a = 1 by CARD_1:30;
end;
then
A23: A is finite by A1,A7;
PP is finite from FRAENKEL:sch 21(A23);
hence thesis by A2,A3,A22,A20,Th24;
end;
theorem Th25:
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 Lm2;
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 Lm3;
hence thesis by Lm6;
end;
theorem Th26:
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 Th25;
hence thesis by Lm3;
end;
thus thesis by Lm6;
end;
theorem Th27:
for T be T_1 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 T_1 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 Th26;
hence thesis by Lm4;
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 Lm5;
end;
theorem
for T be T_1 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 Lm5,Th27;
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:17;
R/\[:X(),X():]c=[:X(),X():] by XBOOLE_1:17;
then reconsider R2=R |_2 X() as Relation of X() by WELLORD1:def 6;
reconsider RS=RelStr(#X(),R2#) as non empty RelStr;
set cRS=the carrier of RS;
defpred H[object,object,object] 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) );
A4: for x,y being object st x in cRS & y in PFuncs(cRS, bX)
ex z be object st z in bX & H[x,y,z]
proof
let x,y be object such that
A5: x in cRS and
A6: y in PFuncs(cRS, bX);
reconsider f=y as PartFunc of cRS,bX by A6,PARTFUN1:46;
reconsider p=x as Element of X() by A5;
per cases;
suppose
A7: for q be Element of X() st q in union(rng f) holds P[p,q];
take union (rng f) \/ {p};
thus thesis by A7;
end;
suppose
A8: ex q be Element of X() st q in union (rng f) & not P[p,q];
take union (rng f);
thus thesis by A8;
end;
end;
consider h be Function of [:cRS,PFuncs(cRS, bX):],bX such that
A9: for x,y being object st x in cRS & y in PFuncs(cRS, bX)
holds H[x,y,h.(x,y)]
from BINOP_1:sch 1(A4);
set IRS=the InternalRel of RS;
A10: R2 well_orders X() by A3,PCOMPS_2:1;
then R2 is_well_founded_in X() by WELLORD1:def 5;
then
A11: RS is well_founded by WELLFND1:def 2;
then consider f be Function of cRS, bX such that
A12: f is_recursively_expressed_by h by WELLFND1:11;
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]);
reconsider rngf=rng f as Subset of bX;
take A=union rngf;
A13: field R2 = X() by A3,PCOMPS_2:1;
then
A14: R2 is well-ordering by A10,WELLORD1:4;
A15: 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
A16: for y be Element of RS st y <> x & [y,x] in IRS holds S[y];
set fIx=f|IRS-Seg x;
A17: union rng fIx c= IRS-Seg x
proof
let y be object;
assume y in union rng fIx;
then consider z be set such that
A18: y in z and
A19: z in rng fIx by TARSKI:def 4;
consider t be object such that
A20: t in dom fIx and
A21: fIx.t=z by A19,FUNCT_1:def 3;
A22: t in IRS-Seg x by A20,RELAT_1:57;
reconsider t as Element of RS by A20;
A23: {t} c= IRS-Seg(x) by A22,ZFMISC_1:31;
A24: [t,x] in IRS by A22,WELLORD1:1;
then IRS-Seg(t)c=IRS-Seg(x) by A13,A14,WELLORD1:29;
then
A25: (IRS-Seg t)\/{t} c= IRS-Seg(x) by A23,XBOOLE_1:8;
t<>x by A22,WELLORD1:1;
then
A26: f.t c= (IRS-Seg t)\/{t} by A16,A24;
fIx.t=f.t by A20,FUNCT_1:47;
then y in (IRS-Seg t)\/{t} by A18,A21,A26;
hence thesis by A25;
end;
A27: fIx in PFuncs(cRS,bX) by PARTFUN1:45;
A28: f.x=h.(x,fIx) by A12,WELLFND1:def 5;
per cases;
suppose
A29: for q be Element of X() st q in union(rng fIx) holds P[x,q];
then
A30: f.x=union(rng fIx)\/{x} by A9,A28,A27;
hence f.x c= IRS-Seg x\/{x} by A17,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 A29;
A31: x in {x} by TARSKI:def 1;
assume not x in f.x;
hence thesis by A30,A31,XBOOLE_0:def 3;
end;
suppose
A32: ex q be Element of X() st q in union (rng fIx) & not P[x,q];
then
A33: f.x c= IRS-Seg x by A9,A17,A28,A27;
IRS-Seg x c= IRS-Seg x\/{x} by XBOOLE_1:7;
hence f.x c= IRS-Seg x\/{x} by A33;
thus thesis by A32,A33,WELLORD1:1;
end;
end;
A34: for x being Element of RS holds S[x] from WELLFND1:sch 3(A15,A11);
thus for x,y be Element of X() st x in A & y in A & x <> y holds P[x,y]
proof
A35: now
let x be Element of X();
assume x in A;
then consider y such that
A36: x in y and
A37: y in rng f by TARSKI:def 4;
defpred T[set] means x in f.$1;
consider z be object such that
A38: z in dom f and
A39: f.z=y by A37,FUNCT_1:def 3;
reconsider z as Element of RS by A38;
A40: T[z] by A36,A39;
consider p being Element of RS such that
A41: T[p] and
A42: not ex q being Element of RS st p <> q & T[q] & [q,p] in IRS
from WELLFND1:sch 2(A40,A11);
p = x
proof
set fIp=f|IRS-Seg p;
A43: fIp in PFuncs(cRS, bX) by PARTFUN1:45;
A44: f.p=h.(p,fIp) by A12,WELLFND1:def 5;
assume
A45: p<>x;
now
per cases;
suppose
A46: for q be Element of X() st q in union(rng fIp) holds P[p, q];
A47: not x in {p} by A45,TARSKI:def 1;
f.p=union(rng fIp)\/{p} by A9,A44,A43,A46;
hence x in union(rng fIp) by A41,A47,XBOOLE_0:def 3;
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 A9,A41,A44,A43;
end;
end;
then consider y9 be set such that
A48: x in y9 and
A49: y9 in rng fIp by TARSKI:def 4;
consider z9 be object such that
A50: z9 in dom fIp and
A51: fIp.z9=y9 by A49,FUNCT_1:def 3;
reconsider z9 as Point of RS by A50;
A52: z9 in IRS-Seg p by A50,RELAT_1:57;
then
A53: z9<> p by WELLORD1:1;
A54: [z9,p] in IRS by A52,WELLORD1:1;
T[z9] by A48,A50,A51,FUNCT_1:47;
hence thesis by A42,A53,A54;
end;
hence x in f.x by A41;
end;
A55: now
A56: dom f = cRS by FUNCT_2:def 1;
let x,y be Element of X() such that
A57: x in A and
A58: y in A and
A59: x <> y and
A60: [x,y] in IRS;
A61: y in f.y by A35,A58;
set fIy=f|IRS-Seg y;
x in IRS-Seg y by A59,A60,WELLORD1:1;
then
A62: x in dom fIy by A56,RELAT_1:57;
then
A63: fIy.x in rng fIy by FUNCT_1:def 3;
A64: fIy.x=f.x by A62,FUNCT_1:47;
x in f.x by A35,A57;
then x in union(rng fIy) by A63,A64,TARSKI:def 4;
then P[y,x] by A34,A61;
hence P[x,y] by A1;
end;
let x,y be Element of X() such that
A65: x in A and
A66: y in A and
A67: x <> y;
R2 well_orders X() by A3,PCOMPS_2:1;
then R2 is_connected_in X() by WELLORD1:def 5;
then [x,y] in IRS or [y,x] in IRS by A67,RELAT_2:def 6;
then P[x,y] or P[y,x] by A55,A65,A66,A67;
hence thesis by A1;
end;
let x be Element of X();
per cases;
suppose
A68: x in A;
take x;
thus thesis by A2,A68;
end;
suppose
A69: not x in A;
not x in f.x
proof
dom f=cRS by FUNCT_2:def 1;
then
A70: f.x in rng f by FUNCT_1:def 3;
assume x in f.x;
hence thesis by A69,A70,TARSKI:def 4;
end;
then consider r be Element of X() such that
A71: r in union(rng (f|IRS-Seg x)) and
A72: not P[x,r] by A34;
take r;
union rng (f|IRS-Seg x) c= A by RELAT_1:70,ZFMISC_1:77;
hence thesis by A71,A72;
end;
end;
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:17;
R/\[:X(),X():]c=[:X(),X():] by XBOOLE_1:17;
then reconsider R2=R |_2 X() as Relation of X() by WELLORD1:def 6;
reconsider RS=RelStr(#X(),R2#) as non empty RelStr;
set cRS=the carrier of RS;
defpred H[object,object,object] 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) );
A4: for x,y being object st x in cRS & y in PFuncs(cRS, bX)
ex z be object st z in bX & H[x,y,z]
proof
let x,y be object such that
A5: x in cRS and
A6: y in PFuncs(cRS, bX);
reconsider f=y as PartFunc of cRS,bX by A6,PARTFUN1:46;
reconsider p=x as Element of X() by A5;
per cases;
suppose
A7: for q be Element of X() st q in union(rng f) holds P[p,q];
take union (rng f) \/ {p};
thus thesis by A7;
end;
suppose
A8: ex q be Element of X() st q in union (rng f) & not P[p,q];
take union (rng f);
thus thesis by A8;
end;
end;
consider h be Function of [:cRS,PFuncs(cRS, bX):],bX such that
A9: for x,y being object st x in cRS & y in PFuncs(cRS, bX)
holds H[x,y,h.(x,y)] from BINOP_1:sch 1(A4);
set IRS=the InternalRel of RS;
A10: R2 well_orders X() by A3,PCOMPS_2:1;
then R2 is_well_founded_in X() by WELLORD1:def 5;
then
A11: RS is well_founded by WELLFND1:def 2;
then consider f be Function of cRS, bX such that
A12: f is_recursively_expressed_by h by WELLFND1:11;
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]);
reconsider rngf=rng f as Subset of bX;
take A=union rngf;
A13: field R2 = X() by A3,PCOMPS_2:1;
then
A14: R2 is well-ordering by A10,WELLORD1:4;
A15: 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
A16: for y be Element of RS st y <> x & [y,x] in IRS holds S[y];
set fIx=f|IRS-Seg x;
A17: union rng fIx c= IRS-Seg x
proof
let y be object;
assume y in union rng fIx;
then consider z be set such that
A18: y in z and
A19: z in rng fIx by TARSKI:def 4;
consider t be object such that
A20: t in dom fIx and
A21: fIx.t=z by A19,FUNCT_1:def 3;
A22: t in IRS-Seg x by A20,RELAT_1:57;
reconsider t as Element of RS by A20;
A23: {t} c= IRS-Seg(x) by A22,ZFMISC_1:31;
A24: [t,x] in IRS by A22,WELLORD1:1;
then IRS-Seg(t)c=IRS-Seg(x) by A13,A14,WELLORD1:29;
then
A25: (IRS-Seg t)\/{t} c= IRS-Seg(x) by A23,XBOOLE_1:8;
t<>x by A22,WELLORD1:1;
then
A26: f.t c= (IRS-Seg t)\/{t} by A16,A24;
fIx.t=f.t by A20,FUNCT_1:47;
then y in (IRS-Seg t)\/{t} by A18,A21,A26;
hence thesis by A25;
end;
A27: fIx in PFuncs(cRS,bX) by PARTFUN1:45;
A28: f.x=h.(x,fIx) by A12,WELLFND1:def 5;
per cases;
suppose
A29: for q be Element of X() st q in union(rng fIx) holds P[x,q];
then
A30: f.x=union(rng fIx)\/{x} by A9,A28,A27;
hence f.x c= IRS-Seg x\/{x} by A17,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 A29;
A31: x in {x} by TARSKI:def 1;
assume not x in f.x;
hence thesis by A30,A31,XBOOLE_0:def 3;
end;
suppose
A32: ex q be Element of X() st q in union (rng fIx) & not P[x,q];
then
A33: f.x c= IRS-Seg x by A9,A17,A28,A27;
IRS-Seg x c= IRS-Seg x\/{x} by XBOOLE_1:7;
hence f.x c= IRS-Seg x\/{x} by A33;
thus thesis by A32,A33,WELLORD1:1;
end;
end;
A34: for x being Element of RS holds S[x] from WELLFND1:sch 3(A15,A11);
thus for x,y be Element of X() st x in A & y in A & x <> y holds P[x,y]
proof
A35: now
let x be Element of X();
assume x in A;
then consider y such that
A36: x in y and
A37: y in rng f by TARSKI:def 4;
defpred T[set] means x in f.$1;
consider z be object such that
A38: z in dom f and
A39: f.z=y by A37,FUNCT_1:def 3;
reconsider z as Element of RS by A38;
A40: T[z] by A36,A39;
consider p being Element of RS such that
A41: T[p] and
A42: not ex q being Element of RS st p <> q & T[q] & [q,p] in IRS
from WELLFND1:sch 2(A40,A11);
p = x
proof
set fIp=f|IRS-Seg p;
A43: fIp in PFuncs(cRS, bX) by PARTFUN1:45;
A44: f.p=h.(p,fIp) by A12,WELLFND1:def 5;
assume
A45: p<>x;
now
per cases;
suppose
A46: for q be Element of X() st q in union(rng fIp) holds P[p, q];
A47: not x in {p} by A45,TARSKI:def 1;
f.p=union(rng fIp)\/{p} by A9,A44,A43,A46;
hence x in union(rng fIp) by A41,A47,XBOOLE_0:def 3;
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 A9,A41,A44,A43;
end;
end;
then consider y9 be set such that
A48: x in y9 and
A49: y9 in rng fIp by TARSKI:def 4;
consider z9 be object such that
A50: z9 in dom fIp and
A51: fIp.z9=y9 by A49,FUNCT_1:def 3;
reconsider z9 as Point of RS by A50;
A52: z9 in IRS-Seg p by A50,RELAT_1:57;
then
A53: z9<> p by WELLORD1:1;
A54: [z9,p] in IRS by A52,WELLORD1:1;
T[z9] by A48,A50,A51,FUNCT_1:47;
hence thesis by A42,A53,A54;
end;
hence x in f.x by A41;
end;
A55: now
A56: dom f = cRS by FUNCT_2:def 1;
let x,y be Element of X() such that
A57: x in A and
A58: y in A and
A59: x <> y and
A60: [x,y] in IRS;
A61: y in f.y by A35,A58;
set fIy=f|IRS-Seg y;
x in IRS-Seg y by A59,A60,WELLORD1:1;
then
A62: x in dom fIy by A56,RELAT_1:57;
then
A63: fIy.x in rng fIy by FUNCT_1:def 3;
A64: fIy.x=f.x by A62,FUNCT_1:47;
x in f.x by A35,A57;
then x in union(rng fIy) by A63,A64,TARSKI:def 4;
then P[y,x] by A34,A61;
hence P[x,y] by A1;
end;
let x,y be Element of X() such that
A65: x in A and
A66: y in A and
A67: x <> y;
R2 well_orders X() by A3,PCOMPS_2:1;
then R2 is_connected_in X() by WELLORD1:def 5;
then [x,y] in IRS or [y,x] in IRS by A67,RELAT_2:def 6;
then P[x,y] or P[y,x] by A55,A65,A66,A67;
hence thesis by A1;
end;
let x be Element of X();
per cases;
suppose
A68: x in A;
take x;
thus thesis by A2,A68;
end;
suppose
A69: not x in A;
not x in f.x
proof
dom f=cRS by FUNCT_2:def 1;
then
A70: f.x in rng f by FUNCT_1:def 3;
assume x in f.x;
hence thesis by A69,A70,TARSKI:def 4;
end;
then consider r be Element of X() such that
A71: r in union(rng (f|IRS-Seg x)) and
A72: not P[x,r] by A34;
take r;
union rng (f|IRS-Seg x) c= A by RELAT_1:70,ZFMISC_1:77;
hence thesis by A71,A72;
end;
end;
theorem Th29:
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;
set cM=the carrier of M;
defpred P[set,set] means for p,q be Point of M st p=$1 & q=$2 holds dist(p,q
)>=r;
A2: 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;
A3: for x,y be Element of cM holds P[x,y] iff P[y,x];
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(A3,A2);
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 and
A7: not P[p,y] by A5;
take y;
thus thesis by A6,A7,METRIC_1:11;
end;
theorem Th30:
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:215;
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;
defpred f[object,object] means
ex D2 being set st D2 = $2 & $1 in D2 & $2 in G;
A7: for x being object st x in A
ex y being object st y in bool(the carrier of M) & f[x,y]
proof
let x be object;
assume x in A;
then consider y such that
A8: x in y and
A9: y in G by A5,TARSKI:def 4;
reconsider y as Subset of M by A9;
take y;
thus thesis by A8,A9;
end;
consider F be Function of A, bool the carrier of M such that
A10: for x being object st x in A holds f[x,F.x] from FUNCT_2:sch 1(A7);
now
let x1,x2 be object such that
A11: x1 in A and
A12: x2 in A and
A13: F.x1 = F.x2;
reconsider p1=x1,p2=x2 as Point of M by A11,A12;
A14: f[x1,F.x1] by A10,A11;
then F.x1 in G;
then consider w be Point of M such that
A15: F.x1 = Ball(w,r/2) by A6;
p1 in Ball(w,r/2) by A15,A14;
then
A16: dist(p1,w)<r/2 by METRIC_1:11;
A17: dist(p1,p2)<=dist(p1,w)+dist(w,p2) by METRIC_1:4;
f[x2,F.x2] by A10,A12;
then p2 in Ball(w,r/2) by A13,A15;
then dist(w,p2)<r/2 by METRIC_1:11;
then dist(p1,w)+dist(w,p2)<r/2+r/2 by A16,XREAL_1:8;
then dist(p1,p2)<r/2+r/2 by A17,XXREAL_0:2;
hence x1 = x2 by A3,A11,A12;
end;
then
A18: F is one-to-one by FUNCT_2:19;
A19: rng F c= G
proof
let x be object;
assume x in rng F;
then consider y being object such that
A20: y in dom F & x=F.y by FUNCT_1:def 3;
f[y,F.y] by A10,A20;
then consider D2 being set such that
A21: D2 = F.y & y in D2 & F.y in G;
thus thesis by A20,A21;
end;
dom F=A by FUNCT_2:def 1;
then A,rng F are_equipotent by A18,WELLORD2:def 4;
hence thesis by A4,A19,CARD_1:38;
end;
assume
A22: 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;
let r such that
A23: r>0;
reconsider r as Real;
consider A be Subset of M such that
A24: for p,q be Point of M st p <> q & p in A & q in A holds dist(p,q) >= r and
A25: for p be Point of M ex q be Point of M st q in A& p in Ball(q,r) by A23
,Th29;
deffunc B(Point of M)=Ball($1,r);
set BA={B(p) where p is Point of M:p in A};
A26: A is finite by A22,A23,A24;
A27: BA is finite from FRAENKEL:sch 21(A26);
BA c= bool the carrier of M
proof
let x be object;
assume x in BA;
then ex p be Point of M st x = B(p) & p in A;
hence thesis;
end;
then reconsider BA as Subset-Family of M;
take BA;
the carrier of M c= union BA
proof
let x be object;
assume x in the carrier of M;
then reconsider p=x as Point of M;
consider q be Point of M such that
A28: q in A and
A29: p in B(q) by A25;
B(q) in BA by A28;
hence thesis by A29,TARSKI:def 4;
end;
hence BA is finite & union BA = the carrier of M by A27,XBOOLE_0:def 10;
let C be Subset of M;
assume C in BA;
then ex p be Point of M st C=B(p) & p in A;
hence thesis;
end;
Lm7: 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;
A3: r/2>0 by A1,XREAL_1:215;
let F be Subset-Family of T such that
A4: F={{x} where x is Element of T: x in A};
let x be Point of T;
reconsider x9=x as Point of M;
reconsider B=Ball(x9,r/2) as Subset of T;
take B;
A5: dist(x9,x9)=0 by METRIC_1:1;
B in Family_open_set M by PCOMPS_1:29;
hence x in B & B is open by A5,A3,METRIC_1:11,PRE_TOPC:def 2;
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,x9) >= r/2;
VV is empty
proof
assume VV is non empty;
then consider v be object such that
A7: v in VV by XBOOLE_0:def 1;
consider V be Subset of T such that
v=V and
A8: V in F and
A9: V meets B by A7;
consider y be Point of T such that
A10: V = {y} and
A11: y in A by A4,A8;
reconsider y as Point of M;
y in B by A9,A10,ZFMISC_1:50;
then dist(x9,y)<r/2 by METRIC_1:11;
hence thesis by A6,A11;
end;
hence thesis;
end;
suppose
ex p be Point of M st p in A & dist(p,x9) < r/2;
then consider p be Point of M such that
A12: p in A and
A13: dist(p,x9) < r/2;
VV c= {{p}}
proof
let v be object;
assume v in VV;
then consider V be Subset of T such that
A14: v=V and
A15: V in F and
A16: V meets B;
consider y be Point of T such that
A17: V = {y} and
A18: y in A by A4,A15;
reconsider y as Point of M;
y in B by A16,A17,ZFMISC_1:50;
then dist(x9,y)<r/2 by METRIC_1:11;
then
A19: dist(p,x9)+dist(x9,y)<r/2+r/2 by A13,XREAL_1:8;
dist(p,y)<=dist(p,x9)+dist(x9,y) by METRIC_1:4;
then dist(p,y)<r/2+r/2 by A19,XXREAL_0:2;
then p = y by A2,A12,A18;
hence thesis by A14,A17,TARSKI:def 1;
end;
hence thesis;
end;
end;
theorem Th31:
for M be Reflexive symmetric triangle non empty MetrStruct st
TopSpaceMetr M is countably_compact holds M is totally_bounded
proof
deffunc P(set)=meet $1;
let M be Reflexive symmetric triangle non empty MetrStruct such that
A1: TopSpaceMetr M is countably_compact;
set T=TopSpaceMetr M;
assume not M is totally_bounded;
then consider 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 and
A4: A is infinite by Th30;
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: now
let a be Subset of T;
assume a in F;
then ex y be Point of T st a={y} & y in A;
hence card a = 1 by CARD_1:30;
end;
set PP={P(y) where y is Subset of T:y in F};
A6: A c= PP
proof
let y be object such that
A7: y in A;
reconsider y9=y as Point of T by A7;
{y9} in F by A7;
then P({y9}) in PP;
hence thesis by SETFAM_1:10;
end;
F is locally_finite by A2,A3,Lm7;
then
A8: F is finite by A1,A5,Th26;
PP is finite from FRAENKEL:sch 21(A8);
hence thesis by A4,A6;
end;
theorem Th32:
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[object,object] 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 being object st x in NAT
ex y being object st y in bool bool(the carrier of T) & F[x,y]
proof
let x be object;
assume x in NAT;
then reconsider i=x as Nat;
1/(i+1)>0 by XREAL_1:139;
then consider G be Subset-Family of T such that
A3: G is finite and
A4: the carrier of M = union G and
A5: 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;
take G;
thus thesis by A3,A4,A5;
end;
consider f be sequence of bool bool(the carrier of T) such that
A6: for x being object st x in NAT holds F[x,f.x] from FUNCT_2:sch 1(A2);
set U = Union f;
A7: dom f=NAT by FUNCT_2:def 1;
A8: 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
A9: A is open;
let p be Point of T such that
A10: p in A;
reconsider p9=p as Point of M;
consider r be Real such that
A11: r>0 and
A12: Ball(p9,r) c= A by A9,A10,TOPMETR:15;
reconsider r as Real;
consider n be Nat such that
A13: n>0 and
A14: 1/n<r/2 by A11,UNIFORM1:1,XREAL_1:215;
A15: 1/n+1/n<r/2+r/2 by A14,XREAL_1:8;
reconsider n1=n-1 as Element of NAT by A13,NAT_1:20;
reconsider fn=f.n1 as Subset-Family of T;
the carrier of M = union fn by A6;
then consider x be set such that
A16: p in x and
A17: x in fn by TARSKI:def 4;
reconsider x as Subset of M by A17;
consider w be Point of M such that
A18: x=Ball(w,1/(n1+1)) by A6,A17;
reconsider B=Ball(w,1/n) as Subset of T;
take B;
f.n1 in rng f by A7,FUNCT_1:def 3;
then B in union rng f by A17,A18,TARSKI:def 4;
hence B in U & p in B by A16,A18,CARD_3:def 4;
let q be object such that
A19: q in B;
reconsider q9=q as Point of M by A19;
A20: dist(q9,w)<1/n by A19,METRIC_1:11;
dist(w,p9)<1/(n1+1) by A16,A18,METRIC_1:11;
then
A21: dist(q9,w)+dist(w,p9)<1/n+1/n by A20,XREAL_1:8;
dist(q9,p9)<=dist(q9,w)+dist(w,p9) by METRIC_1:4;
then dist(q9,p9)<1/n+1/n by A21,XXREAL_0:2;
then dist(q9,p9)<r/2+r/2 by A15,XXREAL_0:2;
then q in Ball(p9,r) by METRIC_1:11;
hence thesis by A12;
end;
set CB=the set of all card B where B is Basis of T ;
U c= the topology of T
proof
let x be object;
assume x in U;
then x in union rng f by CARD_3:def 4;
then consider y such that
A22: x in y and
A23: y in rng f by TARSKI:def 4;
reconsider X=x as Subset of T by A22,A23;
consider z be object such that
A24: z in dom f and
A25: f.z=y by A23,FUNCT_1:def 3;
reconsider z as Element of NAT by A24;
f.z=y by A25;
then ex w be Point of M st X=Ball(w,1/(z+1)) by A6,A22;
hence thesis by PCOMPS_1:29;
end;
then U is Basis of T by A8,YELLOW_9:32;
then
A26: card U in CB;
now
let x;
assume x in dom f;
then reconsider i=x as Element of NAT;
reconsider fx=f.i as Subset-Family of T;
fx is finite by A6;
hence f.x is countable by CARD_4:1;
end;
then U is countable by A7,CARD_4:2,11;
then
A27: card U c= omega by CARD_3:def 14;
weight T = meet CB by WAYBEL23:def 5;
then weight T c= card U by A26,SETFAM_1:3;
then weight T c= omega by A27;
hence thesis by WAYBEL23:def 6;
end;
theorem Th33:
for T be non empty TopSpace holds T is second-countable implies
for F being Subset-Family of T st F is Cover of T & F is open ex G being
Subset-Family of T st G c= F & G is Cover of T & G is countable
proof
let T be non empty TopSpace;
assume T is second-countable;
then consider B being Basis of T such that
A1: B is countable by TOPGEN_4:57;
A2: card B c= omega by A1,CARD_3:def 14;
let F being Subset-Family of T such that
A3: F is Cover of T and
A4: F is open;
defpred P[object,object] means
ex D2 being set st D2 = $2 &
for b be Subset of T st b=$1 holds ((ex y st y in F
& b c= y) implies ($2 in F & b c= D2)) & ((for y st y in F holds not b c= y)
implies $2={});
A5: for x being object st x in B
ex y being object st y in bool(the carrier of T) & P[x,y]
proof
let x be object;
assume x in B;
then reconsider b=x as Subset of T;
per cases;
suppose
ex y st y in F & b c= y;
then consider y such that
A6: y in F and
A7: b c= y;
reconsider y as Subset of T by A6;
take y;
thus y in bool the carrier of T;
take y;
thus thesis by A6,A7;
end;
suppose
A8: for y st y in F holds not b c= y;
take y={}T;
thus y in bool the carrier of T;
take y;
thus thesis by A8;
end;
end;
consider p be Function of B,bool(the carrier of T) such that
A9: for x being object st x in B holds P[x,p.x] from FUNCT_2:sch 1(A5);
take RNG=rng p\{{}};
A10: dom p=B by FUNCT_2:def 1;
thus RNG c= F
proof
let y be object such that
A11: y in RNG;
y in rng p by A11,XBOOLE_0:def 5;
then consider z be object such that
A12: z in dom p and
A13: p.z=y by FUNCT_1:def 3;
reconsider z as Subset of T by A10,A12;
A14: P[z,p.z] by A9,A12;
(ex y st y in F & z c= y) or for y st y in F holds not z c= y;
then p.z in F & z c= p.z or p.z={} by A14;
hence thesis by A11,A13,ZFMISC_1:56;
end;
the carrier of T c= union RNG
proof
let y be object;
assume y in the carrier of T;
then reconsider q=y as Point of T;
consider W be Subset of T such that
A15: q in W and
A16: W in F by A3,PCOMPS_1:3;
W is open by A4,A16;
then consider U be Subset of T such that
A17: U in B and
A18: q in U and
A19: U c= W by A15,YELLOW_9:31;
A20: p.U in rng p by A10,A17,FUNCT_1:def 3;
then reconsider pU=p.U as Subset of T;
P[U,p.U] by A9,A17;
then
A21: U c= pU by A16,A19;
then pU in RNG by A18,A20,ZFMISC_1:56;
hence thesis by A18,A21,TARSKI:def 4;
end;
then [#]T=union RNG by XBOOLE_0:def 10;
hence RNG is Cover of T by SETFAM_1:45;
card rng p c= card B by A10,CARD_2:61;
then card rng p c= omega by A2;
then rng p is countable by CARD_3:def 14;
hence thesis by CARD_3:95;
end;
begin :: The main theorem
theorem Th34:
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;
assume
A1: T is countably_compact;
let F be Subset-Family of T such that
A2: F is Cover of T and
A3: F is open;
M is totally_bounded by A1,Th31;
then T is second-countable by Th32;
then consider G be Subset-Family of T such that
A4: G c= F and
A5: G is Cover of T and
A6: G is countable by A2,A3,Th33;
G is open by A3,A4;
then ex H be Subset-Family of T st H c= G & H is Cover of T & H is
finite by A1,A5,A6;
hence thesis by A4,XBOOLE_1:1;
end;
theorem Th35:
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
defpred P[object,object] means
ex D2 being set st D2 = $2 & $1 in D2;
:: Choice !!!
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 and
A3: A c= union F;
set I=INTERSECTION (F,{A});
card [:F,{A}:] =card F by CARD_1:69;
then card I c= card F by TOPGEN_4:25;
then
A4: I is finite by A1;
A5: for x being object st x in A ex y being object st y in I & P[x,y]
proof
let x be object such that
A6: x in A;
consider y such that
A7: x in y and
A8: y in F by A3,A6,TARSKI:def 4;
take y/\A;
A in {A} by TARSKI:def 1;
hence y/\A in I by A8,SETFAM_1:def 5;
take y/\A;
thus thesis by A6,A7,XBOOLE_0:def 4;
end;
consider p be Function of A,I such that
A9: for x being object st x in A holds P[x,p.x] from FUNCT_2:sch 1(A5);
consider x being object such that
A10: x in A by A2,XBOOLE_0:def 1;
ex y being object st y in I & P[x,y] by A5,A10;
then dom p=A by FUNCT_2:def 1;
then consider t be object such that
A11: t in rng p and
A12: p"{t} is infinite by A2,A4,CARD_2:101;
consider Y,Z be set such that
A13: Y in F and
A14: Z in {A} and
A15: t=Y/\Z by A11,SETFAM_1:def 5;
reconsider Y as Subset of X by A13;
take Y;
A16: Z = A by A14,TARSKI:def 1;
p"{t} c= Y/\A
proof
let z be object such that
A17: z in p"{t};
p.z in {t} by A17,FUNCT_1:def 7;
then
A18: p.z=t by TARSKI:def 1;
P[z,p.z] by A9,A17;
hence thesis by A15,A16,A18;
end;
hence thesis by A12,A13;
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:8,9;
assume that
A1: M is totally_bounded and
A2: M is complete;
now
reconsider NULL=0 as Real;
deffunc F(Nat)=1/(1+$1);
set cM=the carrier of M;
defpred P[object,object] means
for a,b be Subset of M st $1=a & $2=b holds b c=
a & diameter b <= (diameter a)/2;
defpred Q[object] means
for a be Subset of M st a=$1 holds a is bounded & a
is infinite & a is closed;
consider seq be Real_Sequence such that
A3: for n be Nat holds seq.n=F(n) from SEQ_1:sch 1;
set Ns=NULL(#)seq;
A4: for x being object st x in bool cM & Q[x]
ex y being object st y in bool cM & P[x,y] & Q[y]
proof
let x being object such that
A5: x in bool cM and
A6: Q[x];
reconsider X=x as Subset of M by A5;
reconsider X9=X as Subset of T;
set d=diameter X;
per cases by A6,TBSP_1:21;
suppose
A7: d=0;
take Y=X;
thus thesis by A6,A7;
end;
suppose
A8: d>0;
then d/4>0 by XREAL_1:224;
then consider F be Subset-Family of M such that
A9: F is finite and
A10: cM = union F and
A11: for C be Subset of M st C in F ex w be Point of M st C = Ball
(w,d/4) by A1;
X is infinite by A6;
then consider Y be Subset of M such that
A12: Y in F and
A13: Y /\ X is infinite by A9,A10,Th35;
set YX=Y/\X;
A14: ex w be Point of M st Y = Ball(w,d/4) by A11,A12;
then
A15: Y is bounded;
then
A16: diameter YX <=diameter Y by TBSP_1:24,XBOOLE_1:17;
diameter Y<=2*( d /4) by A8,A14,TBSP_1:23,XREAL_1:224;
then
A17: diameter YX<=d/2 by A16,XXREAL_0:2;
reconsider yx=YX as Subset of T;
reconsider CYX=Cl yx as Subset of M;
take CYX;
A18: yx c= Cl yx by PRE_TOPC:18;
A19: yx c= X9 by XBOOLE_1:17;
X is closed by A6;
then
A20: X9 is closed by Th6;
YX is bounded by A15,TBSP_1:14,XBOOLE_1:17;
hence thesis by A13,A17,A18,A20,A19,Th6,Th8,TOPS_1:5;
end;
end;
consider G be Subset-Family of M such that
A21: G is finite and
A22: the carrier of M = union G and
A23: for C be Subset of M st C in G ex w be Point of M st C = Ball(w,1/
2) by A1;
let A be Subset of T;
assume A is infinite;
then consider X be Subset of M such that
A24: X in G and
A25: X /\ A is infinite by A21,A22,Th35;
reconsider XA=X/\A as Subset of M;
reconsider xa=XA as Subset of T;
reconsider CXA=Cl xa as Subset of M;
A26: XA is bounded & diameter XA <=1
proof
A27: ex w be Point of M st X = Ball(w,1/2) by A23,A24;
then
A28: diameter X<=2*(1/2) by TBSP_1:23;
A29: X is bounded by A27;
then diameter XA <=diameter X by TBSP_1:24,XBOOLE_1:17;
hence thesis by A29,A28,TBSP_1:14,XBOOLE_1:17,XXREAL_0:2;
end;
then CXA is bounded by Th8;
then
A30: 0<=diameter CXA by TBSP_1:21;
xa c= Cl xa by PRE_TOPC:18;
then
A31: CXA in bool cM & Q[CXA] by A25,A26,Th6,Th8;
consider f be Function such that
A32: dom f = NAT & rng f c= bool cM and
A33: f.0 = CXA and
A34: for k be Nat holds P[f.k,f.(k+1)] & Q[f.k] from
TREES_2:sch 5(A31,A4);
reconsider f as SetSequence of M by A32,FUNCT_2:2;
A35: for n holds f.n is bounded by A34;
A36: now
let x be object;
assume x in dom f;
then reconsider i=x as Element of NAT;
f.i is infinite by A34;
hence f.x is non empty;
end;
for n holds f.n is closed by A34;
then reconsider f as non-empty pointwise_bounded closed SetSequence of M
by A36,A35,Def1,Def8,FUNCT_1:def 9;
A37: Ns.0=NULL*seq.0 by SEQ_1:9;
for n be Nat holds f.(n+1) c= f.n
by A34;
then
A38: f is non-ascending by KURATO_0:def 3;
set df=diameter f;
defpred N[Nat] means Ns.$1 <= df.$1 & df.$1<=seq.$1;
A39: for n be Nat st N[n] holds N[n+1]
proof
let n be Nat;
assume N[n];
then df.n<=F(n) by A3;
then
A40: (df.n)/2<=F(n)/2 by XREAL_1:72;
set n1=n+1;
A41: diameter (f.n)=df. n by Def2;
diameter (f.n1)<=(diameter (f.n))/2 by A34;
then df.n1<=(df.n)/2 by A41,Def2;
then
A42: df.n1<=F(n)/2 by A40,XXREAL_0:2;
A43: Ns.n1=NULL*seq.n1 by SEQ_1:9;
f.n1 is bounded by Def1;
then
A44: 0<= diameter (f.n1) by TBSP_1:21;
n1+1<=(n1+1)+n by NAT_1:11;
then
A45: F(n1)>=1/(2*n1) by XREAL_1:118;
1/(2*n1)=F(n)/2 by XCMPLX_1:78;
then F(n1)>=df.n1 by A42,A45,XXREAL_0:2;
hence thesis by A3,A44,A43,Def2;
end;
A46: seq.0=1/(1+0) by A3;
A47: for n be Nat holds seq.n=1/(n+1) by A3;
then
A48: seq is convergent by SEQ_4:31;
diameter CXA <= 1 by A26,Th8;
then
A49: N[0] by A33,A30,A46,A37,Def2;
A50: for n be Nat holds N[n] from NAT_1:sch 2(A49,A39);
A51: Ns is convergent by A47,SEQ_2:7,SEQ_4:31;
A52: lim seq=0 by A47,SEQ_4:31;
then
A53: lim Ns=NULL*0 by A47,SEQ_2:8,SEQ_4:31;
then
A54: lim df = 0 by A48,A52,A51,A50,SEQ_2:20;
then meet f is non empty by A2,A38,Th10;
then consider p be object such that
A55: p in meet f by XBOOLE_0:def 1;
reconsider p as Point of T by A55;
reconsider p9=p as Point of M;
A56: df is convergent by A48,A52,A51,A53,A50,SEQ_2:19;
now
let U be open Subset of T;
assume p in U;
then consider r be Real such that
A57: r>0 and
A58: Ball(p9,r) c= U by TOPMETR:15;
r/2 >0 by A57,XREAL_1:215;
then consider n be Nat such that
A59: for m be Nat st n<=m holds |.df.m-0.|<r/2 by A54,A56,
SEQ_2:def 7;
p in f.n by A55,KURATO_0:3;
then
A60: {p} c= f.n by ZFMISC_1:31;
f.n is infinite by A34;
then {p} c<f.n by A60,XBOOLE_0:def 8;
then f.n\{p} <>{} by XBOOLE_1:105;
then consider q be object such that
A61: q in f.n\{p} by XBOOLE_0:def 1;
reconsider q as Point of T by A61;
A62: q in f.n by A61,ZFMISC_1:56;
A63: q in f.n by A61,ZFMISC_1:56;
reconsider q9=q as Point of M;
q<>p by A61,ZFMISC_1:56;
then
A64: dist(p9,q9)<>0 by METRIC_1:2;
reconsider B=Ball(q9,dist(p9,q9)) as Subset of T;
A65: dist(p9,q9)>=0 by METRIC_1:5;
dist(q9,q9)=0 by METRIC_1:1;
then
A66: q in B by A64,A65,METRIC_1:11;
Ball(q9,dist(p9,q9)) in Family_open_set M by PCOMPS_1:29;
then
A67: B is open by PRE_TOPC:def 2;
f.n c= Cl xa by A33,A38,PROB_1:def 4;
then B meets xa by A67,A66,A62,PRE_TOPC:24;
then consider s be object such that
A68: s in B and
A69: s in xa by XBOOLE_0:3;
reconsider s as Point of M by A68;
reconsider s9=s as Point of T;
take s9;
A70: Ns.n=NULL*seq.n by SEQ_1:9;
A71: |.df.n-0.|<r/2 by A59;
A72: f.n is bounded by A34;
df.n>=Ns.n by A50;
then df.n<r/2 by A70,A71,ABSVALUE:def 1;
then
A73: diameter (f.n) < r/2 by Def2;
p in f.n by A55,KURATO_0:3;
then dist(p9,q9)<=diameter (f.n) by A63,A72,TBSP_1:def 8;
then
A74: dist(p9,q9)<r/2 by A73,XXREAL_0:2;
dist(q9,s)<dist(p9,q9) by A68,METRIC_1:11;
then dist(q9,s)<r/2 by A74,XXREAL_0:2;
then
A75: dist(p9,q9)+dist(q9,s)< r/2+r/2 by A74,XREAL_1:8;
dist(p9,s)<=dist(p9,q9)+dist(q9,s) by METRIC_1:4;
then dist(p9,s)<r by A75,XXREAL_0:2;
then
A76: s in Ball(p9,r) by METRIC_1:11;
s in A by A69,XBOOLE_0:def 4;
hence s9 in A/\U & s9<>p by A58,A68,A76,METRIC_1:11,XBOOLE_0:def 4;
end;
hence Der A is non empty by TOPGEN_1:17;
end;
then T is countably_compact by Th27;
hence thesis by Th34;
end;
begin :: Well spaces
theorem Th37:
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 3;
suppose
x in [:X,(the carrier of M)\{a}:];
then consider x1,x2 be object such that
A2: x1 in X and
A3: x2 in (the carrier of M)\{a} and
A4: x=[x1,x2] by ZFMISC_1:def 2;
reconsider x2 as Point of M by A3;
reconsider x1 as set by TARSKI:1;
take x1,x2;
thus thesis by A2,A3,A4,ZFMISC_1:56;
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
A5: x=[y,b] and
A6: y in X & b<>a or y = X & b = a;
per cases by A6;
suppose
A7: y in X & b<>a;
the carrier of M is non empty
proof
assume
A8: the carrier of M is empty;
then a={} by SUBSET_1:def 1;
hence thesis by A7,A8,SUBSET_1:def 1;
end;
then b in (the carrier of M)\{a} by A7,ZFMISC_1:56;
then x in [:X,(the carrier of M)\{a}:] by A5,A7,ZFMISC_1:87;
hence thesis by XBOOLE_0:def 3;
end;
suppose
y = X & b = a;
then x in {[X,a]} by A5,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
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 object,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[object,object,object] means
for x,y be Element of XX st x=$1 & y=$2
for x1,y1 be object, 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 being object st x in XX & y in XX
ex z be object st z in REAL & P[x,y,z]
proof
let x,y be object such that
A2: x in XX and
A3: y in XX;
consider y1 be set,y2 be Point of M such that
A4: y=[y1,y2] and
y1 in X & y2<>a or y1 = X & y2 = a by A3,Th37;
consider x1 be set,x2 be Point of M such that
A5: x=[x1,x2] and
x1 in X & x2<>a or x1 = X & x2 = a by A2,Th37;
per cases;
suppose
A6: x1 = y1;
take d=dist(x2,y2);
thus d in REAL by XREAL_0:def 1;
let x9,y9 be Element of XX such that
A7: x9 = x and
A8: y9 = y;
let x19,y19 be object, x29,y29 be Point of M such that
A9: x9 = [x19,x29] and
A10: y9 = [y19,y29];
A11: x29=x2 by A5,A7,A9,XTUPLE_0:1;
x19=x1 by A5,A7,A9,XTUPLE_0:1;
hence (x19 = y19 implies d = dist(x29,y29) ) & (x19 <> y19 implies d
= dist(x29,a)+dist(a,y29)) by A4,A6,A8,A10,A11,XTUPLE_0:1;
end;
suppose
A12: x1<>y1;
take d=dist(x2,a)+dist(a,y2);
thus d in REAL by XREAL_0:def 1;
let x9,y9 be Element of XX such that
A13: x9=x and
A14: y9=y;
let x19,y19 be object, x29,y29 be Point of M such that
A15: x9 = [x19,x29] and
A16: y9 = [y19,y29];
A17: x29=x2 by A5,A13,A15,XTUPLE_0:1;
x19=x1 by A5,A13,A15,XTUPLE_0:1;
hence (x19 = y19 implies d = dist(x29,y29) ) & (x19 <> y19 implies d
= dist(x29,a)+dist(a,y29)) by A4,A12,A14,A16,A17,XTUPLE_0:1;
end;
end;
consider f being Function of [:XX,XX:],REAL such that
A18: for x,y being object 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 A18;
end;
uniqueness
proof
set XX=[:X,(the carrier of M)\{a}:]\/{[X,a]};
let w1,w2 be Function of [:XX,XX:],REAL such that
A19: for x,y be Element of XX
for x1,y1 be object, 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
A20: for x,y be Element of XX
for x1,y1 be object, 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
A21: x in XX and
A22: y in XX;
consider y1 be set,y2 be Point of M such that
A23: y=[y1,y2] and
y1 in X & y2<>a or y1 = X & y2 = a by A22,Th37;
consider x1 be set,x2 be Point of M such that
A24: x=[x1,x2] and
x1 in X & x2<>a or x1 = X & x2 = a by A21,Th37;
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 A19,A20,A21,A22,A24,A23;
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 object such that
A1: x0 in X by XBOOLE_0:def 1;
set w=well_dist(A,X);
set XX=[:X,(the carrier of M)\{A}:]\/{[X,A]};
thus
A2: 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 Th37;
hence dist(a,a) = w.([X,a],[X,a]) by Def10
.= 0 by A3,A4;
end;
suppose
a<>A;
then
A5: [x0,a] in XX by A1,Th37;
hence dist(a,a) = w.([x0,a],[x0,a]) by Def10
.= 0 by A3,A5;
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
A6: 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
A7: a=A & b<>A;
then
A8: [x0,b] in XX by A1,Th37;
A9: [X,A] in XX by Th37;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx; then
A10: X<>x0 by A1;
then dist(A,A)+dist(A,b) = w.([X,A],[x0,b]) by A9,A8,Def10
.= w.([x0,b],[X,A]) by A6,A9,A8
.= dist(b,A)+dist(A,A) by A9,A8,A10,Def10;
hence dist(a,b)=dist(b,a) by A7;
end;
suppose
A11: a<>A & b=A;
then
A12: [x0,a] in XX by A1,Th37;
A13: [X,A] in XX by Th37;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx; then
A14: X<>x0 by A1;
then dist(A,A)+dist(A,a) = w.([X,A],[x0,a]) by A13,A12,Def10
.= w.([x0,a],[X,A]) by A6,A13,A12
.= dist(a,A)+dist(A,A) by A13,A12,A14,Def10;
hence dist(a,b)=dist(b,a) by A11;
end;
suppose
A15: a<>A & b<>A;
then
A16: [x0,b] in XX by A1,Th37;
A17: [x0,a] in XX by A1,A15,Th37;
hence dist(a,b) = w.([x0,a],[x0,b]) by A16,Def10
.= w.([x0,b],[x0,a]) by A6,A17,A16
.= dist(b,a) by A17,A16,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
A18: 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 Th37;
A19: dist(a,c)=w.(Xa,Xc) by Def10;
A20: dist(a,b)=w.(Xa,Xb) by Def10;
w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc) by A18;
hence dist(a,c)<=dist(a,b)+dist(b,c) by A19,A20,Def10;
end;
suppose
A21: a=A & b=A & c <> A;
dist(a,a)=0 by A2,A18,METRIC_1:1;
hence dist(a,c)<=dist(a,b)+dist(b,c) by A21;
end;
suppose
A22: a=A & b<>A & c = A;
then reconsider Xa=[X,a],Xb=[x0,b],Xc =[X,c] as Element of XX by A1
,Th37;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx; then
A23: x0<>X by A1;
then
A24: dist(b,c)+dist(a,a)=w.(Xb,Xc) by A22,Def10;
A25: dist(a,a)=0 by A2,A18,METRIC_1:1;
A26: w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc) by A18;
dist(a,a)+dist(a,b)=w.(Xa,Xb) by A22,A23,Def10;
hence dist(a,c)<=dist(a,b)+dist(b,c) by A26,A24,A25,Def10;
end;
suppose
A27: a=A & b<>A & c <> A;
then reconsider
Xa=[X,a],Xb=[x0,b],Xc =[x0,c] as Element of XX by A1,Th37;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx; then
A28: x0<>X by A1;
then
A29: dist(a,a)+dist(a,b)=w.(Xa,Xb) by A27,Def10;
A30: dist(a,a)=0 by A2,A18,METRIC_1:1;
A31: w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc) by A18;
dist(a,a)+dist(a,c)=w.(Xa,Xc) by A27,A28,Def10;
hence dist(a,c)<=dist(a,b)+dist(b,c) by A31,A29,A30,Def10;
end;
suppose
A32: a<>A & b=A & c =A;
dist(c,c)=0 by A2,A18,METRIC_1:1;
hence dist(a,c)<=dist(a,b)+dist(b,c) by A32;
end;
suppose
A33: a<>A & b=A & c <>A;
then reconsider
Xa=[x0,a],Xb=[X,b],Xc =[x0,c] as Element of XX by A1,Th37;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx; then
A34: x0<>X by A1;
then
A35: dist(b,b)+dist(b,c)=w.(Xb,Xc) by A33,Def10;
A36: dist(b,b)=0 by A2,A18,METRIC_1:1;
A37: w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc) by A18;
dist(a,b)+dist(b,b)=w.(Xa,Xb) by A33,A34,Def10;
hence dist(a,c)<=dist(a,b)+dist(b,c) by A37,A35,A36,Def10;
end;
suppose
A38: a<>A & b<>A & c = A;
then reconsider
Xa=[x0,a],Xb=[x0,b],Xc =[X,c] as Element of XX by A1,Th37;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx; then
A39: x0<>X by A1;
then
A40: dist(b,c)+dist(c,c)=w.(Xb,Xc) by A38,Def10;
A41: dist(c,c)=0 by A2,A18,METRIC_1:1;
A42: w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc) by A18;
dist(a,c)+dist(c,c)=w.(Xa,Xc) by A38,A39,Def10;
hence dist(a,c)<=dist(a,b)+dist(b,c) by A42,A40,A41,Def10;
end;
suppose
a<>A & b<>A & c <> A;
then reconsider
Xa=[x0,a],Xb=[x0,b],Xc =[x0,c] as Element of XX by A1,Th37;
A43: dist(a,c)=w.(Xa,Xc) by Def10;
A44: dist(a,b)=w.(Xa,Xb) by Def10;
w.(Xa,Xc)<=w.(Xa,Xb)+w.(Xb,Xc) by A18;
hence dist(a,c)<=dist(a,b)+dist(b,c) by A43,A44,Def10;
end;
end;
hence dist(a,c)<=dist(a,b)+dist(b,c);
end;
hence thesis by METRIC_1:4;
end;
assume
A45: w is discerning Reflexive;
now
let a,b be Point of M;
assume
A46: dist(a,b)=0;
now
per cases;
suppose
a=A & b=A;
hence a=b;
end;
suppose
A47: a=A & b<>A;
then reconsider Xa=[X,a],Xb=[x0,b] as Element of XX by A1,Th37;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx; then
x0<>X by A1;
then
A48: dist(a,a)+dist(a,b)=w.(Xa,Xb) by A47,Def10;
dist(a,a)=0 by A2,A45,METRIC_1:1;
then Xa=Xb by A45,A46,A48;
hence a=b by XTUPLE_0:1;
end;
suppose
A49: a<>A & b=A;
then reconsider Xa=[x0,a],Xb=[X,b] as Element of XX by A1,Th37;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx; then
x0<>X by A1;
then
A50: dist(a,b)+dist(b,b)=w.(Xa,Xb) by A49,Def10;
dist(b,b)=0 by A2,A45,METRIC_1:1;
then Xa=Xb by A45,A46,A50;
hence a=b by XTUPLE_0:1;
end;
suppose
a<>A & b<>A;
then reconsider Xa=[x0,a],Xb=[x0,b] as Element of XX by A1,Th37;
dist(a,b)=w.(Xa,Xb) by Def10;
then Xa=Xb by A45,A46;
hence a=b by XTUPLE_0:1;
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;
Lm8: 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] and
y in X & b<>a or y = X & b = a by Th37;
thus w.(A,A) = dist(b,b) by A2,Def10
.= 0 by A1,METRIC_1:1;
end;
then w is Reflexive;
hence thesis;
end;
thus M is symmetric implies W is symmetric
proof
assume M is symmetric;
then reconsider M as symmetric MetrStruct;
reconsider a as Point of M;
now
let A,B be Element of XX;
consider y1 be set,b1 be Point of M such that
A3: A=[y1,b1] and
A4: y1 in X & b1<>a or y1 = X & b1 = a by Th37;
consider y2 be set,b2 be Point of M such that
A5: B=[y2,b2] and
A6: y2 in X & b2<>a or y2 = X & b2 = a by Th37;
now
per cases by A4,A6;
suppose
b1=a & y1=X & b2=a & y2=X;
hence w.(A,B)=w.(B,A) by A3,A5;
end;
suppose
A7: y1 <>y2;
hence w.(A,B) = dist(b1,a)+dist(a,b2) by A3,A5,Def10
.= dist(a,b1)+dist(a,b2)
.= dist(a,b1)+dist(b2,a)
.= w.(B,A) by A3,A5,A7,Def10;
end;
suppose
A8: b1<>a & b2<>a & y1=y2;
hence w.(A,B) = dist(b1,b2) by A3,A5,Def10
.= dist(b2,b1)
.=w.(B,A) by A3,A5,A8,Def10;
end;
end;
hence w.(A,B)=w.(B,A);
end;
then w is symmetric;
hence thesis;
end;
thus M is triangle symmetric Reflexive implies WellSpace(a,X) is triangle
proof
assume
A9: 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
A10: A=[y1,b1] and
y1 in X & b1<>a or y1 = X & b1 = a by Th37;
consider y2 be set,b2 be Point of M such that
A11: B=[y2,b2] and
y2 in X & b2<>a or y2 = X & b2 = a by Th37;
consider y3 be set,b3 be Point of M such that
A12: C=[y3,b3] and
y3 in X & b3<>a or y3 = X & b3 = a by Th37;
now
per cases;
suppose
A13: y1=y2 & y1=y3;
then
A14: dist(b2,b3)=w.(B,C) by A11,A12,Def10;
A15: dist(b1,b2)=w.(A,B) by A10,A11,A13,Def10;
dist(b1,b3)=w.(A,C) by A10,A12,A13,Def10;
hence w.(A,C)<=w.(A,B)+w.(B,C) by A9,A15,A14,METRIC_1:4;
end;
suppose
A16: y1<>y2 & y1=y3;
then
A17: dist(b2,a)+dist(a,b3)=w.(B,C) by A11,A12,Def10;
A18: dist(b1,b2)<=dist(b1,a)+dist(a,b2) by A9,METRIC_1:4;
A19: dist(b2,b3)<=dist(b2,a)+dist(a,b3) by A9,METRIC_1:4;
dist(b1,a)+dist(a,b2)=w.(A,B) by A10,A11,A16,Def10;
then
A20: dist(b1,b2)+dist(b2,b3)<=w.(A,B)+w.(B,C) by A17,A18,A19,XREAL_1:7;
A21: dist(b1,b3)<= dist(b1,b2)+dist(b2,b3) by A9,METRIC_1:4;
dist(b1,b3)=w.(A,C) by A10,A12,A16,Def10;
hence w.(A,C)<=w.(A,B)+w.(B,C) by A20,A21,XXREAL_0:2;
end;
suppose
A22: y1=y2 & y1<>y3;
A23: dist(b1,a)<=dist(b1,b2) + dist(b2,a) by A9,METRIC_1:4;
dist(b1,a)+dist(a,b3)=w.(A,C) by A10,A12,A22,Def10;
then
A24: w.(A,C)<=dist(b1,b2)+dist(b2,a)+dist(a,b3)by A23,XREAL_1:6;
A25: dist(b2,a)+dist(a,b3)=w.(B,C) by A11,A12,A22,Def10;
dist(b1,b2)=w.(A,B) by A10,A11,A22,Def10;
hence w.(A,C)<=w.(A,B)+w.(B,C) by A25,A24;
end;
suppose
A26: y1<>y2 & y1<>y3 & y2<>y3;
A27: 0<=dist(b2,a) by A9,METRIC_1:5;
dist(b2,a)+dist(a,b3)=w.(B,C) by A11,A12,A26,Def10;
then
A28: 0+dist(a,b3)<=w.(B,C) by A27,XREAL_1:6;
A29: 0<=dist(a,b2) by A9,METRIC_1:5;
dist(b1,a)+dist(a,b2)= w.( A,B) by A10,A11,A26,Def10;
then
A30: dist(b1,a)+0<=w.(A,B) by A29,XREAL_1:6;
dist(b1,a)+dist(a,b3)=w.(A,C) by A10,A12,A26,Def10;
hence w.(A,C)<=w.(A,B)+w.(B,C) by A30,A28,XREAL_1:7;
end;
suppose
A31: y1<>y2 & y1<>y3 & y2=y3;
A32: dist(a,b3)<=dist(a,b2)+dist(b2,b3) by A9,METRIC_1:4;
dist(b1,a)+dist(a,b3)=w.(A,C) by A10,A12,A31,Def10;
then
A33: w.(A,C)<=dist(b1,a)+(dist(a,b2)+dist(b2,b3)) by A32,XREAL_1:7;
A34: dist(b2,b3)=w.(B,C) by A11,A12,A31,Def10;
dist(b1,a)+dist(a,b2)= w.( A,B) by A10,A11,A31,Def10;
hence w.(A,C)<=w.(A,B)+w.(B,C) by A34,A33;
end;
end;
hence w.(A,C)<=w.(A,B)+w.(B,C);
end;
then w is triangle;
hence thesis;
end;
assume
A35: M is triangle symmetric Reflexive discerning;
now
let A,B be Element of XX;
consider y1 be set,b1 be Point of M such that
A36: A=[y1,b1] and
A37: y1 in X & b1<>a or y1 = X & b1 = a by Th37;
consider y2 be set,b2 be Point of M such that
A38: B=[y2,b2] and
A39: y2 in X & b2<>a or y2 = X & b2 = a by Th37;
assume
A40: w.(A,B)=0;
now
per cases;
suppose
A41: y1=y2;
then w.(A,B)=dist(b1,b2) by A36,A38,Def10;
hence A=B by A35,A40,A36,A38,A41,METRIC_1:2;
end;
suppose
y1<>y2;
then
A42: w.(A,B)=dist(b1,a)+dist(a,b2) by A36,A38,Def10;
A43: dist(b1,a)>=0 by A35,METRIC_1:5;
dist(a,b2)>=0 by A35,METRIC_1:5;
then dist(b1,a)=0 by A40,A42,A43;
hence A=B by A35,A40,A36,A37,A38,A39,A42,METRIC_1:2;
end;
end;
hence A=B;
end;
then w is discerning;
hence thesis;
end;
registration
let M be Reflexive MetrStruct;
let a be Point of M;
let X be set;
cluster WellSpace(a,X) -> Reflexive;
coherence by Lm8;
end;
registration
let M be symmetric MetrStruct;
let a be Point of M;
let X be set;
cluster WellSpace(a,X) -> symmetric;
coherence by Lm8;
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 Lm8;
end;
registration
let M be MetrSpace;
let a be Point of M;
let X be set;
cluster WellSpace(a,X) -> discerning;
coherence by Lm8;
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 object such that
A1: x0 in X by XBOOLE_0:def 1;
set W=WellSpace(a,X);
assume
A2: WellSpace(a,X) is complete;
let S be sequence of M such that
A3: S is Cauchy;
defpred P[object,object] means
(S.$1<>a implies $2=[x0,S.$1]) & (S.$1=a implies $2 =[X,S.$1]);
A4: for x being object st x in NAT
ex y being object st y in the carrier of W & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider i=x as Nat;
per cases;
suppose
A5: S.i<>a;
take [x0,S.i];
thus thesis by A1,A5,Th37;
end;
suppose
A6: S.x=a;
take [X,a];
thus thesis by A6,Th37;
end;
end;
consider S9 be sequence of W such that
A7: for x being object st x in NAT holds P[x,S9.x] from FUNCT_2:sch 1(A4);
S9 is Cauchy
proof
let r;
assume r>0;
then consider p be Nat such that
A8: for n,m be Nat st p<=n & p<=m holds dist(S.n,S.m)<r by A3;
take p;
let n,m be Nat such that
A9: p <= n and
A10: p <= m;
A11: n in NAT & m in NAT by ORDINAL1:def 12;
per cases;
suppose
A12: S.n=a & S.m=a;
then
A13: [X,S.m]=S9.m by A7,A11;
[X,S.n]=S9.n by A7,A12,A11;
then dist(S9.n,S9.m)=dist(S.n,S.m) by A13,Def10;
hence thesis by A8,A9,A10;
end;
suppose
A14: S.n<>a & S.m=a;
then
A15: [X,S.m]=S9.m by A7,A11;
A16: dist(S.m,S.m)=0 by METRIC_1:1;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx; then
A17: X<>x0 by A1;
[x0,S.n]=S9.n by A7,A14,A11;
then dist(S9.n,S9.m)=dist(S.n,S.m)+dist(S.m,S.m) by A14,A15,A17,Def10;
hence thesis by A8,A9,A10,A16;
end;
suppose
A18: S.n=a & S.m<>a;
then
A19: [x0,S.m]=S9.m by A7,A11;
A20: dist(S.n,S.n)=0 by METRIC_1:1;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx; then
A21: X<>x0 by A1;
[X,S.n]=S9.n by A7,A18,A11;
then dist(S9.n,S9.m)=dist(S.n,S.n)+dist(S.n,S.m) by A18,A19,A21,Def10;
hence thesis by A8,A9,A10,A20;
end;
suppose
A22: S.n<>a & S.m<>a;
then
A23: [x0,S.m]=S9.m by A7,A11;
[x0,S.n]=S9.n by A7,A22,A11;
then dist(S9.n,S9.m)=dist(S.n,S.m) by A23,Def10;
hence thesis by A8,A9,A10;
end;
end;
then S9 is convergent by A2;
then consider L being Element of W such that
A24: for r st r>0 ex n be Nat st for m be Nat st n
<=m holds dist(S9.m,L)<r;
consider L1 be set,L2 be Point of M such that
A25: L=[L1,L2] and
L1 in X & L2<>a or L1 = X & L2 = a by Th37;
take L2;
let r;
assume r>0;
then consider n be Nat such that
A26: for m be Nat st n<=m holds dist(S9.m,L)<r by A24;
take n;
let m be Nat such that
A27: n<=m;
A28: n in NAT & m in NAT by ORDINAL1:def 12;
per cases;
suppose
A29: S.m=a & L1=X;
then S9.m=[X,a] by A7,A28;
then dist(S9.m,L)=dist(S.m,L2) by A25,A29,Def10;
hence thesis by A26,A27;
end;
suppose
A30: S.m=a & L1<>X;
then S9.m=[X,a] by A7,A28;
then
A31: dist(S9.m,L)=dist(S.m,S.m)+dist(S.m,L2) by A25,A30,Def10;
dist(S.m,S.m)=0 by METRIC_1:1;
hence thesis by A26,A27,A31;
end;
suppose
A32: S.m <> a & L1=x0;
then S9.m=[x0,S.m] by A7,A28;
then dist(S9.m,L)=dist(S.m,L2) by A25,A32,Def10;
hence thesis by A26,A27;
end;
suppose
A33: S.m <> a & L1<>x0;
then S9.m=[x0,S.m] by A7,A28;
then
A34: dist(S9.m,L)=dist(S.m,a)+dist(a,L2) by A25,A33,Def10;
A35: dist(S.m,a)+dist(a,L2)>= dist(S.m,L2) by METRIC_1:4;
dist(S9.m,L)<r by A26,A27;
hence thesis by A34,A35,XXREAL_0:2;
end;
end;
theorem Th40:
for M be symmetric triangle Reflexive non empty MetrStruct for a
be Point of M for S be sequence of WellSpace(a,X) st S is Cauchy holds (for Xa
be Point of WellSpace(a,X) st Xa=[X,a] for r st r > 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);
reconsider Xa=[X,a] as Point of W by Th37;
let S be sequence of W such that
A1: S is Cauchy;
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
A2: r > 0 and
A3: for n ex m st m >= n & dist(S.m,Xa) >= r;
consider p be Nat such that
A4: for n,m be Nat st n>=p & m>=p holds dist(S.n,S.m)<r by A1,A2;
consider p9 be Nat such that
A5: p9 >= p and
A6: dist(S.p9,Xa) >= r by A3;
consider Y be set,y be Point of M such that
A7: S.p9=[Y,y] and
Y in X & y<>a or Y = X & y = a by Th37;
ex n,Y st for m st m >= n ex p be Point of M st S.m = [Y,p]
proof
take p9,Y;
let m such that
A8: m >= p9;
consider Z be set,z be Point of M such that
A9: S.m=[Z,z] and
Z in X & z<>a or Z = X & z = a by Th37;
Y = Z
proof
A10: dist(a,z) >=0 by METRIC_1:5;
A11: dist(a,a)=0 by METRIC_1:1;
X=Y or X<>Y;
then dist(S.p9,Xa)=dist(y,a) or dist(S.p9,Xa)=dist(y,a)+0 by A7,A11
,Def10;
then
A12: dist(y,a)+dist(a,z)>=r+0 by A6,A10,XREAL_1:7;
assume Y<>Z;
then
A13: dist(S.p9,S.m)>=r by A7,A9,A12,Def10;
m>=p by A5,A8,XXREAL_0:2;
hence thesis by A4,A5,A13;
end;
hence thesis by A9;
end;
hence thesis;
end;
end;
theorem Th41:
for M be symmetric triangle Reflexive non empty MetrStruct for a
be Point of M holds M is complete implies WellSpace(a,X) is complete
proof
let M be symmetric triangle Reflexive non empty MetrStruct;
let a be Point of M;
set W=WellSpace(a,X);
reconsider Xa=[X,a] as Point of W by Th37;
assume
A1: M is complete;
let S9 be sequence of W such that
A2: S9 is Cauchy;
defpred P[object,object] means ex x st S9.$1=[x,$2];
A3: for x being object st x in NAT
ex y being object st y in the carrier of M & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider i=x as Nat;
consider s1 be set,s2 be Point of M such that
A4: S9.i=[s1,s2] and
s1 in X & s2<>a or s1 = X & s2 = a by Th37;
take s2;
thus thesis by A4;
end;
consider S be sequence of M such that
A5: for x being object st x in NAT holds P[x,S.x] from FUNCT_2:sch 1(A3);
S is Cauchy
proof
let r;
assume r>0;
then consider p be Nat such that
A6: for n,m be Nat st p<=n & p<=m holds dist(S9.n,S9.m)<r
by A2;
take p;
let n,m be Nat such that
A7: p<=n and
A8: p<=m;
A9: n in NAT & m in NAT by ORDINAL1:def 12;
consider x such that
A10: S9.n=[x,S.n] by A5,A9;
consider y such that
A11: S9.m=[y,S.m] by A5,A9;
per cases;
suppose
x=y;
then dist(S9.n,S9.m)=dist(S.n,S.m) by A10,A11,Def10;
hence thesis by A6,A7,A8;
end;
suppose
A12: x<>y;
A13: dist(S.n,S.m) <= dist(S.n,a)+dist(a,S.m) by METRIC_1:4;
A14: dist(S9.n,S9.m)<r by A6,A7,A8;
dist(S9.n,S9.m)=dist(S.n,a)+dist(a,S.m) by A10,A11,A12,Def10;
hence thesis by A13,A14,XXREAL_0:2;
end;
end;
then S is convergent by A1;
then consider L being Element of M such that
A15: for r st r>0 ex n be Nat st for m be Nat st n
<=m holds dist(S.m,L)<r;
per cases by A2,Th40;
suppose
A16: L=a;
take Xa;
A17: dist(a,a)=0 by METRIC_1:1;
let r;
assume r > 0;
then consider n be Nat such that
A18: for m be Nat st n<=m holds dist(S.m,L)<r by A15;
take n;
let m be Nat such that
A19: m >=n;
A20: n in NAT & m in NAT by ORDINAL1:def 12;
consider x such that
A21: S9.m=[x,S.m] by A5,A20;
x=X or x<>X;
then dist(S9.m,Xa)=dist(S.m,L) or dist(S9.m,Xa)=dist(S.m,L)+0 by A16,A21
,A17,Def10;
hence dist(S9.m,Xa)<r by A18,A19;
end;
suppose
A22: for Xa be Point of W st Xa=[X,a] for r st r > 0 ex n st for m st
m >= n holds dist(S9.m,Xa) < r;
take Xa;
let r;
assume r > 0;
then consider n such that
A23: for m st m >= n holds dist(S9.m,Xa) < r by A22;
reconsider n as Nat;
take n;
let m be Nat;
assume m >= n;
hence dist(S9.m,Xa) < r by A23;
end;
suppose
A24: a<>L & ex n,Y st for m st m >= n ex p be Point of M st S9.m = [Y, p];
then consider n,Y such that
A25: for m st m >= n ex p be Point of M st S9.m = [Y,p];
A26: ex s3 be Point of M st S9.n = [Y,s3] by A25;
A27: ex s1 be set,s2 be Point of M st S9.n=[s1,s2] &( s1 in X & s2<>a or
s1 = X & s2 = a) by Th37;
per cases by A27,A26,XTUPLE_0:1;
suppose
Y in X;
then reconsider YL=[Y,L] as Point of W by A24,Th37;
take YL;
let r;
assume r > 0;
then consider p be Nat such that
A28: for m be Nat st p<=m holds dist(S.m,L)<r by A15;
reconsider mm=max(p,n) as Nat by TARSKI:1;
take mm;
let m be Nat such that
A29: m >= mm;
A30: n in NAT & m in NAT by ORDINAL1:def 12;
consider x such that
A31: S9.m=[x,S.m] by A5,A30;
mm >= n by XXREAL_0:25;
then ex pm be Point of M st S9.m = [Y,pm] by A25,A29,XXREAL_0:2;
then x=Y by A31,XTUPLE_0:1;
then
A32: dist(S9.m,YL)=dist(S.m,L) by A31,Def10;
mm >= p by XXREAL_0:25;
then m>=p by A29,XXREAL_0:2;
hence dist(S9.m,YL)<r by A28,A32;
end;
suppose
A33: Y=X;
reconsider n as Nat;
take Xa;
let r such that
A34: r > 0;
take n;
let m be Nat;
assume m >= n;
then
A35: ex t3 be Point of M st S9.m = [Y,t3] by A25;
consider t1 be set,t2 be Point of M such that
A36: S9.m=[t1,t2] and
A37: t1 in X & t2<>a or t1 = X & t2 = a by Th37;
Y=t1 by A36,A35,XTUPLE_0:1;
hence dist(S9.m,Xa)<r by A33,A34,A36,A37,METRIC_1:1;
end;
end;
end;
theorem Th42:
for M be symmetric triangle Reflexive non empty MetrStruct st M
is complete for a be Point of M st ex b be Point of M st dist(a,b)<>0 for X be
infinite set holds WellSpace(a,X) is complete &
ex S be non-empty pointwise_bounded
SetSequence of WellSpace(a,X) st S is closed & S is non-ascending & 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;
assume ex b be Point of M st dist(a,b) <> 0;
then consider b be Point of M such that
A2: dist(a,b)<>0;
let X be infinite set;
set W=WellSpace(a,X);
thus W is complete by A1,Th41;
set TW=TopSpaceMetr W;
consider f being sequence of X such that
A3: f is one-to-one by DICKSON:3;
defpred p[object,object] means $2=[f.$1,b];
A4: b<>a by A2,METRIC_1:1;
A5: for x being object st x in NAT
ex y being object st y in the carrier of TW & p[x,y]
proof
let x be object;
assume x in NAT;
then x in dom f by FUNCT_2:def 1;
then
A6: f.x in rng f by FUNCT_1:def 3;
take [f.x,b];
thus thesis by A4,A6,Th37;
end;
consider s be sequence of the carrier of TW such that
A7: for x being object st x in NAT holds p[x,s.x] from FUNCT_2:sch 1(A5);
deffunc P(object)={s.$1};
A8: for x being object st x in NAT holds P(x) in bool(the carrier of TW)
proof
A9: dom s=NAT by FUNCT_2:def 1;
let x be object;
assume x in NAT;
then s.x in rng s by A9,FUNCT_1:def 3;
then P(x) is Subset of W by SUBSET_1:33;
hence thesis;
end;
consider S be SetSequence of TW such that
A10: for x being object st x in NAT holds S.x=P(x) from FUNCT_2:sch 2(A8);
A11: now
let x1,x2 be object such that
A12: x1 in NAT and
A13: x2 in NAT and
A14: S.x1 = S.x2;
A15: S.x2={s.x2} by A10,A13;
A16: s.x1=[f.x1,b] by A7,A12;
A17: s.x1 in {s.x1} by TARSKI:def 1;
A18: s.x2=[f.x2,b] by A7,A13;
S.x1={s.x1} by A10,A12;
then s.x1=s.x2 by A14,A15,A17,TARSKI:def 1;
then f.x1=f.x2 by A16,A18,XTUPLE_0:1;
hence x1 = x2 by A3,A12,A13,FUNCT_2:19;
end;
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;
dist(a,b)>0 by A2,METRIC_1:5;
then
A19: 2*dist(a,b)>0 by XREAL_1:129;
A20: rng S c= F
proof
let x be object;
assume x in rng S;
then consider y being object such that
A21: y in dom S and
A22: S.y=x by FUNCT_1:def 3;
dom s=NAT by FUNCT_2:def 1;
then
A23: s.y in rngs by A21,FUNCT_1:def 3;
x={s.y} by A10,A21,A22;
hence thesis by A23;
end;
now
let x be object;
assume x in dom S;
then S.x={s.x} by A10;
hence S.x is non empty;
end;
then S is non-empty by FUNCT_1:def 9;
then consider R be non-empty closed SetSequence of TW such that
A24: R is non-ascending and
A25: F is locally_finite & S is one-to-one implies meet R = {} and
A26: 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 A20,Th23;
reconsider R9=R as non-empty SetSequence of W;
A27: now
let x,y be Point of W such that
A28: x in rngs and
A29: y in rngs and
A30: x <> y;
consider y1 be object such that
A31: y1 in dom s and
A32: s.y1=y by A29,FUNCT_1:def 3;
A33: y=[f.y1,b] by A7,A31,A32;
consider x1 be object such that
A34: x1 in dom s and
A35: s.x1=x by A28,FUNCT_1:def 3;
x=[f.x1,b] by A7,A34,A35;
then well_dist(a,X).(x,y)=dist(b,a)+dist(a,b) by A30,A33,Def10;
hence dist(x,y)=2*dist(a,b);
end;
now
let i;
consider Si be Subset-Family of TW such that
A36: R.i = Cl union Si and
A37: Si = {S.j where j is Element of NAT: j >= i} by A26;
reconsider SI=union Si as Subset of W;
now
let x,y being Point of W such that
A38: x in SI and
A39: y in SI;
consider xS be set such that
A40: x in xS and
A41: xS in Si by A38,TARSKI:def 4;
consider j1 be Element of NAT such that
A42: xS=S.j1 and
j1 >= i by A37,A41;
A43: S.j1={s.j1} by A10;
A44: dom s=NAT by FUNCT_2:def 1;
then s.j1 in rngs by FUNCT_1:def 3;
then
A45: x in rngs by A40,A42,A43,TARSKI:def 1;
consider yS be set such that
A46: y in yS and
A47: yS in Si by A39,TARSKI:def 4;
consider j2 be Element of NAT such that
A48: yS=S.j2 and
j2 >= i by A37,A47;
A49: S.j2={s.j2} by A10;
s.j2 in rngs by A44,FUNCT_1:def 3;
then
A50: y in rngs by A46,A48,A49,TARSKI:def 1;
x=y or x<>y;
hence dist(x,y)<=2*dist(a,b) by A19,A27,A45,A50,METRIC_1:1;
end;
then SI is bounded by A19;
hence R9.i is bounded by A36,Th8;
end;
then reconsider R9 as non-empty pointwise_bounded SetSequence of W by Def1;
take R9;
thus R9 is closed & R9 is non-ascending by A24,Th7;
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 A27;
hence thesis by A25,A19,A11,Lm7,FUNCT_2:19;
end;
theorem
ex M be non empty MetrSpace st M is complete & ex S be non-empty
pointwise_bounded SetSequence of M st S is closed & S is non-ascending &
meet S is empty
proof
reconsider D=DiscreteSpace 2 as non empty MetrSpace;
0 in Segm 2 & 1 in Segm 2 by NAT_1:44;
then reconsider a=0,b=1 as Point of D;
TopSpaceMetr D is compact;
then
A1: D is complete by TBSP_1:8;
A2: 1=dist(a,b) by METRIC_1:def 10;
then
A3: ex S be non-empty pointwise_bounded SetSequence of WellSpace(a,NAT) st
S is closed
& S is non-ascending & meet S is empty by A1,Th42;
WellSpace(a,NAT) is complete by A2,A1,Th42;
hence thesis by A3;
end;