pcomps_1.miz



    begin

    reserve PM for MetrStruct;

    reserve x,y for Element of PM;

    reserve r,p,q,s,t for Real;

    theorem :: PCOMPS_1:1

    

     Th1: for r,p be Real st r <= p holds ( Ball (x,r)) c= ( Ball (x,p))

    proof

      let r,p be Real;

      assume

       A1: r <= p;

      for y holds y in ( Ball (x,r)) implies y in ( Ball (x,p))

      proof

        let y;

        assume

         A2: y in ( Ball (x,r));

        then ( dist (x,y)) < r by METRIC_1: 11;

        then

         A3: ( dist (x,y)) < p by A1, XXREAL_0: 2;

        PM is non empty by A2;

        hence thesis by A3, METRIC_1: 11;

      end;

      hence thesis;

    end;

    reserve T for TopSpace;

    reserve A for Subset of T;

    theorem :: PCOMPS_1:2

    

     Th2: ( Cl A) <> {} iff A <> {}

    proof

      A <> {} implies ( Cl A) <> {}

      proof

        set x = the Element of A;

        

         A1: A c= ( Cl A) by PRE_TOPC: 18;

        assume

         A2: A <> {} ;

        ex x be set st x in ( Cl A)

        proof

          take x;

          thus thesis by A2, A1;

        end;

        hence thesis;

      end;

      hence thesis by PRE_TOPC: 22;

    end;

    reserve T for non empty TopSpace;

    reserve x for Point of T;

    reserve Z,X,V,W,Y,Q for Subset of T;

    reserve FX for Subset-Family of T;

    theorem :: PCOMPS_1:3

    

     Th3: FX is Cover of T implies for x holds ex W st x in W & W in FX

    proof

      assume FX is Cover of T;

      then

       A1: ( union FX) = ( [#] T) by SETFAM_1: 45;

      thus thesis

      proof

        let x;

        thus ex W st x in W & W in FX

        proof

          consider W be set such that

           A2: x in W and

           A3: W in FX by A1, TARSKI:def 4;

          reconsider W as Subset of T by A3;

          take W;

          thus thesis by A2, A3;

        end;

      end;

    end;

    reserve a for set;

    theorem :: PCOMPS_1:4

    the topology of ( 1TopSp a) = ( bool a);

    theorem :: PCOMPS_1:5

    the carrier of ( 1TopSp a) = a;

    theorem :: PCOMPS_1:6

    ( 1TopSp {a}) is compact;

    theorem :: PCOMPS_1:7

    T is T_2 implies {x} is closed;

    reserve x,y for Point of T;

    reserve A,B for Subset of T;

    reserve FX,GX for Subset-Family of T;

    definition

      let T be TopStruct;

      let IT be Subset-Family of T;

      :: PCOMPS_1:def1

      attr IT is locally_finite means for x be Point of T holds ex W be Subset of T st x in W & W is open & { V where V be Subset of T : V in IT & V meets W } is finite;

    end

    theorem :: PCOMPS_1:8

    

     Th8: for W holds { V : V in FX & V meets W } c= FX

    proof

      let W;

      now

        let Y be object;

        assume Y in { V : V in FX & V meets W };

        then ex V st Y = V & V in FX & V meets W;

        hence Y in FX;

      end;

      hence thesis;

    end;

    theorem :: PCOMPS_1:9

    

     Th9: FX c= GX & GX is locally_finite implies FX is locally_finite

    proof

      assume that

       A1: FX c= GX and

       A2: GX is locally_finite;

      now

        let x;

        thus ex W be Subset of T st x in W & W is open & { V : V in FX & V meets W } is finite

        proof

          consider Y be Subset of T such that

           A3: x in Y and

           A4: Y is open and

           A5: { X : X in GX & X meets Y } is finite by A2;

          take W = Y;

          thus x in W by A3;

          thus W is open by A4;

          { V : V in FX & V meets W } c= { X : X in GX & X meets Y }

          proof

            let Z be object;

            assume

             A6: Z in { V : V in FX & V meets W };

            ex X st Z = X & X in GX & X meets Y

            proof

              consider V such that

               A7: Z = V and

               A8: V in FX and

               A9: V meets W by A6;

              take X = V;

              thus Z = X by A7;

              thus X in GX by A1, A8;

              thus thesis by A9;

            end;

            hence Z in { X : X in GX & X meets Y };

          end;

          hence thesis by A5;

        end;

      end;

      hence thesis;

    end;

    theorem :: PCOMPS_1:10

    

     Th10: FX is finite implies FX is locally_finite

    proof

      assume

       A1: FX is finite;

      for x holds ex W be Subset of T st x in W & W is open & { V : V in FX & V meets W } is finite

      proof

        let x;

        take ( [#] T);

        thus x in ( [#] T);

        thus ( [#] T) is open;

        thus thesis by A1, Th8, FINSET_1: 1;

      end;

      hence thesis;

    end;

    definition

      let T be TopStruct, FX be Subset-Family of T;

      :: PCOMPS_1:def2

      func clf FX -> Subset-Family of T means

      : Def2: for Z be Subset of T holds Z in it iff ex W be Subset of T st Z = ( Cl W) & W in FX;

      existence

      proof

        defpred P[ set] means ex W be Subset of T st $1 = ( Cl W) & W in FX;

        thus ex S be Subset-Family of T st for Z be Subset of T holds Z in S iff P[Z] from SUBSET_1:sch 3;

      end;

      uniqueness

      proof

        let HX,GX be Subset-Family of T;

        assume that

         A1: for Z be Subset of T holds Z in HX iff ex W be Subset of T st Z = ( Cl W) & W in FX and

         A2: for X be Subset of T holds X in GX iff ex V be Subset of T st X = ( Cl V) & V in FX;

        now

          let X be object;

          assume

           A3: X in GX;

          then

          reconsider X9 = X as Subset of T;

          ex V be Subset of T st X9 = ( Cl V) & V in FX by A2, A3;

          hence X in HX by A1;

        end;

        then

         A4: GX c= HX;

        now

          let Z be object;

          assume

           A5: Z in HX;

          then

          reconsider Z9 = Z as Subset of T;

          ex W be Subset of T st Z9 = ( Cl W) & W in FX by A1, A5;

          hence Z in GX by A2;

        end;

        then HX c= GX;

        hence thesis by A4, XBOOLE_0:def 10;

      end;

    end

    theorem :: PCOMPS_1:11

    for T be TopSpace, FX be Subset-Family of T holds ( clf FX) is closed

    proof

      let T be TopSpace, FX be Subset-Family of T;

      for V be Subset of T st V in ( clf FX) holds V is closed

      proof

        let V be Subset of T;

        assume V in ( clf FX);

        then ex W be Subset of T st V = ( Cl W) & W in FX by Def2;

        hence thesis;

      end;

      hence thesis by TOPS_2:def 2;

    end;

    theorem :: PCOMPS_1:12

    

     Th12: for T be TopSpace, FX be Subset-Family of T st FX = {} holds ( clf FX) = {}

    proof

      let T be TopSpace, FX be Subset-Family of T;

      reconsider CFX = ( clf FX) as set;

      set X = the Element of CFX;

      assume

       A1: FX = {} ;

      

       A2: for X be set holds not X in CFX

      proof

        let X be set;

        assume

         A3: X in CFX;

        then

        reconsider X as Subset of T;

        ex V be Subset of T st X = ( Cl V) & V in FX by A3, Def2;

        hence thesis by A1;

      end;

      assume not thesis;

      then X in CFX;

      hence contradiction by A2;

    end;

    theorem :: PCOMPS_1:13

    

     Th13: FX = {V} implies ( clf FX) = {( Cl V)}

    proof

      reconsider CFX = ( clf FX) as set;

      assume

       A1: FX = {V};

      for W be object holds W in CFX iff W = ( Cl V)

      proof

        let W be object;

        

         A2: W = ( Cl V) implies W in CFX

        proof

          assume

           A3: W = ( Cl V);

          ex X st W = ( Cl X) & X in FX

          proof

            take V;

            thus thesis by A1, A3, TARSKI:def 1;

          end;

          hence thesis by Def2;

        end;

        W in CFX implies W = ( Cl V)

        proof

          assume

           A4: W in CFX;

          then

          reconsider W as Subset of T;

          ex X st W = ( Cl X) & X in FX by A4, Def2;

          hence thesis by A1, TARSKI:def 1;

        end;

        hence thesis by A2;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: PCOMPS_1:14

    

     Th14: FX c= GX implies ( clf FX) c= ( clf GX)

    proof

      reconsider CFX = ( clf FX), CGX = ( clf GX) as set;

      assume

       A1: FX c= GX;

      for X be object st X in CFX holds X in CGX

      proof

        let X be object;

        assume

         A2: X in CFX;

        then

        reconsider X as Subset of T;

        ex V st X = ( Cl V) & V in FX by A2, Def2;

        hence thesis by A1, Def2;

      end;

      hence thesis;

    end;

    theorem :: PCOMPS_1:15

    

     Th15: ( clf (FX \/ GX)) = (( clf FX) \/ ( clf GX))

    proof

      for X be object holds X in ( clf (FX \/ GX)) iff X in (( clf FX) \/ ( clf GX))

      proof

        let X be object;

         A1:

        now

          assume

           A2: X in (( clf FX) \/ ( clf GX));

          now

            per cases by A2, XBOOLE_0:def 3;

              suppose

               A3: X in ( clf FX);

              then

              reconsider X9 = X as Subset of T;

              ex W st X9 = ( Cl W) & W in (FX \/ GX)

              proof

                consider Z such that

                 A4: X9 = ( Cl Z) & Z in FX by A3, Def2;

                take Z;

                thus thesis by A4, XBOOLE_0:def 3;

              end;

              hence X in ( clf (FX \/ GX)) by Def2;

            end;

              suppose

               A5: X in ( clf GX);

              then

              reconsider X9 = X as Subset of T;

              ex W st X9 = ( Cl W) & W in (FX \/ GX)

              proof

                consider Z such that

                 A6: X9 = ( Cl Z) & Z in GX by A5, Def2;

                take Z;

                thus thesis by A6, XBOOLE_0:def 3;

              end;

              hence X in ( clf (FX \/ GX)) by Def2;

            end;

          end;

          hence X in ( clf (FX \/ GX));

        end;

        now

          assume

           A7: X in ( clf (FX \/ GX));

          then

          reconsider X9 = X as Subset of T;

          consider W such that

           A8: X9 = ( Cl W) and

           A9: W in (FX \/ GX) by A7, Def2;

          now

            per cases by A9, XBOOLE_0:def 3;

              suppose W in FX;

              then X9 in ( clf FX) by A8, Def2;

              hence X9 in (( clf FX) \/ ( clf GX)) by XBOOLE_0:def 3;

            end;

              suppose W in GX;

              then X9 in ( clf GX) by A8, Def2;

              hence X9 in (( clf FX) \/ ( clf GX)) by XBOOLE_0:def 3;

            end;

          end;

          hence X in (( clf FX) \/ ( clf GX));

        end;

        hence thesis by A1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: PCOMPS_1:16

    

     Th16: FX is finite implies ( Cl ( union FX)) = ( union ( clf FX))

    proof

      assume FX is finite;

      then

      consider p be FinSequence such that

       A1: ( rng p) = FX by FINSEQ_1: 52;

      consider n be Nat such that

       A2: ( dom p) = ( Seg n) by FINSEQ_1:def 2;

      defpred P[ Nat] means for GX st GX = (p .: ( Seg $1)) & $1 <= n & 1 <= n holds ( Cl ( union GX)) = ( union ( clf GX));

      

       A3: for k be Nat holds P[k] implies P[(k + 1)]

      proof

        let k be Nat;

        assume

         A4: for GX st GX = (p .: ( Seg k)) & k <= n & 1 <= n holds ( Cl ( union GX)) = ( union ( clf GX));

        let GX such that

         A5: GX = (p .: ( Seg (k + 1)));

        assume that

         A6: (k + 1) <= n and

         A7: 1 <= n;

        now

          reconsider G2 = ( Im (p,(k + 1))) as Subset-Family of T by A1, RELAT_1: 111, TOPS_2: 2;

          reconsider G1 = (p .: ( Seg k)) as Subset-Family of T by A1, RELAT_1: 111, TOPS_2: 2;

          (k + 1) <= (n + 1) by A6, NAT_1: 12;

          then

           A8: k <= n by XREAL_1: 6;

          ( 0 + 1) = 1;

          then 1 <= (k + 1) by XREAL_1: 7;

          then (k + 1) in ( dom p) by A2, A6, FINSEQ_1: 1;

          then

           A9: G2 = {(p . (k + 1))} by FUNCT_1: 59;

          then ( union G2) = (p . (k + 1)) by ZFMISC_1: 25;

          then

          reconsider G3 = (p . (k + 1)) as Subset of T;

          

           A10: ( union ( clf G2)) = ( union {( Cl G3)}) by A9, Th13

          .= ( Cl G3) by ZFMISC_1: 25

          .= ( Cl ( union G2)) by A9, ZFMISC_1: 25;

          

           A11: (p .: ( Seg (k + 1))) = (p .: (( Seg k) \/ {(k + 1)})) by FINSEQ_1: 9

          .= ((p .: ( Seg k)) \/ (p .: {(k + 1)})) by RELAT_1: 120;

          

          then ( Cl ( union GX)) = ( Cl (( union G1) \/ ( union G2))) by A5, ZFMISC_1: 78

          .= (( Cl ( union G1)) \/ ( Cl ( union G2))) by PRE_TOPC: 20;

          then ( Cl ( union GX)) = (( union ( clf G1)) \/ ( union ( clf G2))) by A4, A7, A10, A8;

          then ( Cl ( union GX)) = ( union (( clf G1) \/ ( clf G2))) by ZFMISC_1: 78;

          hence thesis by A5, A11, Th15;

        end;

        hence thesis;

      end;

      

       A12: P[ 0 ]

      proof

        let GX;

        assume that

         A13: GX = (p .: ( Seg 0 )) and 0 <= n and 1 <= n;

        ( union GX) = ( {} T) by A13, ZFMISC_1: 2;

        then ( Cl ( union GX)) = ( {} T) by PRE_TOPC: 22;

        hence thesis by A13, Th12, ZFMISC_1: 2;

      end;

      

       A14: for k be Nat holds P[k] from NAT_1:sch 2( A12, A3);

       A15:

      now

        assume

         A16: 1 <= n;

        FX = (p .: ( Seg n)) by A1, A2, RELAT_1: 113;

        hence thesis by A14, A16;

      end;

       A17:

      now

        assume n = 0 ;

        then ( Seg n) = {} ;

        then

         A18: FX = (p .: {} ) by A1, A2, RELAT_1: 113;

        then ( union FX) = ( {} T) by ZFMISC_1: 2;

        then ( Cl ( union FX)) = ( {} T) by PRE_TOPC: 22;

        hence thesis by A18, Th12, ZFMISC_1: 2;

      end;

      now

        

         A19: 1 = ( 0 + 1);

        assume n <> 0 ;

        hence 1 <= n by A19, NAT_1: 13;

      end;

      hence thesis by A15, A17;

    end;

    theorem :: PCOMPS_1:17

    

     Th17: FX is_finer_than ( clf FX)

    proof

      set GX = ( clf FX);

      for X be set st X in FX holds ex Y be set st Y in GX & X c= Y

      proof

        let X be set;

        assume

         A1: X in FX;

        then

        reconsider X as Subset of T;

        thus thesis

        proof

          reconsider Y = ( Cl X) as set;

          take Y;

          thus Y in GX by A1, Def2;

          thus thesis by PRE_TOPC: 18;

        end;

      end;

      hence thesis by SETFAM_1:def 2;

    end;

    scheme :: PCOMPS_1:sch1

    Lambda1top { T() -> TopSpace , X() -> Subset-Family of T() , Y() -> Subset-Family of T() , F( object) -> Subset of T() } :

ex f be Function of X(), Y() st for Z be Subset of T() st Z in X() holds (f . Z) = F(Z)

      provided

       A1: for Z be Subset of T() st Z in X() holds F(Z) in Y();

      

       A2: for x be object st x in X() holds F(x) in Y() by A1;

      consider f be Function of X(), Y() such that

       A3: for x be object st x in X() holds (f . x) = F(x) from FUNCT_2:sch 2( A2);

      take f;

      thus thesis by A3;

    end;

    theorem :: PCOMPS_1:18

    FX is locally_finite implies ( clf FX) is locally_finite

    proof

      set GX = ( clf FX);

      assume

       A1: FX is locally_finite;

      for x holds ex W be Subset of T st x in W & W is open & { V : V in GX & V meets W } is finite

      proof

        let x;

        thus thesis

        proof

          deffunc G( Subset of T) = ( Cl $1);

          consider W be Subset of T such that

           A2: x in W and

           A3: W is open and

           A4: { V : V in FX & V meets W } is finite by A1;

          take W;

          thus x in W by A2;

          thus W is open by A3;

          set CGX = { V : V in GX & V meets W }, CFX = { V : V in FX & V meets W };

          

           A5: for Y st Y in FX holds G(Y) in GX by Def2;

          consider f be Function of FX, GX such that

           A6: for X st X in FX holds (f . X) = G(X) from Lambda1top( A5);

          

           A7: GX = {} implies FX = {} by Th17, SETFAM_1: 16;

          then

           A8: ( dom f) = FX by FUNCT_2:def 1;

          for Z be object holds Z in (f .: CFX) iff Z in CGX

          proof

            let Z be object;

            

             A9: Z in CGX implies Z in (f .: CFX)

            proof

              assume

               A10: Z in CGX;

              ex Y be set st Y in ( dom f) & Y in CFX & Z = (f . Y)

              proof

                consider V such that

                 A11: Z = V and

                 A12: V in GX and

                 A13: V meets W by A10;

                consider X such that

                 A14: V = ( Cl X) and

                 A15: X in FX by A12, Def2;

                take X;

                

                 A16: (V /\ W) <> {} by A13, XBOOLE_0:def 7;

                ex Q st X = Q & Q in FX & Q meets W

                proof

                  take Q = X;

                  thus X = Q;

                  thus Q in FX by A15;

                  ( Cl (W /\ ( Cl Q))) <> {} by A16, A14, Th2;

                  then ( Cl (W /\ Q)) <> {} by A3, TOPS_1: 14;

                  then (Q /\ W) <> {} by Th2;

                  hence thesis by XBOOLE_0:def 7;

                end;

                hence thesis by A6, A7, A11, A14, FUNCT_2:def 1;

              end;

              hence thesis by FUNCT_1:def 6;

            end;

            Z in (f .: CFX) implies Z in CGX

            proof

              assume Z in (f .: CFX);

              then

              consider Y be object such that

               A17: Y in ( dom f) and

               A18: Y in CFX and

               A19: Z = (f . Y) by FUNCT_1:def 6;

              reconsider Y as Subset of T by A8, A17;

              

               A20: (f . Y) = ( Cl Y) by A6, A8, A17;

              then

              reconsider Z as Subset of T by A19;

              ex V st Y = V & V in FX & V meets W by A18;

              then

               A21: Z meets W by A19, A20, PRE_TOPC: 18, XBOOLE_1: 63;

              Z in GX by A8, A17, A19, A20, Def2;

              hence thesis by A21;

            end;

            hence thesis by A9;

          end;

          hence thesis by A4, TARSKI: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: PCOMPS_1:19

    ( union FX) c= ( union ( clf FX)) by Th17, SETFAM_1: 13;

    theorem :: PCOMPS_1:20

    

     Th20: FX is locally_finite implies ( Cl ( union FX)) = ( union ( clf FX))

    proof

      set UFX = ( Cl ( union FX)), UCFX = ( union ( clf FX));

      assume

       A1: FX is locally_finite;

      for x st x in UFX holds x in UCFX

      proof

        let x;

        consider W be Subset of T such that

         A2: x in W & W is open and

         A3: { V : V in FX & V meets W } is finite by A1;

        set HX = { V : V in FX & V meets W };

        reconsider HX as Subset-Family of T by Th8, TOPS_2: 2;

        

         A4: ( Cl ( union HX)) = ( union ( clf HX)) by A3, Th16;

        set FHX = (FX \ HX);

        

         A5: not x in ( Cl ( union FHX))

        proof

          assume

           A6: x in ( Cl ( union FHX));

          reconsider FHX as set;

          for Z be set st Z in FHX holds Z misses W

          proof

            let Z be set;

            assume

             A7: Z in FHX;

            then

            reconsider Z as Subset of T;

            Z in FX & not Z in HX by A7, XBOOLE_0:def 5;

            hence thesis;

          end;

          then ( union FHX) misses W by ZFMISC_1: 80;

          hence thesis by A2, A6, TOPS_1: 12;

        end;

        (HX \/ (FX \ HX)) = (HX \/ FX) by XBOOLE_1: 39

        .= FX by Th8, XBOOLE_1: 12;

        

        then

         A8: ( Cl ( union FX)) = ( Cl (( union HX) \/ ( union (FX \ HX)))) by ZFMISC_1: 78

        .= (( Cl ( union HX)) \/ ( Cl ( union (FX \ HX)))) by PRE_TOPC: 20;

        ( clf HX) c= ( clf FX) by Th8, Th14;

        then

         A9: ( union ( clf HX)) c= ( union ( clf FX)) by ZFMISC_1: 77;

        assume x in UFX;

        then x in ( Cl ( union HX)) by A5, A8, XBOOLE_0:def 3;

        hence thesis by A4, A9;

      end;

      then

       A10: UFX c= UCFX;

      for x st x in UCFX holds x in UFX

      proof

        let x;

        assume x in UCFX;

        then

        consider X be set such that

         A11: x in X and

         A12: X in ( clf FX) by TARSKI:def 4;

        reconsider X as Subset of T by A12;

        consider Y such that

         A13: X = ( Cl Y) and

         A14: Y in FX by A12, Def2;

        for A be Subset of T st A is open & x in A holds ( union FX) meets A

        proof

          let A be Subset of T;

          assume

           A15: A is open & x in A;

          ex y st y in (( union FX) /\ A)

          proof

            Y meets A by A11, A13, A15, TOPS_1: 12;

            then

            consider z be object such that

             A16: z in (Y /\ A) by XBOOLE_0: 4;

            z in Y by A16, XBOOLE_0:def 4;

            then

             A17: z in ( union FX) by A14, TARSKI:def 4;

            take z;

            z in A by A16, XBOOLE_0:def 4;

            hence thesis by A17, XBOOLE_0:def 4;

          end;

          hence thesis by XBOOLE_0: 4;

        end;

        hence thesis by TOPS_1: 12;

      end;

      then UCFX c= UFX;

      hence thesis by A10, XBOOLE_0:def 10;

    end;

    theorem :: PCOMPS_1:21

    FX is locally_finite & FX is closed implies ( union FX) is closed

    proof

      assume that

       A1: FX is locally_finite and

       A2: FX is closed;

      ( union ( clf FX)) c= ( union FX)

      proof

        set UFX = ( union FX), UCFX = ( union ( clf FX));

        for x st x in UCFX holds x in UFX

        proof

          let x;

          assume x in UCFX;

          then

          consider X be set such that

           A3: x in X and

           A4: X in ( clf FX) by TARSKI:def 4;

          reconsider X as Subset of T by A4;

          consider W be Subset of T such that

           A5: X = ( Cl W) and

           A6: W in FX by A4, Def2;

          reconsider W as Subset of T;

          W is closed by A2, A6, TOPS_2:def 2;

          then x in W by A3, A5, PRE_TOPC: 22;

          hence thesis by A6, TARSKI:def 4;

        end;

        hence thesis;

      end;

      then

       A7: ( Cl ( union FX)) c= ( union FX) by A1, Th20;

      ( union FX) c= ( union ( clf FX)) by Th17, SETFAM_1: 13;

      then ( union FX) c= ( Cl ( union FX)) by A1, Th20;

      hence thesis by A7, XBOOLE_0:def 10;

    end;

    definition

      let IT be TopStruct;

      :: PCOMPS_1:def3

      attr IT is paracompact means for FX be Subset-Family of IT st FX is Cover of IT & FX is open holds ex GX be Subset-Family of IT st GX is open & GX is Cover of IT & GX is_finer_than FX & GX is locally_finite;

    end

    registration

      cluster paracompact for non empty TopSpace;

      existence

      proof

        take PT = ( 1TopSp {1});

        let FX be Subset-Family of PT;

        assume that

         A1: FX is Cover of PT and FX is open;

        consider GX be Subset-Family of PT such that

         A2: GX c= FX & GX is Cover of PT and GX is finite by A1;

        take GX;

        thus thesis by A2, Th10, SETFAM_1: 12, TOPS_2: 11;

      end;

    end

    theorem :: PCOMPS_1:22

    T is compact implies T is paracompact

    proof

      assume

       A1: T is compact;

      for FX st FX is Cover of T & FX is open holds ex GX st GX is open & GX is Cover of T & GX is_finer_than FX & GX is locally_finite

      proof

        let FX;

        assume that

         A2: FX is Cover of T and

         A3: FX is open;

        consider GX such that

         A4: GX c= FX and

         A5: GX is Cover of T and

         A6: GX is finite by A1, A2, A3;

        take GX;

        for W be Subset of T st W in GX holds W is open by A3, A4, TOPS_2:def 1;

        hence GX is open by TOPS_2:def 1;

        thus GX is Cover of T by A5;

        thus GX is_finer_than FX by A4, SETFAM_1: 12;

        thus thesis by A6, Th10;

      end;

      hence thesis;

    end;

    theorem :: PCOMPS_1:23

    

     Th23: T is paracompact & B is closed & (for x st x in B holds ex V,W be Subset of T st V is open & W is open & A c= V & x in W & V misses W) implies ex Y,Z be Subset of T st Y is open & Z is open & A c= Y & B c= Z & Y misses Z

    proof

      assume that

       A1: T is paracompact and

       A2: B is closed and

       A3: for x st x in B holds ex V,W be Subset of T st V is open & W is open & A c= V & x in W & V misses W;

      defpred P[ set] means $1 = (B ` ) or ex V,W be Subset of T, x st x in B & $1 = W & V is open & W is open & A c= V & x in W & V misses W;

      consider GX such that

       A4: for X be Subset of T holds X in GX iff P[X] from SUBSET_1:sch 3;

      now

        let x;

        assume x in ( [#] T);

        then

         A5: x in (B \/ (B ` )) by PRE_TOPC: 2;

        now

          per cases by A5, XBOOLE_0:def 3;

            suppose

             A6: x in B;

            ex X st x in X & X in GX

            proof

              consider V,W be Subset of T such that

               A7: V is open & W is open & A c= V and

               A8: x in W and

               A9: V misses W by A3, A6;

              take X = W;

              thus x in X by A8;

              thus thesis by A4, A6, A7, A8, A9;

            end;

            hence x in ( union GX) by TARSKI:def 4;

          end;

            suppose

             A10: x in (B ` );

            ex X st x in X & X in GX

            proof

              take X = (B ` );

              thus x in X by A10;

              thus thesis by A4;

            end;

            hence x in ( union GX) by TARSKI:def 4;

          end;

        end;

        hence x in ( union GX);

      end;

      then ( [#] T) c= ( union GX);

      then ( [#] T) = ( union GX) by XBOOLE_0:def 10;

      then

       A11: GX is Cover of T by SETFAM_1: 45;

      for X be Subset of T st X in GX holds X is open

      proof

        let X be Subset of T;

        assume

         A12: X in GX;

        now

          per cases by A4, A12;

            suppose X = (B ` );

            hence thesis by A2;

          end;

            suppose ex V,W be Subset of T, y st y in B & X = W & V is open & W is open & A c= V & y in W & V misses W;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      then GX is open by TOPS_2:def 1;

      then

      consider FX such that

       A13: FX is open and

       A14: FX is Cover of T and

       A15: FX is_finer_than GX and

       A16: FX is locally_finite by A1, A11;

      set HX = { W : W in FX & W meets B };

      

       A17: HX c= FX by Th8;

      reconsider HX as Subset-Family of T by Th8, TOPS_2: 2;

      take Y = (( union ( clf HX)) ` );

      take Z = ( union HX);

      ( union ( clf HX)) = ( Cl ( union HX)) by A16, A17, Th9, Th20;

      hence Y is open;

      thus Z is open by A13, A17, TOPS_2: 11, TOPS_2: 19;

      

       A18: for X st X in HX holds (A /\ ( Cl X)) = {}

      proof

        let X;

        assume X in HX;

        then

         A19: ex W st W = X & W in FX & W meets B;

        then

        consider Y be set such that

         A20: Y in GX and

         A21: X c= Y by A15, SETFAM_1:def 2;

        reconsider Y as Subset of T by A20;

        now

          per cases by A4, A20;

            suppose Y = (B ` );

            hence thesis by A19, A21, XBOOLE_1: 63, XBOOLE_1: 79;

          end;

            suppose ex V,W be Subset of T, y st y in B & Y = W & V is open & W is open & A c= V & y in W & V misses W;

            then

            consider V,W be Subset of T, y such that y in B and

             A22: Y = W and

             A23: V is open and W is open and

             A24: A c= V and y in W and

             A25: V misses W;

            V misses X by A21, A22, A25, XBOOLE_1: 63;

            then ( Cl (V /\ X)) = ( Cl ( {} T)) by XBOOLE_0:def 7;

            then ( Cl (V /\ X)) = {} by PRE_TOPC: 22;

            then ( Cl (V /\ ( Cl X))) = {} by A23, TOPS_1: 14;

            then (V /\ ( Cl X)) = {} by Th2;

            then ( Cl X) misses V by XBOOLE_0:def 7;

            then A misses ( Cl X) by A24, XBOOLE_1: 63;

            hence thesis by XBOOLE_0:def 7;

          end;

        end;

        hence thesis;

      end;

      A misses ( union ( clf HX))

      proof

        assume A meets ( union ( clf HX));

        then

        consider x be object such that

         A26: x in A and

         A27: x in ( union ( clf HX)) by XBOOLE_0: 3;

        reconsider x as Point of T by A26;

        now

          assume x in ( union ( clf HX));

          then

          consider X be set such that

           A28: x in X and

           A29: X in ( clf HX) by TARSKI:def 4;

          reconsider X as Subset of T by A29;

          ex W st X = ( Cl W) & W in HX by A29, Def2;

          then (A /\ X) = {} by A18;

          then A misses X by XBOOLE_0:def 7;

          hence not x in A by A28, XBOOLE_0: 3;

        end;

        hence thesis by A26, A27;

      end;

      hence A c= Y by SUBSET_1: 23;

      now

        let y;

        assume

         A30: y in B;

        ex W st y in W & W in HX

        proof

          consider W such that

           A31: y in W and

           A32: W in FX by A14, Th3;

          take W;

          thus y in W by A31;

          W meets B by A30, A31, XBOOLE_0: 3;

          hence thesis by A32;

        end;

        hence y in Z by TARSKI:def 4;

      end;

      hence B c= Z;

      Z c= (Y ` ) by Th17, SETFAM_1: 13;

      hence Y misses Z by SUBSET_1: 23;

    end;

    theorem :: PCOMPS_1:24

    

     Th24: T is T_2 & T is paracompact implies T is regular

    proof

      assume

       A1: T is T_2;

      assume

       A2: T is paracompact;

      for x holds for A be Subset of T st A <> {} & A is closed & x in (A ` ) holds ex W,V be Subset of T st W is open & V is open & x in W & A c= V & W misses V

      proof

        let x;

        let A be Subset of T;

        assume that A <> {} and

         A3: A is closed and

         A4: x in (A ` );

        set B = {x};

        

         A5: not x in A by A4, XBOOLE_0:def 5;

        for y st y in A holds ex V,W be Subset of T st V is open & W is open & B c= V & y in W & V misses W

        proof

          let y;

          assume y in A;

          then

          consider V,W be Subset of T such that

           A6: V is open & W is open & x in V & y in W & V misses W by A1, A5, PRE_TOPC:def 10;

          take V, W;

          thus thesis by A6, ZFMISC_1: 31;

        end;

        then

        consider Y,Z be Subset of T such that

         A7: Y is open & Z is open & B c= Y & A c= Z & Y misses Z by A2, A3, Th23;

        take Y, Z;

        thus thesis by A7, ZFMISC_1: 31;

      end;

      hence thesis;

    end;

    theorem :: PCOMPS_1:25

    T is T_2 & T is paracompact implies T is normal

    proof

      assume that

       A1: T is T_2 and

       A2: T is paracompact;

      for A,B be Subset of T st A <> {} & B <> {} & A is closed & B is closed & A misses B holds ex W,V be Subset of T st W is open & V is open & A c= W & B c= V & W misses V

      proof

        let A,B be Subset of T;

        assume that

         A3: A <> {} and B <> {} and

         A4: A is closed and

         A5: B is closed and

         A6: A misses B;

        for x st x in B holds ex W,V be Subset of T st W is open & V is open & A c= W & x in V & W misses V

        proof

          let x;

          assume x in B;

          then not x in A by A6, XBOOLE_0: 3;

          then

           A7: x in (A ` ) by SUBSET_1: 29;

          T is regular by A1, A2, Th24;

          then

          consider V,W be Subset of T such that

           A8: V is open & W is open & x in V & A c= W & V misses W by A3, A4, A7;

          take W, V;

          thus thesis by A8;

        end;

        then

        consider Y,Z be Subset of T such that

         A9: Y is open & Z is open & A c= Y & B c= Z & Y misses Z by A2, A5, Th23;

        take Y, Z;

        thus thesis by A9;

      end;

      hence thesis;

    end;

    reserve x,y,z for Element of PM;

    reserve V,W,Y for Subset of PM;

    definition

      let PM;

      :: PCOMPS_1:def4

      func Family_open_set (PM) -> Subset-Family of PM means

      : Def4: for V holds V in it iff for x st x in V holds ex r st r > 0 & ( Ball (x,r)) c= V;

      existence

      proof

        defpred P[ set] means for x st x in $1 holds ex r st r > 0 & ( Ball (x,r)) c= $1;

        thus ex S be Subset-Family of PM st for V holds V in S iff P[V] from SUBSET_1:sch 3;

      end;

      uniqueness

      proof

        let FX,GX be Subset-Family of PM;

        assume

         A1: for V holds V in FX iff for x st x in V holds ex r st r > 0 & ( Ball (x,r)) c= V;

        assume

         A2: for W holds W in GX iff for y st y in W holds ex p st p > 0 & ( Ball (y,p)) c= W;

        for Y holds Y in FX iff Y in GX

        proof

          let Y;

           A3:

          now

            assume Y in GX;

            then for x st x in Y holds ex r st r > 0 & ( Ball (x,r)) c= Y by A2;

            hence Y in FX by A1;

          end;

          now

            assume Y in FX;

            then for x st x in Y holds ex r st r > 0 & ( Ball (x,r)) c= Y by A1;

            hence Y in GX by A2;

          end;

          hence thesis by A3;

        end;

        hence thesis by SETFAM_1: 31;

      end;

    end

    theorem :: PCOMPS_1:26

    

     Th26: for x holds ex r st r > 0 & ( Ball (x,r)) c= the carrier of PM

    proof

      let x;

      consider r such that

       A1: r = 1;

      take r;

      thus r > 0 by A1;

      thus thesis;

    end;

    theorem :: PCOMPS_1:27

    

     Th27: for r be Real st PM is triangle & y in ( Ball (x,r)) holds ex p st p > 0 & ( Ball (y,p)) c= ( Ball (x,r))

    proof

      let r be Real;

      reconsider r9 = r as Real;

      assume

       A1: PM is triangle;

      assume

       A2: y in ( Ball (x,r));

      then

       A3: ( dist (x,y)) < r by METRIC_1: 11;

      

       A4: PM is non empty by A2;

      thus thesis

      proof

        set p = (r9 - ( dist (x,y)));

        take p;

        thus p > 0 by A3, XREAL_1: 50;

        for z holds z in ( Ball (y,p)) implies z in ( Ball (x,r))

        proof

          let z;

          assume z in ( Ball (y,p));

          then ( dist (y,z)) < (r9 - ( dist (x,y))) by METRIC_1: 11;

          then

           A5: (( dist (x,y)) + ( dist (y,z))) < r by XREAL_1: 20;

          (( dist (x,y)) + ( dist (y,z))) >= ( dist (x,z)) by A1, METRIC_1: 4;

          then ( dist (x,z)) < r by A5, XXREAL_0: 2;

          hence thesis by A4, METRIC_1: 11;

        end;

        hence thesis;

      end;

    end;

    theorem :: PCOMPS_1:28

    PM is triangle & y in (( Ball (x,r)) /\ ( Ball (z,p))) implies ex q st ( Ball (y,q)) c= ( Ball (x,r)) & ( Ball (y,q)) c= ( Ball (z,p))

    proof

      assume

       A1: PM is triangle;

      assume

       A2: y in (( Ball (x,r)) /\ ( Ball (z,p)));

      then y in ( Ball (x,r)) by XBOOLE_0:def 4;

      then

      consider s such that s > 0 and

       A3: ( Ball (y,s)) c= ( Ball (x,r)) by A1, Th27;

      y in ( Ball (z,p)) by A2, XBOOLE_0:def 4;

      then

      consider t such that t > 0 and

       A4: ( Ball (y,t)) c= ( Ball (z,p)) by A1, Th27;

      take q = ( min (s,t));

      ( Ball (y,q)) c= ( Ball (y,s)) by Th1, XXREAL_0: 17;

      hence ( Ball (y,q)) c= ( Ball (x,r)) by A3;

      ( Ball (y,q)) c= ( Ball (y,t)) by Th1, XXREAL_0: 17;

      hence thesis by A4;

    end;

    theorem :: PCOMPS_1:29

    

     Th29: for r be Real st PM is triangle holds ( Ball (x,r)) in ( Family_open_set PM)

    proof

      let r be Real;

      assume PM is triangle;

      then for y st y in ( Ball (x,r)) holds ex p st p > 0 & ( Ball (y,p)) c= ( Ball (x,r)) by Th27;

      hence thesis by Def4;

    end;

    theorem :: PCOMPS_1:30

    

     Th30: the carrier of PM in ( Family_open_set PM)

    proof

      the carrier of PM c= the carrier of PM & for y st y in the carrier of PM holds ex p st p > 0 & ( Ball (y,p)) c= the carrier of PM by Th26;

      hence thesis by Def4;

    end;

    theorem :: PCOMPS_1:31

    

     Th31: for V, W st V in ( Family_open_set PM) & W in ( Family_open_set PM) holds (V /\ W) in ( Family_open_set PM)

    proof

      let V, W;

      assume that

       A1: V in ( Family_open_set PM) and

       A2: W in ( Family_open_set PM);

      for z st z in (V /\ W) holds ex q st q > 0 & ( Ball (z,q)) c= (V /\ W)

      proof

        let z;

        assume

         A3: z in (V /\ W);

        then z in V by XBOOLE_0:def 4;

        then

        consider p such that

         A4: p > 0 and

         A5: ( Ball (z,p)) c= V by A1, Def4;

        z in W by A3, XBOOLE_0:def 4;

        then

        consider r such that

         A6: r > 0 and

         A7: ( Ball (z,r)) c= W by A2, Def4;

        take q = ( min (p,r));

        thus q > 0 by A4, A6, XXREAL_0: 15;

        ( Ball (z,q)) c= ( Ball (z,r)) by Th1, XXREAL_0: 17;

        then

         A8: ( Ball (z,q)) c= W by A7;

        ( Ball (z,q)) c= ( Ball (z,p)) by Th1, XXREAL_0: 17;

        then ( Ball (z,q)) c= V by A5;

        hence thesis by A8, XBOOLE_1: 19;

      end;

      hence thesis by Def4;

    end;

    theorem :: PCOMPS_1:32

    

     Th32: for A be Subset-Family of PM st A c= ( Family_open_set PM) holds ( union A) in ( Family_open_set PM)

    proof

      let A be Subset-Family of PM;

      assume

       A1: A c= ( Family_open_set PM);

      for x st x in ( union A) holds ex r st r > 0 & ( Ball (x,r)) c= ( union A)

      proof

        let x;

        assume x in ( union A);

        then

        consider W be set such that

         A2: x in W and

         A3: W in A by TARSKI:def 4;

        reconsider W as Subset of PM by A3;

        consider r such that

         A4: r > 0 and

         A5: ( Ball (x,r)) c= W by A1, A2, A3, Def4;

        take r;

        thus r > 0 by A4;

        W c= ( union A) by A3, ZFMISC_1: 74;

        hence thesis by A5;

      end;

      hence thesis by Def4;

    end;

    theorem :: PCOMPS_1:33

    

     Th33: TopStruct (# the carrier of PM, ( Family_open_set PM) #) is TopSpace

    proof

      set T = TopStruct (# the carrier of PM, ( Family_open_set PM) #);

      

       A1: for p,q be Subset of T st p in the topology of T & q in the topology of T holds (p /\ q) in the topology of T by Th31;

      the carrier of T in the topology of T & for a be Subset-Family of T st a c= the topology of T holds ( union a) in the topology of T by Th30, Th32;

      hence thesis by A1, PRE_TOPC:def 1;

    end;

    definition

      let PM;

      :: PCOMPS_1:def5

      func TopSpaceMetr PM -> TopStruct equals TopStruct (# the carrier of PM, ( Family_open_set PM) #);

      coherence ;

    end

    registration

      let PM;

      cluster ( TopSpaceMetr PM) -> strict TopSpace-like;

      coherence by Th33;

    end

    registration

      let PM be non empty MetrStruct;

      cluster ( TopSpaceMetr PM) -> non empty;

      coherence ;

    end

    theorem :: PCOMPS_1:34

    

     Th34: for PM be non empty MetrSpace holds ( TopSpaceMetr PM) is T_2

    proof

      let PM be non empty MetrSpace;

      set TPS = ( TopSpaceMetr PM);

      for x,y be Element of TPS st not x = y holds ex W,V be Subset of TPS st W is open & V is open & x in W & y in V & W misses V

      proof

        let x,y be Element of TPS;

        assume

         A1: not x = y;

        reconsider x, y as Element of PM;

        set r = (( dist (x,y)) / 2);

        ( dist (x,y)) <> 0 by A1, METRIC_1: 2;

        then ( dist (x,y)) > 0 by METRIC_1: 5;

        then

         A2: r > 0 by XREAL_1: 139;

        ex W,V be Subset of TPS st W is open & V is open & x in W & y in V & W misses V

        proof

          set V = ( Ball (y,r));

          set W = ( Ball (x,r));

          

           A3: W in ( Family_open_set PM) & V in ( Family_open_set PM) by Th29;

          reconsider W, V as Subset of TPS;

          

           A4: for z be object holds not z in (W /\ V)

          proof

            let z be object;

            assume

             A5: z in (W /\ V);

            then

            reconsider z as Element of PM;

            z in V by A5, XBOOLE_0:def 4;

            then

             A6: ( dist (y,z)) < r by METRIC_1: 11;

            z in W by A5, XBOOLE_0:def 4;

            then ( dist (x,z)) < r by METRIC_1: 11;

            then (( dist (x,z)) + ( dist (y,z))) < (r + r) by A6, XREAL_1: 8;

            hence thesis by METRIC_1: 4;

          end;

          take W, V;

          ( dist (x,x)) = 0 & ( dist (y,y)) = 0 by METRIC_1: 1;

          hence thesis by A2, A3, A4, METRIC_1: 11, PRE_TOPC:def 2, XBOOLE_0: 4;

        end;

        hence thesis;

      end;

      hence thesis by PRE_TOPC:def 10;

    end;

    registration

      cluster T_2 non empty strict for TopSpace;

      existence

      proof

        set M = the non empty MetrSpace;

        take ( TopSpaceMetr M);

        thus thesis by Th34;

      end;

    end

    definition

      let D be set, f be Function of [:D, D:], REAL ;

      :: PCOMPS_1:def6

      pred f is_metric_of D means for a,b,c be Element of D holds ((f . (a,b)) = 0 iff a = b) & (f . (a,b)) = (f . (b,a)) & (f . (a,c)) <= ((f . (a,b)) + (f . (b,c)));

    end

    theorem :: PCOMPS_1:35

    

     Th35: for D be set, f be Function of [:D, D:], REAL holds f is_metric_of D iff MetrStruct (# D, f #) is MetrSpace

    proof

      let D be set, f be Function of [:D, D:], REAL ;

      set DF = MetrStruct (# D, f #);

      

       A1: DF is MetrSpace implies f is_metric_of D

      proof

        assume DF is MetrSpace;

        then

        reconsider DF as MetrSpace;

        for a,b,c be Element of DF holds ((the distance of DF . (a,b)) = 0 iff a = b) & (the distance of DF . (a,b)) = (the distance of DF . (b,a)) & (the distance of DF . (a,c)) <= ((the distance of DF . (a,b)) + (the distance of DF . (b,c)))

        proof

          let a,b,c be Element of DF;

          

           A2: (the distance of DF . (a,b)) = ( dist (a,b)) by METRIC_1:def 1;

          hence (the distance of DF . (a,b)) = 0 iff a = b by METRIC_1: 1, METRIC_1: 2;

          (the distance of DF . (b,a)) = ( dist (b,a)) by METRIC_1:def 1;

          hence (the distance of DF . (a,b)) = (the distance of DF . (b,a)) by A2;

          (the distance of DF . (a,c)) = ( dist (a,c)) & (the distance of DF . (b,c)) = ( dist (b,c)) by METRIC_1:def 1;

          hence thesis by A2, METRIC_1: 4;

        end;

        hence thesis;

      end;

      f is_metric_of D implies DF is MetrSpace

      proof

        assume

         A3: f is_metric_of D;

        for a,b,c be Element of DF holds (( dist (a,b)) = 0 iff a = b) & ( dist (a,b)) = ( dist (b,a)) & ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c)))

        proof

          let a,b,c be Element of DF;

          

           A4: (the distance of DF . (a,b)) = ( dist (a,b)) by METRIC_1:def 1;

          hence ( dist (a,b)) = 0 iff a = b by A3;

          (the distance of DF . (b,a)) = ( dist (b,a)) by METRIC_1:def 1;

          hence ( dist (a,b)) = ( dist (b,a)) by A3, A4;

          (the distance of DF . (a,c)) = ( dist (a,c)) & (the distance of DF . (b,c)) = ( dist (b,c)) by METRIC_1:def 1;

          hence thesis by A3, A4;

        end;

        hence thesis by METRIC_1: 6;

      end;

      hence thesis by A1;

    end;

    definition

      let D be set, f be Function of [:D, D:], REAL ;

      assume

       A1: f is_metric_of D;

      :: PCOMPS_1:def7

      func SpaceMetr (D,f) -> strict MetrSpace equals

      : Def7: MetrStruct (# D, f #);

      coherence by A1, Th35;

    end

    definition

      let IT be TopStruct;

      :: PCOMPS_1:def8

      attr IT is metrizable means ex f be Function of [:the carrier of IT, the carrier of IT:], REAL st f is_metric_of the carrier of IT & ( Family_open_set ( SpaceMetr (the carrier of IT,f))) = the topology of IT;

    end

    registration

      cluster strict metrizable for non empty TopSpace;

      existence

      proof

        set MS = the strict non empty MetrSpace;

        take TS = ( TopSpaceMetr MS);

        reconsider f = the distance of MS as Function of [:the carrier of TS, the carrier of TS:], REAL ;

        thus TS is strict;

        take f;

        thus f is_metric_of the carrier of TS by Th35;

        hence thesis by Def7;

      end;

    end

    theorem :: PCOMPS_1:36

    for D be non empty set, f be Function of [:D, D:], REAL st f is_metric_of D holds ( SpaceMetr (D,f)) is non empty

    proof

      let D be non empty set, f be Function of [:D, D:], REAL ;

      assume f is_metric_of D;

      then ( SpaceMetr (D,f)) = MetrStruct (# D, f #) by Def7;

      hence thesis;

    end;