The abstract of the Mizar article:

On Paracompactness of Metrizable Spaces

by

Leszek Borys

Received July 23, 1992

MML identifier: PCOMPS_2

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, FUNCT_1, ARYTM_3, RELAT_1, WELLORD1, RELAT_2, BOOLE, TARSKI,
      FINSEQ_1, PRE_TOPC, METRIC_1, SETFAM_1, COMPTS_1, SUBSET_1, ARYTM_1,
      PCOMPS_1, FINSET_1, PCOMPS_2, GROUP_1, FINSEQ_4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XREAL_0, REAL_1, TOPS_2, FUNCT_1, FUNCT_2, NAT_1, SETFAM_1, STRUCT_0,
      METRIC_1, COMPTS_1, PRE_TOPC, PCOMPS_1, PREPOWER, WELLORD1, RELAT_1,
      FINSEQ_1, FINSET_1, RELAT_2, FINSEQ_2, FINSEQ_4;
 constructors TOPS_2, NAT_1, COMPTS_1, PCOMPS_1, REAL_1, PREPOWER, WELLORD1,
      WELLORD2, RELAT_2, FINSEQ_4, MEMBERED;
 clusters SUBSET_1, PRE_TOPC, FINSET_1, RELSET_1, STRUCT_0, XREAL_0, FINSEQ_1,
      METRIC_1, NEWTON, MEMBERED, ZFMISC_1, ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: 1. Selected properties of real numbers

  reserve r,u for real number;
  reserve n,k,i for Nat;

canceled 2;

  theorem :: PCOMPS_2:3
   r>0 & u > 0 implies ex k be Nat st u/(2 |^ k) <= r;

theorem :: PCOMPS_2:4
    k>=n & r >= 1 implies r |^ k >= r |^ n;

begin :: 2. Certain functions defined on families of sets

  reserve R for Relation;
  reserve A for set;

theorem :: PCOMPS_2:5
   R well_orders A implies R |_2 A well_orders A & A = field (R |_2 A);

scheme MinSet{A()->set,R()->Relation,P[set]}:
  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) equals
:: PCOMPS_2:def 1
   union (R-Seg(B));
end;

definition let FX be set, R be Relation;
  func DisjointFam(FX,R) 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 Nat, f be Function of NAT,bool X;
  func PartUnionNat(n,f) 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:6
  PT is_T3 implies
       for FX st FX is_a_cover_of PT & FX is open
         ex HX st HX is open & HX is_a_cover_of PT &
           for V st V in HX ex W st W in FX & Cl V c= W;

theorem :: PCOMPS_2:7
    for PT,FX st PT is_T2 & PT is paracompact &
             FX is_a_cover_of PT & FX is open
         ex GX st GX is open & GX is_a_cover_of PT &
           clf GX is_finer_than FX & GX is locally_finite;

theorem :: PCOMPS_2:8
  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;

canceled 2;

theorem :: PCOMPS_2:11
    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;

definition let PM be non empty set;
           let g be Function of NAT,(bool bool PM)*;
           let n;
     redefine func g.n -> FinSequence of bool bool PM;
     end;

theorem :: PCOMPS_2:12  :: Stone Theorem - general case
   PT is metrizable implies
     for FX being Subset-Family of PT
        st FX is_a_cover_of PT & FX is open
      ex GX being Subset-Family of PT
         st GX is open & GX is_a_cover_of PT &
               GX is_finer_than FX & GX is locally_finite;

theorem :: PCOMPS_2:13  :: Stone Theorem
    PT is metrizable implies PT is paracompact;