:: On Paracompactness of Metrizable Spaces
::  by Leszek Borys
::
:: Received July 23, 1992
:: Copyright (c) 1992-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, 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;