:: Paracompact and Metrizable Spaces :: by Leszek Borys :: :: Received June 8, 1991 :: Copyright (c) 1991-2021 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, METRIC_1, SUBSET_1, REAL_1, XXREAL_0, TARSKI, ARYTM_3, XBOOLE_0, PRE_TOPC, SETFAM_1, ZFMISC_1, COMPTS_1, STRUCT_0, RCOMP_1, FINSET_1, FINSEQ_1, RELAT_1, NAT_1, CARD_1, FUNCT_1, CARD_5, ARYTM_1, PCOMPS_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, TOPS_2, SETFAM_1, DOMAIN_1, STRUCT_0, FINSET_1, COMPTS_1, PRE_TOPC, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, FINSEQ_1, NAT_1, METRIC_1; constructors SETFAM_1, DOMAIN_1, REAL_1, SQUARE_1, NAT_1, MEMBERED, FINSEQ_1, TOPS_2, COMPTS_1, METRIC_1, RELSET_1, BINOP_1, BINOP_2, VALUED_0; registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, STRUCT_0, TOPS_1, COMPTS_1, METRIC_1, FINSEQ_1, PRE_TOPC, RELAT_1, ORDINAL1, BINOP_2, VALUED_0; 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 for r, p being Real st r <= p holds 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 <> {}; reserve T for non empty TopSpace; reserve x 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:3 FX is Cover of T implies for x ex W st x in W & W in FX; reserve a for set; theorem :: PCOMPS_1:4 the topology of 1TopSp a = bool a; theorem :: PCOMPS_1:5 the carrier of 1TopSp a = a; theorem :: PCOMPS_1:6 1TopSp {a} is compact; theorem :: PCOMPS_1:7 T is T_2 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 1 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:8 for W holds { V : V in FX & V meets W} c= FX; theorem :: PCOMPS_1:9 FX c= GX & GX is locally_finite implies FX is locally_finite; theorem :: PCOMPS_1:10 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 2 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:11 for T being TopSpace, FX being Subset-Family of T holds clf FX is closed; theorem :: PCOMPS_1:12 for T being TopSpace, FX being Subset-Family of T st FX = {} holds clf FX = {}; theorem :: PCOMPS_1:13 FX = { V } implies clf FX = { Cl V }; theorem :: PCOMPS_1:14 FX c= GX implies clf FX c= clf GX; theorem :: PCOMPS_1:15 clf(FX \/ GX) = (clf FX) \/ (clf GX); theorem :: PCOMPS_1:16 FX is finite implies Cl(union FX) = union (clf FX); theorem :: PCOMPS_1:17 FX is_finer_than clf FX; scheme :: PCOMPS_1:sch 1 Lambda1top{T()->TopSpace, X()->Subset-Family of T(), Y()->Subset-Family of T (), F(object)->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:18 FX is locally_finite implies clf FX is locally_finite; theorem :: PCOMPS_1:19 union FX c= union(clf FX); theorem :: PCOMPS_1:20 FX is locally_finite implies Cl union FX = union clf FX; theorem :: PCOMPS_1:21 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 3 for FX being Subset-Family of IT st FX is Cover of IT & FX is open ex GX being Subset-Family of IT st GX is open & GX is Cover of IT & GX is_finer_than FX & GX is locally_finite; end; registration cluster paracompact for non empty TopSpace; end; theorem :: PCOMPS_1:22 T is compact implies T is paracompact; theorem :: PCOMPS_1:23 T is paracompact & B is closed & (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:24 T is T_2 & T is paracompact implies T is regular; theorem :: PCOMPS_1:25 T is T_2 & T is paracompact implies T is normal; :: Topological space of metric space reserve x,y,z for Element of PM; reserve V,W,Y for Subset of PM; definition let PM; func Family_open_set(PM) -> Subset-Family of PM means :: PCOMPS_1:def 4 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:26 for x ex r st r>0 & Ball(x,r) c= the carrier of PM; theorem :: PCOMPS_1:27 for r being Real 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:28 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); theorem :: PCOMPS_1:29 for r being Real st PM is triangle holds Ball(x,r) in Family_open_set(PM); theorem :: PCOMPS_1:30 the carrier of PM in Family_open_set(PM); theorem :: PCOMPS_1:31 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:32 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:33 TopStruct (#the carrier of PM,Family_open_set(PM)#) is TopSpace; definition let PM; func TopSpaceMetr PM -> TopStruct equals :: PCOMPS_1:def 5 TopStruct (#the carrier of PM, Family_open_set(PM)#); end; registration let PM; cluster TopSpaceMetr PM -> strict TopSpace-like; end; registration let PM be non empty MetrStruct; cluster TopSpaceMetr PM -> non empty; end; theorem :: PCOMPS_1:34 for PM being non empty MetrSpace holds TopSpaceMetr PM is T_2; registration cluster T_2 non empty strict for TopSpace; end; :: 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 6 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:35 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 set, f be Function of [:D,D:],REAL; assume f is_metric_of D; func SpaceMetr(D,f) -> strict MetrSpace equals :: PCOMPS_1:def 7 MetrStruct(#D,f#); end; :: Metrizable topological spaces definition let IT be TopStruct; attr IT is metrizable means :: PCOMPS_1:def 8 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; registration cluster strict metrizable for non empty TopSpace; end; theorem :: PCOMPS_1:36 for D be non empty set, f be Function of [:D,D:],REAL st f is_metric_of D holds SpaceMetr(D,f) is non empty;