Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

### The abstract of the Mizar article:

### On Paracompactness of Metrizable Spaces

**by****Leszek Borys**- Received July 23, 1992
- 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;

Back to top