Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### On Paracompactness of Metrizable Spaces

by
Leszek Borys

MML identifier: PCOMPS_2
[ Mizar article, MML identifier index ]

```environ

vocabulary ARYTM, FUNCT_1, ARYTM_3, RELAT_1, WELLORD1, RELAT_2, BOOLE, TARSKI,
FINSEQ_1, PRE_TOPC, METRIC_1, SETFAM_1, COMPTS_1, SUBSET_1, ARYTM_1,
PCOMPS_1, FINSET_1, PCOMPS_2, GROUP_1, FINSEQ_4;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, REAL_1, TOPS_2, FUNCT_1, FUNCT_2, NAT_1, SETFAM_1, STRUCT_0,
METRIC_1, COMPTS_1, PRE_TOPC, PCOMPS_1, PREPOWER, WELLORD1, RELAT_1,
FINSEQ_1, FINSET_1, RELAT_2, FINSEQ_2, FINSEQ_4;
constructors TOPS_2, NAT_1, COMPTS_1, PCOMPS_1, REAL_1, PREPOWER, WELLORD1,
WELLORD2, RELAT_2, FINSEQ_4, MEMBERED;
clusters SUBSET_1, PRE_TOPC, FINSET_1, RELSET_1, STRUCT_0, XREAL_0, FINSEQ_1,
METRIC_1, NEWTON, MEMBERED, ZFMISC_1, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;

begin :: 1. Selected properties of real numbers

reserve r,u for real number;
reserve n,k,i for Nat;

canceled 2;

theorem :: PCOMPS_2:3
r>0 & u > 0 implies ex k be Nat st u/(2 |^ k) <= r;

theorem :: PCOMPS_2:4
k>=n & r >= 1 implies r |^ k >= r |^ n;

begin :: 2. Certain functions defined on families of sets

reserve R for Relation;
reserve A for set;

theorem :: PCOMPS_2:5
R well_orders A implies R |_2 A well_orders A & A = field (R |_2 A);

scheme MinSet{A()->set,R()->Relation,P[set]}:
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
R() well_orders A() and
ex X be set st X in A() & P[X];

definition let FX be set, R be Relation,
B be Element of FX;
func PartUnion(B,R) equals
:: PCOMPS_2:def 1
union (R-Seg(B));
end;

definition let FX be set, R be Relation;
func DisjointFam(FX,R) means
:: PCOMPS_2:def 2
A in it iff ex B be Element of FX st B in FX & A = B\PartUnion(B,R);
end;

definition let X be set, n be Nat, f be Function of NAT,bool X;
func PartUnionNat(n,f) equals
:: PCOMPS_2:def 3
union (f.:(Seg(n)\{n}));
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 :: PCOMPS_2:6
PT is_T3 implies
for FX st FX is_a_cover_of PT & FX is open
ex HX st HX is open & HX is_a_cover_of PT &
for V st V in HX ex W st W in FX & Cl V c= W;

theorem :: PCOMPS_2:7
for PT,FX st PT is_T2 & PT is paracompact &
FX is_a_cover_of PT & FX is open
ex GX st GX is open & GX is_a_cover_of PT &
clf GX is_finer_than FX & GX is locally_finite;

theorem :: PCOMPS_2:8
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;

canceled 2;

theorem :: PCOMPS_2:11
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);

reserve Mn for Relation;
reserve n,k,l,q,p,q1 for Nat;

definition let PM be non empty set;
let g be Function of NAT,(bool bool PM)*;
let n;
redefine func g.n -> FinSequence of bool bool PM;
end;

theorem :: PCOMPS_2:12  :: Stone Theorem - general case
PT is metrizable implies
for FX being Subset-Family of PT
st FX is_a_cover_of PT & FX is open
ex GX being Subset-Family of PT
st GX is open & GX is_a_cover_of PT &
GX is_finer_than FX & GX is locally_finite;

theorem :: PCOMPS_2:13  :: Stone Theorem
PT is metrizable implies PT is paracompact;
```