PCOMPS_2: On Paracompactness of Metrizable Spaces

:: On Paracompactness of Metrizable Spaces
:: by Leszek Borys
::
:: Received July 23, 1992
:: Copyright (c) 1992-2016 Association of Mizar Users

environ

vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, WELLORD1, RELAT_2, SETFAM_1;
theorems PCOMPS_1, COMPTS_1, SETFAM_1, TOPS_1, TOPS_2, PRE_TOPC, SUBSET_1, TARSKI, WELLORD2, ZFMISC_1, NAT_1, PREPOWER, WELLORD1, RELAT_1, FUNCT_1, METRIC_1, FINSEQ_1, CARD_1, FINSEQ_2, FINSEQ_4, TBSP_1, NEWTON, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1;
schemes NAT_1, FUNCT_2, SUBSET_1, RECDEF_1, TREES_2, FRAENKEL, XBOOLE_0, XFAMILY;
registrations SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NAT_1, FINSEQ_1, STRUCT_0, PRE_TOPC, METRIC_1, TOPS_1, XREAL_0, NEWTON;
constructors HIDDEN, SETFAM_1, RELAT_2, WELLORD1, WELLORD2, REAL_1, NAT_1, MEMBERED, NEWTON, TOPS_2, PCOMPS_1, FINSEQ_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities WELLORD1, XBOOLE_0, STRUCT_0;
expansions TARSKI, WELLORD1, RELAT_2, SETFAM_1, XBOOLE_0;

theorem Th1: :: PCOMPS_2:1

for R being Relation
for A being set st R well_orders A holds
( R |_2 A well_orders A & A = field (R |_2 A) )

proof end;

scheme :: PCOMPS_2:sch 1
MinSet{ F₁() -> set , F₂() -> Relation, P₁[ object ] } :

ex X being set st
( X in F₁() & P₁[X] & ( for Y being set st Y in F₁() & P₁[Y] holds
[X,Y] in F₂() ) )

provided

A1: F₂() well_orders F₁() and
A2: ex X being set st
( X in F₁() & P₁[X] )

proof end;

definition

let FX be set ;
let R be Relation;
let B be Element of FX;

func PartUnion (B,R) -> set equals :: PCOMPS_2:def 1
union (R -Seg B);

coherence ;

end;

:: deftheorem defines PartUnion PCOMPS_2:def 1 :

definition

let FX be set ;
let R be Relation;

func DisjointFam (FX,R) -> set means :: PCOMPS_2:def 2
for A being set holds
( A in it iff ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines DisjointFam PCOMPS_2:def 2 :

definition

let X be set ;
let n be Element of NAT ;
let f be sequence of (bool X);

func PartUnionNat (n,f) -> set equals :: PCOMPS_2:def 3
union (f .: ((Seg n) \ {n}));

coherence ;

end;

:: deftheorem defines PartUnionNat PCOMPS_2:def 3 :

theorem Th2: :: PCOMPS_2:2

for PT being non empty TopSpace st PT is regular holds
for FX being Subset-Family of PT st FX is Cover of PT & FX is open holds
ex HX being Subset-Family of PT st
( HX is open & HX is Cover of PT & ( for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) ) )

proof end;

theorem :: PCOMPS_2:3

for PT being non empty TopSpace
for FX being Subset-Family of PT st PT is T_2 & PT is paracompact & FX is Cover of PT & FX is open holds
ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & clf GX is_finer_than FX & GX is locally_finite )

proof end;

theorem Th4: :: PCOMPS_2:4

for PT being non empty TopSpace
for PM being MetrSpace
for f being Function of [: the carrier of PT, the carrier of PT:],REAL st f is_metric_of the carrier of PT & PM = SpaceMetr ( the carrier of PT,f) holds
the carrier of PM = the carrier of PT

proof end;

theorem :: PCOMPS_2:5

for PT being non empty TopSpace
for PM being MetrSpace
for FX being Subset-Family of PT
for f being Function of [: the carrier of PT, the carrier of PT:],REAL st f is_metric_of the carrier of PT & PM = SpaceMetr ( the carrier of PT,f) holds
( FX is Subset-Family of PT iff FX is Subset-Family of PM ) by Th4;

scheme :: PCOMPS_2:sch 2
XXX1{ F₁() -> non empty set , F₂() -> Subset-Family of F₁(), F₃( object , object ) -> Subset of F₁(), P₁[ object ], P₂[ object , object , object , object ] } :

ex f being sequence of (bool (bool F₁())) st
( f . 0 = F₂() & ( for n being Nat holds f . (n + 1) = { (union { F₃(c,n) where c is Element of F₁() : for fq being Subset-Family of F₁()
for q being Nat st q <= n & fq = f . q holds
P₂[c,V,n,fq] } ) where V is Subset of F₁() : P₁[V] } ) )

proof end;

reconsider jd = 1 / 2 as Real ;

scheme :: PCOMPS_2:sch 3
XXX{ F₁() -> non empty set , F₂() -> Subset-Family of F₁(), F₃( object , object ) -> Subset of F₁(), P₁[ object ], P₂[ object , object , object ] } :

ex f being sequence of (bool (bool F₁())) st
( f . 0 = F₂() & ( for n being Nat holds f . (n + 1) = { (union { F₃(c,n) where c is Element of F₁() : ( P₂[c,V,n] & not c in union { (union (f . q)) where q is Nat : q <= n } ) } ) where V is Subset of F₁() : P₁[V] } ) )

proof end;

theorem Th6: :: PCOMPS_2:6

for PT being non empty TopSpace st PT is metrizable holds
for FX being Subset-Family of PT st FX is Cover of PT & FX is open holds
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 )

proof end;

theorem :: PCOMPS_2:7

for PT being non empty TopSpace st PT is metrizable holds
PT is paracompact

proof end;