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


begin

begin

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) )
proofend;

scheme :: PCOMPS_2:sch 1
MinSet{ F1() ->  set , F2() ->  Relation, P1[ set ] } :
 ex X being set st
( X in F1() & P1[X] & ( for Y being set st Y in F1() & P1[Y] holds
[X,Y] in F2() ) )
provided
A1: F2() well_orders F1() and
A2: ex X being set st
( X in F1() & P1[X] )
proofend;

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
 union (R -Seg B) is set ;
end;

:: deftheorem  defines PartUnion PCOMPS_2:def_1_:_
 for FX being set
for R being Relation
for B being Element of FX holds PartUnion (B,R) = union (R -Seg B);

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
 ex b1 being set st
for A being set holds
( A in b1 iff ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) )
proofend;
uniqueness
 for b1, b2 being set st ( for A being set holds
( A in b1 iff ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) ) ) & ( for A being set holds
( A in b2 iff ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines DisjointFam PCOMPS_2:def_2_:_
 for FX being set
for R being Relation
for b3 being set holds
( b3 = DisjointFam (FX,R) iff for A being set holds
( A in b3 iff ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) ) );

definition
let X be set ;
let n be Element of NAT ;
let f be Function of NAT,(bool X);
func PartUnionNat (n,f) ->  set  equals :: PCOMPS_2:def 3
 union (f .: ((Seg n) \ {n}));
coherence
 union (f .: ((Seg n) \ {n})) is set ;
end;

:: deftheorem  defines PartUnionNat PCOMPS_2:def_3_:_
 for X being set
for n being Element of NAT
for f being Function of NAT,(bool X) holds PartUnionNat (n,f) = union (f .: ((Seg n) \ {n}));

begin

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 ) ) )
proofend;

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 )
proofend;

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
proofend;

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;

definition
let PM be non empty set ;
let g be Function of NAT,((bool (bool PM)) *);
let n be Element of NAT ;
:: original:.
redefine funcg . n ->  FinSequence of bool (bool PM);
coherence
 g . n is FinSequence of bool (bool PM)
proofend;
end;

scheme :: PCOMPS_2:sch 2
XXX1{ F1() ->  non empty set , F2() ->  Subset-Family of F1(), F3( set , set ) ->  Subset of F1(), P1[ set ], P2[ set , set , set , set ] } :
 ex f being Function of NAT,(bool (bool F1())) st
( f . 0 = F2() & ( for n being Element of NAT holds f . (n + 1) =  {  (union  {  F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n &amp; fq = f . q holds
P2[c,V,n,fq]  }  ) where V is Subset of F1() : P1[V]  }  ) )
proofend;

scheme :: PCOMPS_2:sch 3
XXX{ F1() ->  non empty set , F2() ->  Subset-Family of F1(), F3( set , set ) ->  Subset of F1(), P1[ set ], P2[ set , set , set ] } :
 ex f being Function of NAT,(bool (bool F1())) st
( f . 0 = F2() &amp; ( for n being Element of NAT holds f . (n + 1) =  {  (union  {  F3(c,n) where c is Element of F1() : ( P2[c,V,n] &amp; not c in union  {  (union (f . q)) where q is Element of NAT : q <= n  }  )  }  ) where V is Subset of F1() : P1[V]  }  ) )
proofend;

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 &amp; FX is open holds
ex GX being Subset-Family of PT st
( GX is open &amp; GX is Cover of PT &amp; GX is_finer_than FX &amp; GX is locally_finite )
proofend;

theorem :: PCOMPS_2:7
for PT being non empty TopSpace st PT is metrizable holds
PT is paracompact
proofend;