:: On Paracompactness of Metrizable Spaces
:: by Leszek Borys
::
:: Received July 23, 1992
:: Copyright (c) 1992-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, SUBSET_1, RELAT_1, WELLORD1, RELAT_2, ZFMISC_1, TARSKI,
XBOOLE_0, FUNCT_1, FINSEQ_1, PRE_TOPC, METRIC_1, SETFAM_1, CARD_5,
RCOMP_1, STRUCT_0, PCOMPS_1, CARD_1, ARYTM_3, XXREAL_0, ORDINAL4,
PARTFUN1, NEWTON, NAT_1, REAL_1, FINSET_1, ARYTM_1, PCOMPS_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
REAL_1, XREAL_0, WELLORD1, RELAT_1, FINSET_1, RELAT_2, NAT_1, SETFAM_1,
XXREAL_0, FUNCT_1, PARTFUN1, FUNCT_2, NEWTON, FINSEQ_1, FINSEQ_2,
STRUCT_0, METRIC_1, PRE_TOPC, TOPS_2, PCOMPS_1;
constructors SETFAM_1, RELAT_2, WELLORD1, WELLORD2, REAL_1, NAT_1, MEMBERED,
NEWTON, TOPS_2, PCOMPS_1, FINSEQ_2;
registrations SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NAT_1, FINSEQ_1,
STRUCT_0, PRE_TOPC, METRIC_1, TOPS_1, XREAL_0, NEWTON;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, WELLORD1, RELAT_2, SETFAM_1;
equalities WELLORD1, XBOOLE_0, STRUCT_0;
expansions TARSKI, WELLORD1, RELAT_2, SETFAM_1, XBOOLE_0;
theorems PCOMPS_1, COMPTS_1, SETFAM_1, TOPS_1, TOPS_2, PRE_TOPC, SUBSET_1,
TARSKI, WELLORD2, ZFMISC_1, NAT_1, PREPOWER, WELLORD1, RELAT_1, FUNCT_1,
METRIC_1, FINSEQ_1, CARD_1, FINSEQ_2, FINSEQ_4, TBSP_1, NEWTON, XBOOLE_0,
XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1;
schemes NAT_1, FUNCT_2, SUBSET_1, RECDEF_1, TREES_2, FRAENKEL, XBOOLE_0,
XFAMILY;
begin :: 1. Selected properties of real numbers
reserve i for Nat;
begin :: 2. Certain functions defined on families of sets
reserve R for Relation;
reserve A for set;
theorem Th1:
R well_orders A implies R |_2 A well_orders A & A = field (R |_2 A)
proof
assume
A1: R well_orders A;
then
A2: R is_reflexive_in A;
A3: R |_2 A is_reflexive_in A
proof
let x be object;
assume x in A;
then [x,x] in R & [x,x] in [:A,A:] by A2,ZFMISC_1:87;
hence thesis by XBOOLE_0:def 4;
end;
A4: R |_2 A is_connected_in A
proof
let x,y be object;
assume that
A5: x in A & y in A and
A6: x <>y;
A7: R is_connected_in A by A1;
now
per cases by A5,A6,A7;
case
A8: [x,y] in R;
[x,y] in [:A,A:] by A5,ZFMISC_1:87;
hence [x,y] in R |_2 A by A8,XBOOLE_0:def 4;
end;
case
A9: [y,x] in R;
[y,x] in [:A,A:] by A5,ZFMISC_1:87;
hence [y,x] in R |_2 A by A9,XBOOLE_0:def 4;
end;
end;
hence thesis;
end;
A10: R |_2 A c= R by XBOOLE_1:17;
A11: R |_2 A is_antisymmetric_in A
proof
let x,y be object;
assume
A12: x in A & y in A & [x,y] in R |_2 A & [y,x] in R |_2 A;
R is_antisymmetric_in A by A1;
hence thesis by A10,A12;
end;
A13: R |_2 A is_well_founded_in A
proof
let Y be set;
assume
A14: Y c= A & Y <> {};
R is_well_founded_in A by A1;
then consider a be object such that
A15: a in Y & R-Seg(a) misses Y by A14;
(R |_2 A)-Seg(a) c= R-Seg(a) by WELLORD1:14;
hence thesis by A15,XBOOLE_1:63;
end;
A16: A c= field (R |_2 A)
proof
let x be object;
assume x in A;
then [x,x] in [:A,A:] & [x,x] in R by A2,ZFMISC_1:87;
then [x,x] in R |_2 A by XBOOLE_0:def 4;
hence thesis by RELAT_1:15;
end;
A17: R |_2 A is_transitive_in A
proof
let x,y,z be object;
assume that
A18: x in A and
A19: y in A and
A20: z in A and
A21: [x,y] in R |_2 A & [y,z] in R |_2 A;
A22: [x,z] in [:A,A:] by A18,A20,ZFMISC_1:87;
R is_transitive_in A by A1;
then [x,z] in R by A10,A18,A19,A20,A21;
hence thesis by A22,XBOOLE_0:def 4;
end;
field (R |_2 A) c= A by WELLORD1:13;
hence thesis by A16,A3,A17,A11,A4,A13;
end;
scheme
MinSet{A()->set,R()->Relation,P[object]}:
ex X be set st X in A() & P[X] & for
Y be set st Y in A() & P[Y] holds [X,Y] in R()
provided
A1: R() well_orders A() and
A2: ex X be set st X in A() & P[X]
proof
consider Y be set such that
A3: for x be object holds x in Y iff x in A() & P[x] from XBOOLE_0:sch 1;
A4: ex x be object st x in Y
by A2,A3;
for x be object holds x in Y implies x in A() by A3;
then Y c= A();
then consider X be object such that
A5: X in Y and
A6: for Z be object st Z in Y holds [X,Z] in R() by A1,A4,WELLORD1:5;
A7: for M be set st M in A() & P[M] holds [X,M] in R()
by A3,A6;
X in A() & P[X] by A3,A5;
hence thesis by A7;
end;
definition
let FX be set, R be Relation, B be Element of FX;
func PartUnion(B,R) -> set equals
union (R-Seg(B));
coherence;
end;
definition
let FX be set, R be Relation;
func DisjointFam(FX,R) -> set means
A in it iff ex B be Element of FX st B in FX & A = B\PartUnion(B,R);
existence
proof
defpred P[set] means
ex B be Element of FX st B in FX & $1 = B\PartUnion(B,R);
consider X being set such that
A1: for x being set holds x in X iff x in bool union FX & P[x] from
XFAMILY:sch 1;
reconsider X as set;
take X;
let A;
thus A in X implies ex B be Element of FX st B in FX & A = B\PartUnion(B,R
) by A1;
assume
A2: ex B be Element of FX st B in FX & A = B\PartUnion(B,R);
then A c= union FX by XBOOLE_1:109,ZFMISC_1:74;
hence thesis by A1,A2;
end;
uniqueness
proof
defpred P[object] means
ex B be Element of FX st B in FX & $1 = B\PartUnion(B
,R);
thus for X1,X2 being set st
(for x be set holds x in X1 iff P[x]) & (for x
be set holds x in X2 iff P[x]) holds X1 = X2 from XFAMILY:sch 3;
end;
end;
definition
let X be set, n be Element of NAT, f be sequence of bool X;
func PartUnionNat(n,f) -> set equals
union (f.:(Seg(n)\{n}));
coherence;
end;
begin :: 3. Paracompactness of metrizable spaces
reserve PT for non empty TopSpace;
reserve PM for MetrSpace;
reserve FX,GX,HX for Subset-Family of PT;
reserve Y,V,W for Subset of PT;
theorem Th2:
PT is regular implies for FX st FX is Cover of PT & FX is open ex
HX st HX is open & HX is Cover of PT & for V st V in HX ex W st W in FX & Cl V
c= W
proof
assume
A1: PT is regular;
let FX;
assume that
A2: FX is Cover of PT and
A3: FX is open;
defpred P[set] means ex V1 being Subset of PT st V1 = $1 & V1 is open & ex W
st W in FX & Cl V1 c= W;
consider HX such that
A4: for V being Subset of PT holds V in HX iff P[V] from SUBSET_1:sch 3;
take HX;
for V being Subset of PT st V in HX holds V is open
proof
let V be Subset of PT;
assume V in HX;
then
ex V1 being Subset of PT st V1 = V & V1 is open & ex W st W in FX & Cl
V1 c= W by A4;
hence thesis;
end;
hence HX is open by TOPS_2:def 1;
the carrier of PT c= union HX
proof
let x be object;
assume x in the carrier of PT;
then reconsider x as Point of PT;
consider V being Subset of PT such that
A5: x in V and
A6: V in FX by A2,PCOMPS_1:3;
reconsider V as Subset of PT;
now
per cases;
suppose
A7: V`<> {};
V is open by A3,A6,TOPS_2:def 1;
then
A8: V` is closed;
x in V`` by A5;
then consider X,Y being Subset of PT such that
A9: X is open and
A10: Y is open and
A11: x in X and
A12: V` c= Y and
A13: X misses Y by A1,A7,A8,COMPTS_1:def 2;
X c= Y` & Y` is closed by A10,A13,SUBSET_1:23;
then
A14: Cl X c= Y` by TOPS_1:5;
Y` c= V by A12,SUBSET_1:17;
then Cl X c= V by A14;
then X in HX by A4,A6,A9;
hence x in union HX by A11,TARSKI:def 4;
end;
suppose
A15: V` = {};
consider X being Subset of PT such that
A16: X=[#](PT);
A17: X is open by A16;
V = ({}(PT))` by A15
.= [#](PT) by PRE_TOPC:6;
then Cl X = V by A16,TOPS_1:2;
then X in HX by A4,A6,A17;
hence x in union HX by A16,TARSKI:def 4;
end;
end;
hence thesis;
end;
hence HX is Cover of PT by SETFAM_1:def 11;
let V be Subset of PT;
assume V in HX;
then ex V1 being Subset of PT st V1 = V & V1 is open & ex W st W in FX & Cl
V1 c= W by A4;
hence thesis;
end;
theorem
for PT,FX st PT is T_2 & PT is paracompact & FX is Cover of PT & FX is
open ex GX st GX is open & GX is Cover of PT & clf GX is_finer_than FX & GX is
locally_finite
proof
let PT,FX;
assume that
A1: PT is T_2 and
A2: PT is paracompact and
A3: FX is Cover of PT & FX is open;
consider HX such that
A4: HX is open & HX is Cover of PT and
A5: for V st V in HX ex W st W in FX & Cl V c= W by A1,A2,A3,Th2,PCOMPS_1:24;
consider GX such that
A6: GX is open & GX is Cover of PT and
A7: GX is_finer_than HX and
A8: GX is locally_finite by A2,A4,PCOMPS_1:def 3;
A9: for V st V in GX ex W st W in FX & (Cl V) c= W
proof
let V;
assume V in GX;
then consider X being set such that
A10: X in HX and
A11: V c= X by A7;
reconsider X as Subset of PT by A10;
consider W such that
A12: W in FX & Cl X c= W by A5,A10;
take W;
Cl V c= Cl X by A11,PRE_TOPC:19;
hence thesis by A12;
end;
clf GX is_finer_than FX
proof
let X be set;
assume
A13: X in clf GX;
then reconsider X as Subset of PT;
consider V such that
A14: X = Cl V and
A15: V in GX by A13,PCOMPS_1:def 2;
consider W such that
A16: W in FX & (Cl V) c= W by A9,A15;
take W;
thus thesis by A14,A16;
end;
hence thesis by A6,A8;
end;
theorem Th4:
for f being Function of [:the carrier of PT,the carrier of PT:],
REAL st f is_metric_of ( the carrier of PT) holds PM = SpaceMetr(the carrier of
PT,f) implies the carrier of PM = the carrier of PT
proof
let f be Function of [:the carrier of PT,the carrier of PT:],REAL;
assume
A1: f is_metric_of the carrier of PT;
assume PM = SpaceMetr(the carrier of PT,f);
then PM = MetrStruct(#the carrier of PT,f#) by A1,PCOMPS_1:def 7;
hence thesis;
end;
theorem
for f being Function of [:the carrier of PT,the carrier of PT:],REAL
st f is_metric_of ( the carrier of PT) holds PM = SpaceMetr(the carrier of PT,f
) implies (FX is Subset-Family of PT iff FX is Subset-Family of PM) by Th4;
reserve Mn for Relation;
reserve n,k,l,q,p,q1 for Nat;
scheme
XXX1 { PM() -> non empty set, UB() -> Subset-Family of PM(),
F(object,object)->Subset of PM(), P[object], Q[object,object,object,object]}:
ex f being sequence of bool bool PM() st f.0 = UB() &
for n being Nat holds f.(n+1) = {union { F(c,n) where c is
Element of PM(): for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds Q
[c,V,n,fq] } where V is Subset of PM() : P[V]} proof
reconsider A = <*UB()*> as Element of (bool bool PM())* by FINSEQ_1:def 11;
defpred T[Nat,FinSequence of bool bool PM(),set] means $3 = $2^<*
{union { F(c,$1) where c is Element of PM(): for fq be Subset-Family of PM(),q
st q <= $1 & fq = $2/.(q+1) holds Q[c,V,$1,fq] } where V is Subset of PM() : P[
V]}*>;
A1: for n being Nat for x being Element of (bool bool PM())* ex y
being Element of (bool bool PM())* st T[n,x,y]
proof
let n be Nat;
let x be Element of (bool bool PM())*;
set T = { union { F(c,n) where c is Element of PM(): for fq be
Subset-Family of PM(),q st q <= n & fq = x/.(q+1) holds Q[c,V,n,fq]} where V is
Subset of PM() : P[V]};
now
let X be object;
reconsider XX=X as set by TARSKI:1;
assume X in T;
then consider V be Subset of PM() such that
A2: X=union { F(c,n) where c is Element of PM(): for fq be
Subset-Family of PM(),q st q <= n & fq = x/.(q+1) holds Q[c,V,n,fq] } and
P[V];
now
let a be object;
assume a in XX;
then consider P be set such that
A3: a in P and
A4: P in { F(c,n) where c is Element of PM(): for fq be
Subset-Family of PM(),q st q <= n & fq = x/.(q+1) holds Q[c,V,n,fq]} by A2,
TARSKI:def 4;
ex c be Element of PM() st P = F(c,n) & for fq be Subset-Family of
PM(),q st q <= n & fq = x/.(q+1) holds Q[c,V,n,fq] by A4;
hence a in PM() by A3;
end;
then XX c= PM();
hence X in bool PM();
end;
then reconsider T as Subset-Family of PM() by TARSKI:def 3;
reconsider T1 = <*T*> as FinSequence of bool bool PM();
consider y be FinSequence of bool bool PM() such that
A5: y = x^T1;
reconsider y as Element of (bool bool PM())* by FINSEQ_1:def 11;
take y;
thus thesis by A5;
end;
consider g be sequence of (bool bool PM())* such that
A6: g.0=A and
A7: for n be Nat holds T[n,g.n,g.(n+1)] from RECDEF_1:sch 2
(A1 );
defpred R[Nat] means len(g.$1) = $1 + 1;
A8: for k st R[k] holds R[k+1]
proof
let k such that
A9: len(g.k) = k+1;
len(g.(k+1))=len((g.k)^<*{ union { F(c,k) where c is Element of PM():
for fq be Subset-Family of PM(),q st q <= k & fq = (g.k)/.(q+1) holds Q[c,V,k,
fq] } where V is Subset of PM() : P[V]}*>) by A7
.= len(g.k)+1 by FINSEQ_2:16;
hence thesis by A9;
end;
deffunc G(Nat) = (g.$1)/.len(g.$1);
consider f be sequence of bool bool PM() such that
A10: for n being Element of NAT holds f.n=G(n) from FUNCT_2:sch 4;
A11: for n being Nat holds f.n=G(n)
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A10;
end;
take f;
len <*UB()*> = 1 by FINSEQ_1:39;
hence f.0 = <*UB()*>/.1 by A6,A11
.= UB() by FINSEQ_4:16;
let n be Nat;
reconsider n as Element of NAT by ORDINAL1:def 12;
defpred T[Nat] means for q st q <= $1 holds f.q = (g.$1)/.(q+1);
A12: R[0] by A6,FINSEQ_1:39;
A13: for n holds R[n] from NAT_1:sch 2(A12,A8);
then
A14: len(g.n)+1=n+1+1;
A15: for k st T[k] holds T[k+1]
proof
let k;
assume
A16: for q st q <= k holds f.q = (g.k)/.(q+1);
let q;
assume
A17: q <= k+1;
now
per cases by A17,XXREAL_0:1;
suppose
A18: q = k+1;
thus f.q=(g.q)/.len(g.q) by A11
.= (g.(k+1))/.(q+1) by A13,A18;
end;
suppose
A19: q < k+1;
A20: q+1>=1 by NAT_1:11;
q+1 <= k+1 by A19,NAT_1:13;
then
A21: q+1 in Seg(k+1) by A20,FINSEQ_1:1;
then q+1 in Seg len(g.k) by A13;
then
A22: q+1 in dom (g.k) by FINSEQ_1:def 3;
A23: q <= k by A19,NAT_1:13;
k+1+1>=k+1 by NAT_1:11;
then Seg(k+1) c= Seg(k+1+1) by FINSEQ_1:5;
then q+1 in Seg(k+1+1) by A21;
then q+1 in Seg(len(g.(k+1))) by A13;
then q+1 in dom(g.(k+1)) by FINSEQ_1:def 3;
hence (g.(k+1))/.(q+1) = (g.(k+1)).(q+1) by PARTFUN1:def 6
.= ((g.k)^<*{ union { F(c,k) where c is Element of PM(): for fq be
Subset-Family of PM(),q st q <= k & fq = (g.k)/.(q+1) holds Q[c,V,k,fq]} where
V is Subset of PM() : P[V]}*>).(q+1) by A7
.= (g.k).(q+1) by A22,FINSEQ_1:def 7
.= (g.k)/.(q+1) by A22,PARTFUN1:def 6
.= f.q by A16,A23;
end;
end;
hence thesis;
end;
deffunc G2(set) = union { F(c,n) where c is Element of PM(): for fq be
Subset-Family of PM(),q st q <= n & fq = (g.n)/.(q+1) holds Q[c,$1,n,fq]};
deffunc F2(set) = union { F(c,n) where c is Element of PM(): for fq be
Subset-Family of PM(),q st q <= n & fq = f.q holds Q[c,$1,n,fq]};
set NF = { F2(V) where V is Subset of PM(): P[V] };
len(g.(n+1))= n+1+1 by A13;
then
A24: dom(g.(n+1)) = Seg(n+1+1) by FINSEQ_1:def 3;
A25: T[0]
proof
let q;
assume q <= 0;
then
A26: q = 0;
thus f.q = (g.q)/.len(g.q) by A11
.= (g.0)/.(q+1) by A6,A26,FINSEQ_1:39;
end;
A27: for n holds T[n] from NAT_1:sch 2(A25,A15);
A28: for V be Subset of PM() st P[V] holds F2(V) = G2(V)
proof
deffunc F1(set) = F($1,n);
let V be Subset of PM() such that
P[V];
defpred P1[set] means for fq be Subset-Family of PM(),q st q <= n & fq = f
.q holds Q[$1,V,n,fq];
defpred P[set] means for fq be Subset-Family of PM(),q st q <= n & fq = (g
.n)/.(q+1) holds Q[$1,V,n,fq];
A29: for c be Element of PM() holds P1[c] iff P[c]
proof
let c be Element of PM();
thus (for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds Q[c,V
,n,fq]) implies for fq be Subset-Family of PM(),q st q <= n & fq = (g.n)/.(q+1)
holds Q[c,V,n,fq]
proof
assume
A30: for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds
Q[c,V,n,fq];
let fq be Subset-Family of PM(),q;
assume that
A31: q <= n and
A32: fq = (g.n)/.(q+1);
fq = f.q by A27,A31,A32;
hence thesis by A30,A31;
end;
assume
A33: for fq be Subset-Family of PM(),q st q <= n & fq = (g.n)/.(q+1)
holds Q[c,V,n,fq];
let fq be Subset-Family of PM(),q;
assume that
A34: q <= n and
A35: fq = f.q;
f.q = (g.n)/.(q+1) by A27,A34;
hence thesis by A33,A34,A35;
end;
{ F1(c) where c is Element of PM(): P1[c] } = { F1(c) where c is
Element of PM(): P[c] } from FRAENKEL:sch 3 (A29);
hence thesis;
end;
A36: NF = { G2(V) where V is Subset of PM() : P[V] } from FRAENKEL:sch 6(A28
);
then
A37: len(g.(n+1))=len((g.n)^<*NF*>) by A7
.= len(g.n)+1 by FINSEQ_2:16;
reconsider n1=n+1 as Element of NAT;
f.(n1) = G(n1) by A11
.= (g.(n1))/.len(g.n1)
.= (g.(n1))/.(len(g.n)+1) by A37
.= g.(n+1).(len(g.n)+1) by A24,A14,FINSEQ_1:4,PARTFUN1:def 6
.= ((g.n)^<*NF*>).(len(g.n)+1) by A7,A36
.= NF by FINSEQ_1:42;
hence thesis;
end;
reconsider jd=1/2 as Real;
scheme
XXX { PM() -> non empty set, UB() -> Subset-Family of PM(),
F(object,object) -> Subset of PM(), P[object], Q[object,object,object]} :
ex f being sequence of bool bool PM() st f.0 = UB() &
for n being Nat holds f.(n+1) = { union { F(c,n) where c is Element
of PM(): Q[c,V,n] & not c in union{union(f.q): q <= n } } where V is Subset of
PM() : P[V]};
defpred Q1[set,set,set,set] means Q[$1,$2,$3] & not $1 in union $4;
consider f being sequence of bool bool PM() such that
A1: f.0 = UB() and
A2: for n being Nat holds
f.(n+1) = { union { F(c,n) where c is Element of PM():
for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds Q1[c,V,n,fq] }
where V is Subset of PM() : P[V]} from XXX1;
take f;
thus f.0 = UB() by A1;
let n be Nat;
deffunc F2(set) = union { F(c,n) where c is Element of PM(): for fq be
Subset-Family of PM(),q st q <= n & fq = f.q holds Q[c,$1,n] & not c in union(
fq) };
deffunc G2(set) = union { F(c,n) where c is Element of PM(): Q[c,$1,n] & not
c in union{union(f.q): q <= n } };
set fxxx1 = { F2(V) where V is Subset of PM() : P[V] };
set fxxx = { G2(V) where V is Subset of PM() : P[V] };
A3: now
deffunc F(set) = F($1,n);
let V be Subset of PM();
assume P[V];
defpred P[set] means for fq be Subset-Family of PM(),q st q <= n & fq = f.
q holds Q[$1,V,n] & not $1 in union(fq);
defpred Q1[set] means Q[$1,V,n] & not $1 in union{union(f.q1): q1 <= n };
A4: now
let c be Element of PM();
A5: ( for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds not c
in union(fq)) iff not c in union{union(f.q): q <= n }
proof
thus (for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds not
c in union(fq)) implies not c in union{union(f.q): q <= n }
proof
assume
A6: for fq be Subset-Family of PM(),q st q <= n & fq = f.q holds
not c in union(fq);
assume c in union{union(f.q): q <= n};
then consider C be set such that
A7: c in C and
A8: C in {union(f.q): q <= n}by TARSKI:def 4;
consider q being Nat such that
A9: C = union(f.q) & q <= n by A8;
reconsider q as Element of NAT by ORDINAL1:def 12;
f.q = f.q;
hence contradiction by A6,A7,A9;
end;
assume
A10: not c in union{union(f.q): q <= n};
let fq be Subset-Family of PM(),q;
assume q <= n & fq = f.q;
then union(fq) in {union(f.p): p <= n};
hence thesis by A10,TARSKI:def 4;
end;
thus P[c] iff Q1[c]
proof
hereby
reconsider q = n as Element of NAT by ORDINAL1:def 12;
assume
A11: for fq be Subset-Family of PM(),q st q <= n & fq = f.q
holds Q[c,V,n] & not c in union(fq);
ex fq be Subset-Family of PM() st fq = f.q;
hence Q[c,V,n] by A11;
thus not c in union{union(f.p): p <= n } by A5,A11;
end;
assume Q[c,V,n] & not c in union{union(f.q): q <= n };
hence thesis by A5;
end;
end;
{ F(c) where c is Element of PM(): P[c] } = { F(c) where c is Element
of PM(): Q1[c] } from FRAENKEL:sch 3(A4);
hence F2(V) = G2(V);
end;
fxxx1 = fxxx from FRAENKEL:sch 6(A3);
hence thesis by A2;
end;
theorem Th6:
PT is metrizable implies for FX being Subset-Family of PT st FX
is Cover of PT & FX is open ex GX being Subset-Family of PT st GX is open & GX
is Cover of PT & GX is_finer_than FX & GX is locally_finite
proof
assume PT is metrizable;
then consider
metr being Function of [:the carrier of PT,the carrier of PT:],REAL
such that
A1: metr is_metric_of (the carrier of PT) and
A2: Family_open_set( SpaceMetr (the carrier of PT,metr) ) = the topology
of PT by PCOMPS_1:def 8;
let FX;
consider R such that
A3: R well_orders FX by WELLORD2:17;
defpred P1[set] means $1 in FX;
consider Mn such that
A4: Mn = R |_2 FX;
assume that
A5: FX is Cover of PT and
A6: FX is open;
consider PM being MetrSpace such that
A7: PM = SpaceMetr(the carrier of PT,metr);
reconsider PM as non empty MetrSpace by A1,A7,PCOMPS_1:36;
deffunc F1(Element of PM,Nat) = Ball($1,1/(2 |^($2+1)));
set UB = {union {Ball(c,jd) where c is Element of PM: c in V\PartUnion(V,Mn
) & Ball(c,3/2) c= V} where V is Subset of PM: V in FX};
UB is Subset-Family of PM
proof
reconsider UB as set;
UB c= bool the carrier of PM
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in UB;
then consider V be Subset of PM such that
A8: x = union {Ball(c,jd) where c is Element of PM: c in V\
PartUnion(V,Mn) & Ball(c,3/2) c= V} and
V in FX;
xx c= the carrier of PM
proof
let y be object;
assume y in xx;
then consider W be set such that
A9: y in W and
A10: W in {Ball(c,jd) where c is Element of PM: c in V\PartUnion(
V,Mn) & Ball(c,3/2) c= V} by A8,TARSKI:def 4;
ex c be Element of PM st W = Ball(c,jd) & c in V\ PartUnion(V,Mn)
& Ball(c,3/2) c= V by A10;
hence thesis by A9;
end;
hence thesis;
end;
hence thesis;
end;
then reconsider UB as Subset-Family of PM;
defpred Q1[Element of PM, Subset of PM,Nat] means $1 in $2\
PartUnion($2,Mn) & Ball($1,3/(2 |^ ($3+1))) c= $2;
consider f being sequence of bool bool the carrier of PM such that
A11: f.0 = UB and
A12: for n being Nat
holds f.(n+1) = {union { F1(c,n) where c is Element of PM: Q1
[c,V,n] & not c in union{union (f.q): q <= n } } where V is Subset of PM: P1[V]
} from XXX;
defpred P2[set] means ex n being Nat st $1 in f.n;
consider GX being Subset-Family of PM such that
A13: for X being Subset of PM holds X in GX iff P2[X] from SUBSET_1:sch
3;
reconsider GX as Subset-Family of PT by A1,A7,Th4;
take GX;
A14: for X being Subset of PT st X in GX holds X is open
proof
let X be Subset of PT;
assume
A15: X in GX;
then reconsider X as Subset of PM;
consider n being Nat such that
A16: X in f.n by A13,A15;
now
per cases;
suppose
A17: n=0;
thus X in the topology of PT
proof
consider V be Subset of PM such that
A18: X = union {Ball(c,jd) where c is Element of PM: c in V\
PartUnion(V,Mn) & Ball(c,3/2) c= V} and
V in FX by A11,A16,A17;
set NF = {Ball(c,jd) where c is Element of PM: c in V\PartUnion(V,
Mn) & Ball(c,3/2) c= V};
NF c= bool the carrier of PM
proof
let a be object;
assume a in NF;
then
ex c be Element of PM st a = Ball(c,jd) & c in V\ PartUnion(V
,Mn) & Ball(c,3/2) c= V;
hence thesis;
end;
then reconsider NF as Subset-Family of PM;
NF c= Family_open_set(PM)
proof
let a be object;
assume a in NF;
then
ex c be Element of PM st a = Ball(c,jd) & c in V\ PartUnion(V
,Mn) & Ball(c,3/2) c= V;
hence thesis by PCOMPS_1:29;
end;
hence thesis by A2,A7,A18,PCOMPS_1:32;
end;
end;
suppose
n>0;
then consider k being Nat such that
A19: n = k + 1 by NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
thus X in the topology of PT
proof
X in {union { Ball(c,1/(2 |^ (k+1))) where c is Element of PM:
c in V\PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union{union(f.q
) where q is Nat: q <= k } } where V is Subset of PM: V in FX} by
A12,A16,A19;
then consider V be Subset of PM such that
A20: X = union { Ball(c,1/(2 |^ (k+1))) where c is Element of PM
: c in V\PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union{union(f
.q) where q is Nat: q <= k } } and
V in FX;
reconsider NF = { Ball(c,1/(2 |^ (k+1))) where c is Element of PM: c
in V\PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union { union(f.q
) where q is Nat: q <= k } } as set;
NF c= bool the carrier of PM
proof
let a be object;
assume a in NF;
then ex c be Element of PM st a = Ball(c,1/(2 |^ (k+1))) & c in V\
PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union { union(f.l ): l
<= k};
hence thesis;
end;
then reconsider NF as Subset-Family of PM;
NF c= Family_open_set(PM)
proof
let a be object;
assume a in NF;
then ex c be Element of PM st a = Ball(c,1/(2 |^ (k+1))) & c in V\
PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union{union(f.l): l <=
k};
hence thesis by PCOMPS_1:29;
end;
hence thesis by A2,A7,A20,PCOMPS_1:32;
end;
end;
end;
hence thesis by PRE_TOPC:def 2;
end;
hence GX is open by TOPS_2:def 1;
A21: Mn well_orders FX by A3,A4,Th1;
the carrier of PT c= union GX
proof
let x be object;
defpred P1[set] means x in $1;
assume
A22: x in the carrier of PT;
then reconsider x9=x as Element of PM by A1,A7,Th4;
ex G be Subset of PT st x in G & G in FX by A5,A22,PCOMPS_1:3;
then
A23: ex G be set st G in FX & P1[G];
consider X be set such that
A24: X in FX and
A25: P1[X] and
A26: for Y be set st Y in FX & P1[Y] holds [X,Y] in Mn from MinSet(A21,A23 );
reconsider X as Subset of PT by A24;
X is open by A6,A24,TOPS_2:def 1;
then
A27: X in Family_open_set(PM) by A2,A7,PRE_TOPC:def 2;
reconsider X as Subset of PM by A1,A7,Th4;
consider r be Real such that
A28: r>0 and
A29: Ball(x9,r) c= X by A25,A27,PCOMPS_1:def 4;
defpred P2[Nat] means 3/(2 |^ $1) <= r;
ex k be Nat st P2[k] by A28,PREPOWER:92;
then
A30: ex k be Nat st P2[k];
consider k be Nat such that
A31: P2[k] and
for l be Nat st P2[l] holds k <= l from NAT_1:sch 5(A30 );
2 |^ (k+1) = 2 |^ k * 2 by NEWTON:6;
then 2 |^ k > 0 & 2 |^ (k+1) >= 2 |^ k by PREPOWER:6,XREAL_1:151;
then
A32: 3/2 |^ (k+1) <= 3/2 |^ k by XREAL_1:118;
assume
A33: not x in union GX;
A34: for V be set,n st V in f.n holds not x in V
proof
let V be set;
let n;
reconsider m = n as Element of NAT by ORDINAL1:def 12;
A35: f.m in bool bool the carrier of PM;
assume V in f.n;
then V in GX by A13,A35;
hence thesis by A33,TARSKI:def 4;
end;
A36: for n holds not x in union (f.n)
proof
let n;
assume x in union (f.n);
then ex V be set st x in V & V in f.n by TARSKI:def 4;
hence contradiction by A34;
end;
now
set W = union{ Ball(y,1/(2 |^ (k+1))) where y is Element of PM: y in X\
PartUnion(X,Mn) & Ball(y,3/(2 |^ (k+1))) c= X & not y in union{ union(f.q)
where q is Nat: q <= k} };
A37: x in W
proof
A38: not x9 in union { union(f.q) where q is Nat: q <= k}
proof
assume x9 in union { union(f.q) where q is Nat: q <= k};
then consider D be set such that
A39: x9 in D and
A40: D in { union(f.q) where q is Nat: q <= k} by TARSKI:def 4;
ex q be Nat st D = union (f.q) & q <= k by A40;
hence contradiction by A36,A39;
end;
not x9 in PartUnion(X,Mn)
proof
reconsider FX as set;
assume x9 in PartUnion(X,Mn);
then consider M be set such that
A41: x9 in M and
A42: M in Mn-Seg(X) by TARSKI:def 4;
A43: M <> X by A42,WELLORD1:1;
A44: Mn is_antisymmetric_in FX by A21;
A45: [M,X] in Mn by A42,WELLORD1:1;
then M in field Mn by RELAT_1:15;
then
A46: M in FX by A3,A4,Th1;
then [X,M] in Mn by A26,A41;
hence contradiction by A24,A43,A45,A46,A44;
end;
then
A47: x9 in X\PartUnion(X,Mn) by A25,XBOOLE_0:def 5;
consider A be Subset of PM such that
A48: A = Ball(x9,1/(2 |^ (k+1)));
0 < 2 |^ (k+1) by PREPOWER:6;
then
A49: x in A by A48,TBSP_1:11,XREAL_1:139;
Ball(x9,3/(2 |^ (k+1))) c= Ball(x9,r) by A31,A32,PCOMPS_1:1,XXREAL_0:2;
then Ball(x9,3/(2 |^ (k+1))) c= X by A29;
then A in { Ball(y,1/(2 |^ (k+1))) where y is Element of PM: y in X\
PartUnion(X,Mn) & Ball(y,3/(2 |^ (k+1))) c= X & not y in union { union(f.q)
where q is Nat: q <= k}} by A48,A47,A38;
hence thesis by A49,TARSKI:def 4;
end;
reconsider W as set;
W in {union{ Ball(y,1/(2 |^ (k+1))) where y is Element of PM: y in
V\PartUnion(V,Mn) & Ball(y,3/(2 |^ (k+1))) c= V & not y in union { union(f.q)
where q is Nat: q <= k}} where V is Subset of PM: V in FX} by A24;
then W in f.(k+1) by A12;
hence ex W be set,l be Element of NAT st W in f.l & x in W by A37;
end;
hence contradiction by A34;
end;
hence
A50: GX is Cover of PT by SETFAM_1:def 11;
for X be set st X in GX ex Y be set st Y in FX & X c= Y
proof
let X be set;
assume
A51: X in GX;
then reconsider X as Subset of PM;
consider n being Nat such that
A52: X in f.n by A13,A51;
now
per cases;
suppose
A53: n=0;
thus ex Y be set st Y in FX & X c= Y
proof
consider V be Subset of PM such that
A54: X = union {Ball(c,1/2) where c is Element of PM: c in V\
PartUnion(V,Mn) & Ball(c,3/2) c= V} and
A55: V in FX by A11,A52,A53;
set NF = {Ball(c,1/2) where c is Element of PM: c in V\PartUnion(V,
Mn) & Ball(c,3/2) c= V};
NF c= bool the carrier of PM
proof
let a be object;
assume a in NF;
then ex c be Element of PM st a = Ball(c,1/2) & c in V\ PartUnion(
V,Mn) & Ball(c,3/2) c= V;
hence thesis;
end;
then reconsider NF as Subset-Family of PM;
A56: for W be set st W in NF holds W c= V
proof
let W be set;
assume W in NF;
then consider c be Element of PM such that
A57: W = Ball(c,1/2) and
c in V\PartUnion(V,Mn) and
A58: Ball(c,3/2) c= V;
Ball(c,1/2) c= Ball(c,3/2) by PCOMPS_1:1;
hence thesis by A57,A58;
end;
reconsider V as set;
take Y = V;
thus Y in FX by A55;
thus thesis by A54,A56,ZFMISC_1:76;
end;
end;
suppose
n>0;
then consider k being Nat such that
A59: n = k + 1 by NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
thus ex Y be set st Y in FX & X c= Y
proof
X in {union { Ball(c,1/(2 |^ (k+1))) where c is Element of PM:
c in V\PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union { union(f
.q) where q is Nat: q <= k}} where V is Subset of PM: V in FX} by
A12,A52,A59;
then consider V be Subset of PM such that
A60: X = union { Ball(c,1/(2 |^ (k+1))) where c is Element of PM: c
in V\PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union{union
(f.q) where q is Nat: q <= k}} and
A61: V in FX;
reconsider NF = { Ball(c,1/(2 |^ (k+1))) where c is Element of PM: c
in V\PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union{union(f.q)
where q is Nat: q <= k}} as set;
NF c= bool the carrier of PM
proof
let a be object;
assume a in NF;
then ex c be Element of PM st a = Ball(c,1/(2 |^ (k+1))) & c in V\
PartUnion(V,Mn) & Ball(c,3/(2 |^ (k+1))) c= V & not c in union { union(f .q)
where q is Nat: q <= k};
hence thesis;
end;
then reconsider NF as Subset-Family of PM;
A62: for W be set st W in NF holds W c= V
proof
let W be set;
assume W in NF;
then consider c be Element of PM such that
A63: W = Ball(c,1/(2 |^ (k+1))) and
c in V\PartUnion(V,Mn) and
A64: Ball(c,3/(2 |^ (k+1))) c= V and
not c in union { union(f.q) where q is Nat: q <= k};
Ball(c,1/(2 |^ (k+1))) c= Ball(c,3/(2 |^ (k+1))) by PCOMPS_1:1
,XREAL_1:72;
hence thesis by A63,A64;
end;
reconsider V as set;
take Y = V;
thus Y in FX by A61;
thus thesis by A60,A62,ZFMISC_1:76;
end;
end;
end;
hence thesis;
end;
hence GX is_finer_than FX;
for x be Point of PT ex W be Subset of PT st x in W & W is open & { V
: V in GX & V meets W } is finite
proof
let x be Point of PT;
reconsider x9=x as Element of PM by A1,A7,Th4;
consider X be Subset of PT such that
A65: x in X and
A66: X in GX by A50,PCOMPS_1:3;
reconsider X as Subset of PT;
X is open by A14,A66;
then X in Family_open_set(PM) by A2,A7,PRE_TOPC:def 2;
then consider r be Real such that
A67: r>0 and
A68: Ball(x9,r) c= X by A65,PCOMPS_1:def 4;
consider m be Nat such that
A69: 1/(2 |^ m) <= r by A67,PREPOWER:92;
defpred P3[set] means X in f.$1;
ex n be Nat st P3[n] by A13,A66;
then
A70: ex n be Nat st P3[n];
consider k be Nat such that
A71: P3[k] and
for l be Nat st P3[l] holds k <= l from NAT_1:sch 5(A70 );
consider W be Subset of PM such that
A72: W = Ball(x9,1/(2 |^ (m+1+k+1)));
reconsider W as Subset of PT by A1,A7,Th4;
A73: { V : V in GX & V meets W } is finite
proof
defpred P4[object,set] means $1 in f.$2;
set NZ={ V : V in GX & V meets W };
A74: for p be object st p in NZ ex n being Nat st P4[p,n]
proof
let p be object;
assume p in NZ;
then ex V be Subset of PT st p = V & V in GX & V meets W;
hence thesis by A13;
end;
consider g be Function such that
A75: dom g = NZ and
A76: for y be object st y in NZ
ex n being Nat st g.y=n & P4[y,n] &
for t be Nat st P4[y,t] holds n <=t from TREES_2:sch 4(A74);
A77: rng g c= {i: i < (m+1+k+1)}
proof
let t be object;
assume t in rng g;
then consider a be object such that
A78: a in dom g and
A79: t = g.a by FUNCT_1:def 3;
assume
A80: not t in {i: i < (m+1+k+1)};
A81: ex n be Nat st g.a = n & a in f.n &
for p be Nat st a in f.p holds n <= p by A75,A76,A78;
then reconsider t as Element of NAT by A79,ORDINAL1:def 12;
consider V such that
A82: a=V and
V in GX and
A83: V meets W by A75,A78;
consider y being object such that
A84: y in V and
A85: y in W by A83,XBOOLE_0:3;
A86: t >= (m+1+k+1) by A80;
now
per cases;
suppose
t=0;
hence contradiction by A80;
end;
suppose
t>0;
then consider l be Nat such that
A87: t=l+1 by NAT_1:6;
reconsider l as Element of NAT by ORDINAL1:def 12;
A88: V in {union { Ball(c,1/(2 |^ (l+1))) where c is Element of
PM: c
in Y\PartUnion(Y,Mn) & Ball(c,3/(2 |^ (l+1))) c= Y & not c in union{union
(f.q) where q is Nat: q <= l}} where Y is Subset of PM: Y in FX} by
A12,A79,A81,A82,A87;
2 |^ t >= 2 |^ (m+1+k+1) & 2 |^ (m+1+k+1) > 0 by A86,PREPOWER:6,93;
then
A89: 1/(2 |^ (m+1+k+1)) >= 1/(2 |^ t) by XREAL_1:118;
consider Y be Subset of PM such that
A90: V = union { Ball(c,1/(2 |^ (l+1))) where c is Element of
PM: c
in Y\PartUnion(Y,Mn) & Ball(c,3/(2 |^ (l+1))) c= Y & not c in union{union
(f.q) where q is Nat: q <= l}} and
Y in FX by A88;
reconsider NF = { Ball(c,1/(2 |^ (l+1) ) ) where c is Element of
PM: c
in Y\PartUnion(Y,Mn) & Ball(c,3/(2 |^ (l+1))) c= Y & not c in union{union
(f.q) where q is Nat: q <= l}} as set;
consider T be set such that
A91: y in T and
A92: T in NF by A84,A90,TARSKI:def 4;
reconsider y as Element of PM by A85;
consider c be Element of PM such that
A93: T = Ball(c,1/(2 |^ (l+1))) and
c in Y\PartUnion(Y,Mn) and
Ball(c,3/(2 |^ (l+1))) c= Y and
A94: not c in union{union (f.q) where q is Nat: q
<= l} by A92;
dist(c,y) < 1/(2 |^ t) by A87,A91,A93,METRIC_1:11;
then dist(c,y) < 1/(2 |^ (m+1+k+1)) by A89,XXREAL_0:2;
then
A95: dist(c,y) + dist(y,x9) < 1/(2 |^ (m+1+k+1)) + dist(y,x9) by
XREAL_1:6;
A96: for t be Element of NAT st t < l holds not c in union(f.t)
proof
let t be Element of NAT;
assume t < l;
then
A97: union(f.t) in {union(f.q) where q is Nat: q <= l};
assume c in union(f.t);
hence contradiction by A94,A97,TARSKI:def 4;
end;
A98: dist(c,x9) >= 1/(2 |^ m)
proof
assume not dist(c,x9) >= 1/(2 |^ m);
then dist(x9,c) < r by A69,XXREAL_0:2;
then c in Ball(x9,r) by METRIC_1:11;
then
A99: c in union (f.k) by A71,A68,TARSKI:def 4;
A100: k <> l
proof
assume k=l;
then union (f.k) in {union(f.q) where q is Nat: q <= l};
hence contradiction by A94,A99,TARSKI:def 4;
end;
l >= k+(m+1) & k+(m+1)>=k by A86,A87,NAT_1:11,XREAL_1:6;
then k <= l by XXREAL_0:2;
then k in NAT & k < l by A100,ORDINAL1:def 12,XXREAL_0:1;
hence contradiction by A96,A99;
end;
dist(c,y) + dist(y,x9) >= dist(c,x9) by METRIC_1:4;
then dist(c,y) + dist(y,x9) >= 1/(2 |^ m) by A98,XXREAL_0:2;
then 1/(2 |^ (m+1+k+1)) + dist(y,x9) > 1/(2 |^ m) by A95,XXREAL_0:2
;
then
A101: dist(y,x9) >= 1/(2 |^ m) - 1/(2 |^ (m+1+k+1)) by XREAL_1:19;
(2 |^ (1+k))*2>=2 by PREPOWER:11,XREAL_1:151;
then
A102: ((2 |^ (1+k))*2)-1>=2-1 by XREAL_1:9;
2 |^ (1+k+1) <> 0 by PREPOWER:5;
then 1/(2 |^ m) - 1/(2 |^ (m+1+k+1)) = (1*(2 |^ (1+k+1)))/((2 |^
m)*(2 |^ (1+k+1))) - 1/(2 |^ (m+1+k+1)) by XCMPLX_1:91
.= (1*(2 |^ (1+k+1)))/(2 |^ (m+((1+k)+1))) - 1/(2 |^ (m+1+k+1)
) by NEWTON:8
.= ((2 |^ (1+k))*2)/(2 |^ (m+1+k+1)) - 1/(2 |^ (m+1+k+1)) by
NEWTON:6
.= (((2 |^ (1+k))*2)-1)/(2 |^ (m+1+k+1)) by XCMPLX_1:120;
then 1 /(2 |^ m) - 1/(2 |^ (m+1+k+1)) >= 1/(2 |^ (m+1+k+1)) by A102
,XREAL_1:72;
then dist(y,x9) >= 1/(2 |^ (m+1+k+1)) by A101,XXREAL_0:2;
hence contradiction by A72,A85,METRIC_1:11;
end;
end;
hence contradiction;
end;
for x1,x2 be object st x1 in dom g & x2 in dom g & g.x1 = g.x2
holds x1 = x2
proof
let x1,x2 be object;
assume that
A103: x1 in dom g and
A104: x2 in dom g and
A105: g.x1 = g.x2;
assume
A106: x1<>x2;
reconsider x1,x2 as set by TARSKI:1;
ex V2 be Subset of PT st x2=V2 & V2 in GX & V2 meets W by A75,A104;
then consider w2 being object such that
A107: w2 in W and
A108: w2 in x2 by XBOOLE_0:3;
consider n1 be Nat such that
A109: g.x1 = n1 and
A110: x1 in f.n1 and
for t be Nat st x1 in f.t holds n1 <= t by A75,A76,A103;
ex V1 be Subset of PT st x1=V1 & V1 in GX & V1 meets W by A75,A103;
then consider w1 being object such that
A111: w1 in W and
A112: w1 in x1 by XBOOLE_0:3;
reconsider w1, w2 as Element of PM by A111,A107;
A113: ex n2 be Nat st g.x2 = n2 & x2 in f.n2 & for t be
Nat st x2 in f.t holds n2 <= t by A75,A76,A104;
now
per cases;
suppose
A114: n1=0;
m+k+1 >= 1 by NAT_1:11;
then 2 |^ (m+1+k) >= 2 |^ 1 by PREPOWER:93;
then 2 |^ (m+1+k) >= 2;
then
A115: 1/(2 |^ (m+1+k)) <= 1/2 by XREAL_1:118;
A116: 2/(2 |^ (m+1+k+1)) =(1*2)/(2 |^ (m+1+k)*2) by NEWTON:6
.= 1/(2 |^ (m+1+k)) by XCMPLX_1:91;
(1/2 + 1/(2 |^ (m+1+k+1))) + (1/(2 |^ (m+1+k+1)) + 1/2) = (1
+1)/2 + (1/(2 |^ (m+1+k+1)) + 1/(2 |^ (m+1+k+1)))
.= 2/2 + 2/(2 |^ (m+1+k+1)) by XCMPLX_1:62;
then (1/2 + 1/(2 |^ (m+1+k+1))) + (1/(2 |^ (m+1+k+1)) + 1/2) - 2/
2 = 1/(2 |^ (m+1+k)) by A116;
then
A117: (1/2 + 1/(2 |^ (m+1+k+1))) + (1/(2 |^ (m+1+k+1)) + 1/2) <= 2
/2 + 1/2 by A115,XREAL_1:20;
A118: Mn is_connected_in FX by A21;
A119: dist(x9,w2) < 1/(2 |^ (m+1+k+1)) by A72,A107,METRIC_1:11;
consider M1 be Subset of PM such that
A120: x1 = union {Ball(c,1/2) where c is Element of PM: c in
M1\PartUnion(M1,Mn) & Ball(c,3/2) c= M1} and
A121: M1 in FX by A11,A110,A114;
consider k1 be set such that
A122: w1 in k1 and
A123: k1 in {Ball(c,1/2) where c is Element of PM: c in M1\
PartUnion(M1,Mn) & Ball(c,3/2) c= M1} by A112,A120,TARSKI:def 4;
consider c1 be Element of PM such that
A124: k1 = Ball(c1,1/2) and
A125: c1 in M1\PartUnion(M1,Mn) and
A126: Ball(c1,3/2) c= M1 by A123;
A127: dist(c1,w1) < 1/2 by A122,A124,METRIC_1:11;
consider M2 be Subset of PM such that
A128: x2 = union {Ball(c,1/2) where c is Element of PM: c in
M2\PartUnion(M2,Mn) & Ball(c,3/2) c= M2} and
A129: M2 in FX by A11,A105,A109,A113,A114;
consider k2 be set such that
A130: w2 in k2 and
A131: k2 in {Ball(c,1/2) where c is Element of PM: c in M2\
PartUnion(M2,Mn) & Ball(c,3/2) c= M2} by A108,A128,TARSKI:def 4;
consider c2 be Element of PM such that
A132: k2 = Ball(c2,1/2) and
A133: c2 in M2\PartUnion(M2,Mn) and
A134: Ball(c2,3/2) c= M2 by A131;
dist(x9,c2) <= dist(x9,w2) + dist(w2,c2) & dist(c1,x9) <=
dist(c1,w1) + dist (w1,x9) by METRIC_1:4;
then
A135: dist(c1,x9) + dist(x9,c2) <= (dist(c1,w1) + dist(w1,x9)) + (
dist(x9,w2) + dist(w2,c2)) by XREAL_1:7;
dist(c1,c2) <= dist(c1,x9) + dist(x9,c2) by METRIC_1:4;
then dist(c1,c2) <= dist(c1,w1) + (dist(w1,x9) + (dist(x9,w2) +
dist(w2,c2))) by A135,XXREAL_0:2;
then dist(c1,c2) - (dist(w1,x9) + (dist(x9,w2) + dist(w2,c2))) <=
dist(c1,w1) by XREAL_1:20;
then dist(c1,c2) - (dist(w1,x9) + (dist(x9,w2) + dist(w2,c2))) <
1/2 by A127,XXREAL_0:2;
then dist(c1,c2) < 1/2 + (dist(w1,x9) + (dist(x9,w2) + dist(w2,c2
))) by XREAL_1:19;
then dist(c1,c2) < dist(w1,x9) + (1/2 + (dist(x9,w2) + dist(w2,c2
)));
then
A136: dist(c1,c2) - (1/2 + (dist(x9,w2) + dist(w2,c2))) < dist(w1,
x9) by XREAL_1:19;
dist(x9,w1) < 1/(2 |^ (m+1+k+1)) by A72,A111,METRIC_1:11;
then dist(c1,c2) - (1/2 + (dist(x9,w2) + dist(w2,c2))) < 1/(2 |^
(m+1+k+1)) by A136,XXREAL_0:2;
then dist(c1,c2) < 1/(2 |^ (m+1+k+1)) + (1/2 + (dist(x9,w2) +
dist(w2,c2))) by XREAL_1:19;
then dist(c1,c2) < dist(x9,w2) + (dist(w2,c2) + (1/(2 |^ (m+1+k+1
)) + 1/2));
then dist(c1,c2) - (dist(w2,c2) + (1/(2 |^ (m+1+k+1)) + 1/2)) <
dist(x9,w2) by XREAL_1:19;
then dist(c1,c2) - (dist(w2,c2) + (1/(2 |^ (m+1+k+1)) + 1/2)) < 1
/(2 |^ (m+1+k+1)) by A119,XXREAL_0:2;
then dist(c1,c2) < 1/(2 |^ (m+1+k+1)) + (dist(w2,c2) + (1/(2 |^ (
m+1+k+1)) + 1/2)) by XREAL_1:19;
then dist(c1,c2) < dist(w2,c2) + (1/(2 |^ (m+1+k+1)) + (1/(2 |^ (
m+1+k+1)) + 1/2));
then
A137: dist(c1,c2) - (1/(2 |^ (m+1+k+1)) + (1/(2 |^ (m+1+k+1)) + 1/
2)) < dist(w2,c2) by XREAL_1:19;
dist(c2,w2) < 1/2 by A130,A132,METRIC_1:11;
then dist(c1,c2) - (1/(2 |^ (m+1+k+1)) + (1/(2 |^ (m+1+k+1)) + 1/
2)) < 1/2 by A137,XXREAL_0:2;
then dist(c1,c2) < 1/2 + (1/(2 |^ (m+1+k+1)) + (1/(2 |^ (m+1+k+1)
) + 1/2)) by XREAL_1:19;
then
A138: dist(c1,c2) < 3/2 by A117,XXREAL_0:2;
then
A139: c1 in Ball(c2,3/2) by METRIC_1:11;
A140: M1 <> M2 by A106,A120,A128;
A141: c2 in Ball(c1,3/2) by A138,METRIC_1:11;
now
per cases by A121,A129,A118,A140;
suppose
[M1,M2] in Mn;
then M1 in Mn-Seg(M2) by A140,WELLORD1:1;
then c2 in PartUnion(M2,Mn) by A126,A141,TARSKI:def 4;
hence contradiction by A133,XBOOLE_0:def 5;
end;
suppose
[M2,M1] in Mn;
then M2 in Mn-Seg(M1) by A140,WELLORD1:1;
then c1 in PartUnion(M1,Mn) by A134,A139,TARSKI:def 4;
hence contradiction by A125,XBOOLE_0:def 5;
end;
end;
hence contradiction;
end;
suppose
n1>0;
then consider l be Nat such that
A142: n1 = l+1 by NAT_1:6;
reconsider l as Element of NAT by ORDINAL1:def 12;
A143: x1 in {union {Ball(c,1/(2 |^ (l+1))) where c is Element of
PM: c
in M1\PartUnion(M1,Mn) & Ball(c,3/(2 |^ (l+1))) c= M1 & not c in union {
union(f.q) where q is Nat: q <= l}} where M1 is Subset of PM: M1 in
FX} by A12,A110,A142;
A144: dist(x9,w2) < 1/(2 |^ (m+1+k+1)) by A72,A107,METRIC_1:11;
A145: x2 in {union {Ball(c,1/(2 |^ (l+1))) where c is Element of
PM: c
in M2\PartUnion(M2,Mn) & Ball(c,3/(2 |^ (l+1))) c= M2 & not c in union {
union(f.q) where q is Nat: q <= l}} where M2 is Subset of PM: M2 in
FX} by A12,A105,A109,A113,A142;
A146: (1/(2 |^ (l+1)) + 1/(2 |^ (m+1+k+1))) + (1/(2 |^ (m+1+k+1))
+ 1/(2 |^ (l+1))) = (1/(2 |^ (l+1)) + 1/(2 |^ (l+1))) + (1/(2 |^ (m+1+k+1)) + 1
/(2 |^ (m+1+k+1)))
.= (1+1)/(2 |^ (l+1)) + (1/(2 |^ (m+1+k+1)) + 1/(2 |^ (m+1+k+1
))) by XCMPLX_1:62
.= 2/(2 |^ (l+1)) + 2/(2 |^ (m+1+k+1)) by XCMPLX_1:62;
n1 in rng g by A103,A109,FUNCT_1:def 3;
then n1 in {i: i<m+1+k+1} by A77;
then
A147: ex i st n1=i & i < m+1+k+1;
then consider h be Nat such that
A148: m+1+k+1 = (l+1) + h by A142,NAT_1:10;
h <> 0 by A142,A147,A148;
then consider i be Nat such that
A149: h = i + 1 by NAT_1:6;
(l+1)+i >= l+1 by NAT_1:11;
then 2 |^ (l+1) > 0 & 2 |^ ((l+1)+i) >= 2 |^ (l+1) by PREPOWER:6,93
;
then
A150: 1/(2 |^ ((l+1)+i)) <= 1/(2 |^ (l+1)) by XREAL_1:118;
2/(2 |^ (m+1+k+1)) = (1*2)/(2 |^ ((l+1)+i)*2) by A148,A149,NEWTON:6
.= 1/(2 |^ ((l+1)+i)) by XCMPLX_1:91;
then (1/(2 |^ (l+1)) + 1/(2 |^ (m+1+k+1))) + (1/(2 |^ (m+1+k+1))
+ 1/(2 |^ (l+1))) - 2/(2 |^ (l+1)) = 1/(2 |^ ((l+1)+i)) by A146;
then (1/(2 |^ (l+1)) + 1/(2 |^ (m+1+k+1))) + (1/(2 |^ (m+1+k+1))
+ 1/(2 |^ (l+1))) <= 2/(2 |^ (l+1)) + 1/(2 |^ (l+1)) by A150,XREAL_1:20;
then
A151: (1/(2 |^ (l+1)) + 1/(2 |^ (m+1+k+1))) + (1/(2 |^ (m+1+k+1))
+ 1/(2 |^ (l+1))) <= (2+1)/(2 |^ (l+1)) by XCMPLX_1:62;
A152: Mn is_connected_in FX by A21;
consider M1 be Subset of PM such that
A153: x1 = union {Ball(c,1/(2 |^ (l+1))) where c is Element of
PM: c
in M1\PartUnion(M1,Mn) & Ball(c,3/(2 |^ (l+1))) c= M1 & not c in union {
union(f.q) where q is Nat: q <= l}} and
A154: M1 in FX by A143;
reconsider NF = {Ball(c,1/(2 |^ (l+1))) where c is Element of PM:
c in M1\PartUnion(M1,Mn) & Ball(c,3/(2 |^ (l+1))) c= M1 & not c in union {
union(f.q) where q is Nat: q <= l}} as set;
consider k1 be set such that
A155: w1 in k1 and
A156: k1 in NF by A112,A153,TARSKI:def 4;
consider c1 be Element of PM such that
A157: k1 = Ball(c1,1/(2 |^ (l+1))) and
A158: c1 in M1\PartUnion(M1,Mn) and
A159: Ball(c1,3/(2 |^ (l+1))) c= M1 and
not c1 in union { union(f.q) where q is Nat: q <= l
} by A156;
A160: dist(c1,w1) < 1/(2 |^ (l+1)) by A155,A157,METRIC_1:11;
consider M2 be Subset of PM such that
A161: x2 = union {Ball(c,1/(2 |^ (l+1))) where c is Element of
PM: c
in M2\PartUnion(M2,Mn) & Ball(c,3/(2 |^ (l+1))) c= M2 & not c in union {
union(f.q) where q is Nat: q <= l}} and
A162: M2 in FX by A145;
A163: M1 <> M2 by A106,A153,A161;
reconsider NF = {Ball(c,1/(2 |^ (l+1))) where c is Element of PM:
c in M2\PartUnion(M2,Mn) & Ball(c,3/(2 |^ (l+1))) c= M2 & not c in union {
union(f.q) where q is Nat: q <= l}} as set;
consider k2 be set such that
A164: w2 in k2 and
A165: k2 in NF by A108,A161,TARSKI:def 4;
consider c2 be Element of PM such that
A166: k2 = Ball(c2,1/(2 |^ (l+1))) and
A167: c2 in M2\PartUnion(M2,Mn) and
A168: Ball(c2,3/(2 |^ (l+1))) c= M2 and
not c2 in union { union(f.q) where q is Nat: q <= l
} by A165;
dist(x9,c2) <= dist(x9,w2) + dist(w2,c2) & dist(c1,x9) <=
dist(c1,w1) + dist (w1,x9) by METRIC_1:4;
then
A169: dist(c1,x9) + dist(x9,c2) <= (dist(c1,w1) + dist(w1,x9)) + (
dist(x9,w2) + dist(w2,c2)) by XREAL_1:7;
dist(c1,c2) <= dist(c1,x9) + dist(x9,c2) by METRIC_1:4;
then dist(c1,c2) <= dist(c1,w1) + (dist(w1,x9) + (dist(x9,w2) +
dist(w2,c2))) by A169,XXREAL_0:2;
then dist(c1,c2) - (dist(w1,x9) + (dist(x9,w2) + dist(w2,c2))) <=
dist(c1,w1) by XREAL_1:20;
then dist(c1,c2) - (dist(w1,x9) + (dist(x9,w2) + dist(w2,c2))) <
1/(2 |^ (l+1)) by A160,XXREAL_0:2;
then dist(c1,c2) < 1/(2 |^ (l+1)) + (dist(w1,x9) + (dist(x9,w2) +
dist(w2,c2))) by XREAL_1:19;
then dist(c1,c2) < dist(w1,x9) + (1/(2 |^ (l+1)) + (dist(x9,w2) +
dist(w2,c2)));
then
A170: dist(c1,c2) - (1/(2 |^ (l+1)) + (dist(x9,w2) + dist(w2,c2)))
< dist(w1,x9) by XREAL_1:19;
dist(x9,w1) < 1/(2 |^ (m+1+k+1)) by A72,A111,METRIC_1:11;
then dist(c1,c2) - (1/(2 |^ (l+1)) + (dist(x9,w2) + dist(w2,c2)))
< 1/(2 |^ (m+1+k+1)) by A170,XXREAL_0:2;
then dist(c1,c2) < 1/(2 |^ (m+1+k+1)) + (1/(2 |^ (l+1)) + (dist(
x9,w2) + dist(w2,c2))) by XREAL_1:19;
then dist(c1,c2) < dist(x9,w2) + (dist(w2,c2) + (1/(2 |^ (m+1+k+1
)) + 1/(2 |^ (l+1))));
then dist(c1,c2) - (dist(w2,c2) + (1/(2 |^ (m+1+k+1)) + 1/(2 |^ (
l+1)))) < dist(x9,w2) by XREAL_1:19;
then dist(c1,c2) - (dist(w2,c2) + (1/(2 |^ (m+1+k+1)) + 1/(2 |^ (
l+1)))) < 1/(2 |^ (m+1+k+1)) by A144,XXREAL_0:2;
then dist(c1,c2) < 1/(2 |^ (m+1+k+1)) + (dist(w2,c2) + (1/(2 |^ (
m+1+k+1)) + 1/(2 |^ (l+1)))) by XREAL_1:19;
then dist(c1,c2) < dist(w2,c2) + (1/(2 |^ (m+1+k+1)) + (1/(2 |^ (
m+1+k+1)) + 1/(2 |^ (l+1))));
then
A171: dist(c1,c2) - (1/(2 |^ (m+1+k+1)) + (1/(2 |^ (m+1+k+1)) + 1/
(2 |^ (l+1)))) < dist(w2,c2) by XREAL_1:19;
dist(c2,w2) < 1/(2 |^ (l+1)) by A164,A166,METRIC_1:11;
then dist(c1,c2) - (1/(2 |^ (m+1+k+1)) + (1/(2 |^ (m+1+k+1)) + 1/
(2 |^ (l+1)))) < 1/(2 |^ (l+1)) by A171,XXREAL_0:2;
then dist(c1,c2) < 1/(2 |^ (l+1)) + (1/(2 |^ (m+1+k+1)) + (1/(2
|^ (m+1+k+1)) + 1/(2 |^ (l+1)))) by XREAL_1:19;
then
A172: dist(c1,c2) < 3/(2 |^ (l+1)) by A151,XXREAL_0:2;
then
A173: c1 in Ball(c2,3/(2 |^ (l+1))) by METRIC_1:11;
A174: c2 in Ball(c1,3/(2 |^ (l+1))) by A172,METRIC_1:11;
now
per cases by A154,A162,A152,A163;
suppose
[M1,M2] in Mn;
then M1 in Mn-Seg(M2) by A163,WELLORD1:1;
then c2 in PartUnion(M2,Mn) by A159,A174,TARSKI:def 4;
hence contradiction by A167,XBOOLE_0:def 5;
end;
suppose
[M2,M1] in Mn;
then M2 in Mn-Seg(M1) by A163,WELLORD1:1;
then c1 in PartUnion(M1,Mn) by A168,A173,TARSKI:def 4;
hence contradiction by A158,XBOOLE_0:def 5;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
then g is one-to-one by FUNCT_1:def 4;
then
A175: NZ,rng g are_equipotent by A75,WELLORD2:def 4;
{i: i < m+1+k+1 } is finite
proof
{i: i < m+1+k+1 } c= {0} \/ Seg(m+1+k+1)
proof
let x be object;
assume x in {i: i < m+1+k+1};
then
A176: ex i be Nat st x = i & i < (m+1+k+1);
then reconsider x1=x as Nat;
now
per cases;
suppose
x1 = 0;
hence x1 in {0} or x1 in Seg(m+1+k+1) by TARSKI:def 1;
end;
suppose
x1 > 0;
then ex l be Nat st x1 = l +1 by NAT_1:6;
then x1 >= 1 by NAT_1:11;
hence x1 in {0} or x1 in Seg(m+1+k+1) by A176,FINSEQ_1:1;
end;
end;
hence thesis by XBOOLE_0:def 3;
end;
hence thesis;
end;
hence thesis by A77,A175,CARD_1:38;
end;
2 |^ (m+1+k+1) > 0 by PREPOWER:6;
then
A177: 1/(2 |^ (m+1+k+1)) > 0 by XREAL_1:139;
W in the topology of PT by A2,A7,A72,PCOMPS_1:29;
then W is open by PRE_TOPC:def 2;
hence thesis by A177,A72,A73,TBSP_1:11;
end;
hence GX is locally_finite by PCOMPS_1:def 1;
end;
theorem :: Stone Theorem
PT is metrizable implies PT is paracompact
proof
assume PT is metrizable;
then
for FX being Subset-Family of PT st FX is Cover of PT & FX is open ex GX
being Subset-Family of PT st GX is open & GX is Cover of PT & GX is_finer_than
FX & GX is locally_finite by Th6;
hence thesis by PCOMPS_1:def 3;
end;