:: On Paracompactness of Metrizable Spaces
:: by Leszek Borys
::
:: Received July 23, 1992
:: Copyright (c) 1992-2016 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;
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 :: PCOMPS_2:1
R well_orders A implies R |_2 A well_orders A & A = field (R |_2 A);
scheme :: PCOMPS_2:sch 1
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
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) -> set equals
:: PCOMPS_2:def 1
union (R-Seg(B));
end;
definition
let FX be set, R be Relation;
func DisjointFam(FX,R) -> set 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 Element of NAT, f be sequence of bool X;
func PartUnionNat(n,f) -> set 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:2
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;
theorem :: PCOMPS_2:3
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;
theorem :: PCOMPS_2:4
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;
theorem :: PCOMPS_2:5
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;
scheme :: PCOMPS_2:sch 2
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]};
scheme :: PCOMPS_2:sch 3
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]};
theorem :: PCOMPS_2:6
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;
theorem :: PCOMPS_2:7 :: Stone Theorem
PT is metrizable implies PT is paracompact;