Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### The abstract of the Mizar article:

### Paracompact and Metrizable Spaces

**by****Leszek Borys**- Received June 8, 1991
- MML identifier: PCOMPS_1

- [ Mizar article, MML identifier index ]

environ vocabulary METRIC_1, PRE_TOPC, BOOLE, SETFAM_1, TARSKI, SUBSET_1, COMPTS_1, FINSET_1, FINSEQ_1, RELAT_1, FUNCT_1, ARYTM_1, SQUARE_1, ARYTM_3, PCOMPS_1, ARYTM; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1, TOPS_2, SETFAM_1, STRUCT_0, FINSET_1, COMPTS_1, PRE_TOPC, SQUARE_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, NAT_1, METRIC_1; constructors METRIC_1, REAL_1, TOPS_2, COMPTS_1, SQUARE_1, FINSEQ_1, NAT_1, MEMBERED; clusters SUBSET_1, METRIC_1, PRE_TOPC, FINSET_1, STRUCT_0, METRIC_3, COMPLSP1, XREAL_0, RELSET_1, TOPS_1, ARYTM_3, SETFAM_1, MEMBERED, ZFMISC_1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin reserve PM for MetrStruct; reserve x,y for Element of PM; reserve r,p,q,s,t for Real; theorem :: PCOMPS_1:1 r <= p implies Ball(x,r) c= Ball(x,p); reserve T for TopSpace; reserve A for Subset of T; theorem :: PCOMPS_1:2 Cl(A) <> {} iff A <> {}; theorem :: PCOMPS_1:3 Cl(A) = {} implies A = {}; theorem :: PCOMPS_1:4 Cl(A) is closed; reserve T for non empty TopSpace; reserve x,y for Point of T; reserve Z,X,V,W,Y,Q for Subset of T; reserve FX for Subset-Family of T; theorem :: PCOMPS_1:5 FX is_a_cover_of T implies for x ex W st x in W & W in FX; definition let X be set; redefine func bool X -> non empty Subset-Family of X; end; definition let D be set; func 1TopSp D -> TopStruct equals :: PCOMPS_1:def 1 TopStruct (# D, bool D #); end; definition let D be set; cluster 1TopSp D -> strict TopSpace-like; end; definition let D be non empty set; cluster 1TopSp D -> non empty; end; reserve a for set; canceled; theorem :: PCOMPS_1:7 the topology of 1TopSp a = bool a; theorem :: PCOMPS_1:8 the carrier of 1TopSp a = a; theorem :: PCOMPS_1:9 1TopSp {a} is compact; theorem :: PCOMPS_1:10 T is_T2 implies {x} is closed; :: Paracompact spaces reserve x,y for Point of T; reserve A,B for Subset of T; reserve FX,GX for Subset-Family of T; definition let T be TopStruct; let IT be Subset-Family of T; attr IT is locally_finite means :: PCOMPS_1:def 2 for x being Point of T ex W being Subset of T st x in W & W is open & { V where V is Subset of T: V in IT & V meets W } is finite; end; theorem :: PCOMPS_1:11 for W holds { V : V in FX & V meets W} c= FX; theorem :: PCOMPS_1:12 FX c= GX & GX is locally_finite implies FX is locally_finite; theorem :: PCOMPS_1:13 FX is finite implies FX is locally_finite; definition let T be TopStruct, FX be Subset-Family of T; func clf FX -> Subset-Family of T means :: PCOMPS_1:def 3 for Z being Subset of T holds Z in it iff ex W being Subset of T st Z = Cl W & W in FX; end; theorem :: PCOMPS_1:14 clf FX is closed; theorem :: PCOMPS_1:15 FX = {} implies clf FX = {}; theorem :: PCOMPS_1:16 FX = { V } implies clf FX = { Cl V }; theorem :: PCOMPS_1:17 FX c= GX implies clf FX c= clf GX; theorem :: PCOMPS_1:18 clf(FX \/ GX) = (clf FX) \/ (clf GX); reserve k for Nat; theorem :: PCOMPS_1:19 FX is finite implies Cl(union FX) = union (clf FX); theorem :: PCOMPS_1:20 FX is_finer_than clf FX; scheme Lambda1top{T()->TopSpace, X()->Subset-Family of T(), Y()->Subset-Family of T(), F(set)->Subset of T()}: ex f being Function of X(),Y() st for Z being Subset of T() st Z in X() holds f.Z = F(Z) provided for Z being Subset of T() st Z in X() holds F(Z) in Y(); theorem :: PCOMPS_1:21 FX is locally_finite implies clf FX is locally_finite; theorem :: PCOMPS_1:22 union FX c= union(clf FX); theorem :: PCOMPS_1:23 FX is locally_finite implies Cl union FX = union clf FX; theorem :: PCOMPS_1:24 FX is locally_finite & FX is closed implies union FX is closed; definition let IT be TopStruct; attr IT is paracompact means :: PCOMPS_1:def 4 for FX being Subset-Family of IT st FX is_a_cover_of IT & FX is open ex GX being Subset-Family of IT st GX is open & GX is_a_cover_of IT & GX is_finer_than FX & GX is locally_finite; end; definition cluster paracompact (non empty TopSpace); end; theorem :: PCOMPS_1:25 T is compact implies T is paracompact; theorem :: PCOMPS_1:26 T is paracompact & A is closed & B is closed & A misses B & (for x st x in B ex V,W being Subset of T st V is open & W is open & A c= V & x in W & V misses W) implies ex Y,Z being Subset of T st Y is open & Z is open & A c=Y & B c= Z & Y misses Z; theorem :: PCOMPS_1:27 T is_T2 & T is paracompact implies T is_T3; theorem :: PCOMPS_1:28 T is_T2 & T is paracompact implies T is_T4; :: Topological space of metric space reserve x,y,z for Element of PM; reserve V,W,Y for Subset of PM; scheme SubFamExM {A() -> MetrStruct, P[Subset of A()]}: ex F being Subset-Family of A() st for B being Subset of A() holds B in F iff P[B]; definition let PM; func Family_open_set(PM) -> Subset-Family of PM means :: PCOMPS_1:def 5 for V holds V in it iff for x st x in V holds ex r st r>0 & Ball(x,r) c= V; end; theorem :: PCOMPS_1:29 for x ex r st r>0 & Ball(x,r) c= the carrier of PM; theorem :: PCOMPS_1:30 for r being real number st PM is triangle & y in Ball(x,r) holds ex p st p>0 & Ball(y,p) c= Ball(x,r); theorem :: PCOMPS_1:31 PM is triangle & y in Ball(x,r) /\ Ball(z,p) implies ex q st Ball(y,q) c= Ball(x,r) & Ball(y,q) c= Ball(z,p); canceled; theorem :: PCOMPS_1:33 for r being real number st PM is triangle holds Ball(x,r) in Family_open_set(PM); theorem :: PCOMPS_1:34 the carrier of PM in Family_open_set(PM); theorem :: PCOMPS_1:35 for V,W st V in Family_open_set(PM) & W in Family_open_set(PM) holds V /\ W in Family_open_set(PM); theorem :: PCOMPS_1:36 for A being Subset-Family of PM st A c= Family_open_set(PM) holds union A in Family_open_set(PM); theorem :: PCOMPS_1:37 TopStruct (#the carrier of PM,Family_open_set(PM)#) is TopSpace; definition let PM; func TopSpaceMetr PM -> TopStruct equals :: PCOMPS_1:def 6 TopStruct (#the carrier of PM,Family_open_set(PM)#); end; definition let PM; cluster TopSpaceMetr PM -> strict TopSpace-like; end; definition let PM be non empty MetrStruct; cluster TopSpaceMetr PM -> non empty; end; theorem :: PCOMPS_1:38 for PM being non empty MetrSpace holds TopSpaceMetr PM is_T2; :: Metric on a set definition let D be set,f be Function of [:D,D:],REAL; pred f is_metric_of D means :: PCOMPS_1:def 7 for a,b,c be Element of D holds (f.(a,b) = 0 iff a=b) & f.(a,b) = f.(b,a) & f.(a,c)<=f.(a,b)+f.(b,c); end; theorem :: PCOMPS_1:39 for D being set,f being Function of [:D,D:],REAL holds f is_metric_of D iff MetrStruct (#D,f#) is MetrSpace; definition let D be non empty set, f be Function of [:D,D:],REAL; assume f is_metric_of D; func SpaceMetr(D,f) -> strict non empty MetrSpace equals :: PCOMPS_1:def 8 MetrStruct(#D,f#); end; :: Metrizable topological spaces definition let IT be non empty TopStruct; attr IT is metrizable means :: PCOMPS_1:def 9 ex f being Function of [:the carrier of IT,the carrier of IT:],REAL st f is_metric_of (the carrier of IT) & Family_open_set( SpaceMetr (the carrier of IT,f) ) = the topology of IT; end; definition cluster strict metrizable (non empty TopSpace); end;

Back to top