topmetr.miz



    begin

    reserve r for Real;

    reserve a,b for Real;

    reserve T for non empty TopSpace;

    theorem :: TOPMETR:1

    for T be TopStruct, F be Subset-Family of T holds F is Cover of T iff the carrier of T c= ( union F) by SETFAM_1:def 11;

    reserve A for non empty SubSpace of T;

    theorem :: TOPMETR:2

    T is T_2 implies A is T_2

    proof

      assume

       A1: T is T_2;

      for p,q be Point of A st not p = q holds ex W,V be Subset of A st W is open & V is open & p in W & q in V & W misses V

      proof

        let p,q be Point of A such that

         A2: not p = q;

        reconsider p9 = p, q9 = q as Point of T by PRE_TOPC: 25;

        consider W,V be Subset of T such that

         A3: W is open and

         A4: V is open and

         A5: p9 in W & q9 in V and

         A6: W misses V by A1, A2;

        reconsider W9 = (W /\ ( [#] A)), V9 = (V /\ ( [#] A)) as Subset of A;

        V in the topology of T by A4;

        then

         A7: V9 in the topology of A by PRE_TOPC:def 4;

        take W9, V9;

        W in the topology of T by A3;

        then W9 in the topology of A by PRE_TOPC:def 4;

        hence W9 is open & V9 is open by A7;

        thus p in W9 & q in V9 by A5, XBOOLE_0:def 4;

        

         A8: (W /\ V) = {} by A6, XBOOLE_0:def 7;

        (W9 /\ V9) = ((W /\ (V /\ ( [#] A))) /\ ( [#] A)) by XBOOLE_1: 16

        .= ( {} /\ ( [#] A)) by A8, XBOOLE_1: 16

        .= {} ;

        hence thesis by XBOOLE_0:def 7;

      end;

      hence thesis;

    end;

    theorem :: TOPMETR:3

    

     Th3: for T be TopSpace, A,B be SubSpace of T st the carrier of A c= the carrier of B holds A is SubSpace of B

    proof

      let T be TopSpace, A,B be SubSpace of T;

      assume

       A1: the carrier of A c= the carrier of B;

      

       A2: for P be Subset of A holds P in the topology of A iff ex Q be Subset of B st Q in the topology of B & P = (Q /\ ( [#] A))

      proof

        let P be Subset of A;

        thus P in the topology of A implies ex Q be Subset of B st Q in the topology of B & P = (Q /\ ( [#] A))

        proof

          assume P in the topology of A;

          then

          consider Q9 be Subset of T such that

           A3: Q9 in the topology of T and

           A4: P = (Q9 /\ ( [#] A)) by PRE_TOPC:def 4;

          reconsider Q = (Q9 /\ ( [#] B)) as Subset of B;

          

           A5: Q in the topology of B by A3, PRE_TOPC:def 4;

          P = (Q9 /\ (( [#] B) /\ ( [#] A))) by A1, A4, XBOOLE_1: 28

          .= (Q /\ ( [#] A)) by XBOOLE_1: 16;

          hence thesis by A5;

        end;

        given Q be Subset of B such that

         A6: Q in the topology of B and

         A7: P = (Q /\ ( [#] A));

        consider P9 be Subset of T such that

         A8: P9 in the topology of T and

         A9: Q = (P9 /\ ( [#] B)) by A6, PRE_TOPC:def 4;

        P = (P9 /\ (( [#] B) /\ ( [#] A))) by A7, A9, XBOOLE_1: 16

        .= (P9 /\ ( [#] A)) by A1, XBOOLE_1: 28;

        hence thesis by A8, PRE_TOPC:def 4;

      end;

      the carrier of A c= ( [#] B) by A1;

      hence thesis by A2, PRE_TOPC:def 4;

    end;

    reserve P,Q for Subset of T,

p for Point of T;

    theorem :: TOPMETR:4

    

     Th4: (T | P) is SubSpace of (T | (P \/ Q)) & (T | Q) is SubSpace of (T | (P \/ Q))

    proof

      ( [#] (T | P)) = P & ( [#] (T | (P \/ Q))) = (P \/ Q) by PRE_TOPC:def 5;

      hence (T | P) is SubSpace of (T | (P \/ Q)) by Th3, XBOOLE_1: 7;

      ( [#] (T | Q)) = Q & ( [#] (T | (P \/ Q))) = (P \/ Q) by PRE_TOPC:def 5;

      hence thesis by Th3, XBOOLE_1: 7;

    end;

    theorem :: TOPMETR:5

    for P be non empty Subset of T st p in P holds for Q be a_neighborhood of p holds for p9 be Point of (T | P), Q9 be Subset of (T | P) st Q9 = (Q /\ P) & p9 = p holds Q9 is a_neighborhood of p9

    proof

      let P be non empty Subset of T;

      assume

       A1: p in P;

      let Q be a_neighborhood of p;

      let p9 be Point of (T | P), Q9 be Subset of (T | P) such that

       A2: Q9 = (Q /\ P) and

       A3: p9 = p;

      p in ( Int Q) by CONNSP_2:def 1;

      then

      consider S be Subset of T such that

       A4: S is open and

       A5: S c= Q and

       A6: p in S by TOPS_1: 22;

      reconsider R = (S /\ P) as Subset of (T | P) by TOPS_2: 29;

      

       A7: R c= Q9 by A5, A2, XBOOLE_1: 26;

      (S /\ ( [#] (T | P))) = (S /\ P) by PRE_TOPC:def 5;

      then

       A8: R is open by A4, TOPS_2: 24;

      p9 in R by A1, A6, A3, XBOOLE_0:def 4;

      then p9 in ( Int Q9) by A8, A7, TOPS_1: 22;

      hence thesis by CONNSP_2:def 1;

    end;

    theorem :: TOPMETR:6

    for A,B be TopSpace holds for f be Function of A, B holds for C be Subset of B holds f is continuous implies for h be Function of A, (B | C) st h = f holds h is continuous

    proof

      let A,B be TopSpace, f be Function of A, B, C be Subset of B;

      assume

       A1: f is continuous;

      

       A2: the carrier of (B | C) = ( [#] (B | C))

      .= C by PRE_TOPC:def 5;

      let h be Function of A, (B | C) such that

       A3: h = f;

      

       A4: ( rng f) c= the carrier of (B | C) by A3, RELAT_1:def 19;

      for P be Subset of (B | C) holds P is closed implies (h " P) is closed

      proof

        let P be Subset of (B | C);

        assume P is closed;

        then

        consider Q be Subset of B such that

         A5: Q is closed and

         A6: (Q /\ ( [#] (B | C))) = P by PRE_TOPC: 13;

        (h " P) = (f " (Q /\ C)) by A3, A6, PRE_TOPC:def 5

        .= ((f " Q) /\ (f " C)) by FUNCT_1: 68

        .= ((f " Q) /\ (f " (( rng f) /\ C))) by RELAT_1: 133

        .= ((f " Q) /\ (f " ( rng f))) by A2, A4, XBOOLE_1: 28

        .= ((f " Q) /\ ( dom f)) by RELAT_1: 134

        .= (f " Q) by RELAT_1: 132, XBOOLE_1: 28;

        hence thesis by A1, A5;

      end;

      hence thesis;

    end;

    theorem :: TOPMETR:7

    for X be TopStruct, Y be non empty TopStruct, K0 be Subset of X, f be Function of X, Y, g be Function of (X | K0), Y st f is continuous & g = (f | K0) holds g is continuous

    proof

      let X be TopStruct, Y be non empty TopStruct, K0 be Subset of X, f be Function of X, Y, g be Function of (X | K0), Y;

      assume that

       A1: f is continuous and

       A2: g = (f | K0);

      

       A3: ( [#] Y) <> {} ;

      for G be Subset of Y st G is open holds (g " G) is open

      proof

        let G be Subset of Y;

        ( [#] (X | K0)) = K0 by PRE_TOPC:def 5;

        then

         A4: (g " G) = (( [#] (X | K0)) /\ (f " G)) by A2, FUNCT_1: 70;

        assume G is open;

        then (f " G) is open by A3, A1, TOPS_2: 43;

        hence thesis by A4, TOPS_2: 24;

      end;

      hence thesis by A3, TOPS_2: 43;

    end;

    reserve M for non empty MetrSpace,

p for Point of M;

    

     Lm1: for M be MetrSpace holds MetrStruct (# the carrier of M, the distance of M #) is MetrSpace

    proof

      let M be MetrSpace;

      now

        let a,b,c be Element of MetrStruct (# the carrier of M, the distance of M #);

        reconsider a9 = a, b9 = b, c9 = c as Element of M;

        

         A1: ( dist (a,c)) = (the distance of M . (a,c))

        .= ( dist (a9,c9));

        

         A2: ( dist (a,b)) = (the distance of M . (a,b))

        .= ( dist (a9,b9));

        hence ( dist (a,b)) = 0 iff a = b by METRIC_1: 1, METRIC_1: 2;

        ( dist (b,a)) = (the distance of M . (b,a))

        .= ( dist (b9,a9));

        hence ( dist (a,b)) = ( dist (b,a)) by A2;

        ( dist (b,c)) = (the distance of M . (b,c))

        .= ( dist (b9,c9));

        hence ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c))) by A2, A1, METRIC_1: 4;

      end;

      hence thesis by METRIC_1: 6;

    end;

    definition

      let M be MetrSpace;

      :: TOPMETR:def1

      mode SubSpace of M -> MetrSpace means

      : Def1: the carrier of it c= the carrier of M & for x,y be Point of it holds (the distance of it . (x,y)) = (the distance of M . (x,y));

      existence

      proof

        reconsider MM = MetrStruct (# the carrier of M, the distance of M #) as MetrSpace by Lm1;

        take MM;

        thus the carrier of MM c= the carrier of M;

        let x,y be Point of MM;

        thus thesis;

      end;

    end

    registration

      let M be MetrSpace;

      cluster strict for SubSpace of M;

      existence

      proof

        reconsider MM = MetrStruct (# the carrier of M, the distance of M #) as MetrSpace by Lm1;

        for x,y be Point of MM holds (the distance of MM . (x,y)) = (the distance of M . (x,y));

        then MM is SubSpace of M by Def1;

        hence thesis;

      end;

    end

    registration

      let M be non empty MetrSpace;

      cluster strict non empty for SubSpace of M;

      existence

      proof

        reconsider MM = MetrStruct (# the carrier of M, the distance of M #) as MetrSpace by Lm1;

        for x,y be Point of MM holds (the distance of MM . (x,y)) = (the distance of M . (x,y));

        then MM is SubSpace of M by Def1;

        hence thesis;

      end;

    end

    reserve A for non empty SubSpace of M;

    theorem :: TOPMETR:8

    

     Th8: for p be Point of A holds p is Point of M

    proof

      let p be Point of A;

      p in the carrier of A & the carrier of A c= the carrier of M by Def1;

      hence thesis;

    end;

    theorem :: TOPMETR:9

    

     Th9: for r be Real holds for M be MetrSpace, A be SubSpace of M holds for x be Point of M, x9 be Point of A st x = x9 holds ( Ball (x9,r)) = (( Ball (x,r)) /\ the carrier of A)

    proof

      let r be Real;

      let M be MetrSpace, A be SubSpace of M;

      let x be Point of M, x9 be Point of A;

      assume

       A1: x = x9;

      now

        let a be object;

        assume

         A2: a in ( Ball (x9,r));

        then

        reconsider y9 = a as Point of A;

        the carrier of A c= the carrier of M by Def1;

        then

         A3: M is non empty by A2;

        A is non empty by A2;

        then

        reconsider y = y9 as Point of M by A3, Th8;

        ( dist (x9,y9)) < r by A2, METRIC_1: 11;

        then (the distance of A . (x9,y9)) < r;

        then (the distance of M . (x,y)) < r by A1, Def1;

        then ( dist (x,y)) < r;

        then a in ( Ball (x,r)) by A3, METRIC_1: 11;

        hence a in (( Ball (x,r)) /\ the carrier of A) by A2, XBOOLE_0:def 4;

      end;

      then

       A4: ( Ball (x9,r)) c= (( Ball (x,r)) /\ the carrier of A);

      now

        let a be object;

        assume

         A5: a in (( Ball (x,r)) /\ the carrier of A);

        then

        reconsider y9 = a as Point of A by XBOOLE_0:def 4;

        reconsider y = y9 as Point of M by A5;

        a in ( Ball (x,r)) by A5, XBOOLE_0:def 4;

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

        then (the distance of M . (x,y)) < r;

        then (the distance of A . (x9,y9)) < r by A1, Def1;

        then

         A6: ( dist (x9,y9)) < r;

        the carrier of A is non empty by A5;

        then A is non empty;

        hence a in ( Ball (x9,r)) by A6, METRIC_1: 11;

      end;

      then (( Ball (x,r)) /\ the carrier of A) c= ( Ball (x9,r));

      hence thesis by A4, XBOOLE_0:def 10;

    end;

    definition

      let M be non empty MetrSpace, A be non empty Subset of M;

      :: TOPMETR:def2

      func M | A -> strict SubSpace of M means

      : Def2: the carrier of it = A;

      existence

      proof

        reconsider B = A as non empty set;

        set d = (the distance of M || A);

        

         A1: ( dom d) = (( dom the distance of M) /\ [:A, A:]) by RELAT_1: 61

        .= ( [:the carrier of M, the carrier of M:] /\ [:A, A:]) by FUNCT_2:def 1

        .= [:(the carrier of M /\ A), (the carrier of M /\ A):] by ZFMISC_1: 100

        .= [:(the carrier of M /\ A), A:] by XBOOLE_1: 28

        .= [:A, A:] by XBOOLE_1: 28;

        d = (the distance of M | [:A, A:]);

        then ( rng d) c= REAL by RELAT_1:def 19;

        then

        reconsider d as Function of [:B, B:], REAL by A1, FUNCT_2:def 1, RELSET_1: 4;

        set MM = MetrStruct (# B, d #);

         A2:

        now

          let a,b be Element of MM;

          

          thus ( dist (a,b)) = (the distance of MM . (a,b))

          .= (the distance of M . [a, b]) by A1, FUNCT_1: 47

          .= (the distance of M . (a,b));

        end;

        now

          let a,b,c be Element of MM;

          reconsider a9 = a, b9 = b, c9 = c as Point of M by TARSKI:def 3;

          

           A3: ( dist (a,c)) = (the distance of M . (a,c)) by A2

          .= ( dist (a9,c9));

          ( dist (a,b)) = (the distance of M . (a,b)) by A2

          .= ( dist (a9,b9));

          hence ( dist (a,b)) = 0 iff a = b by METRIC_1: 1, METRIC_1: 2;

          

           A4: ( dist (b,c)) = (the distance of M . (b,c)) by A2

          .= ( dist (b9,c9));

          

          thus ( dist (a,b)) = (the distance of M . (a9,b9)) by A2

          .= ( dist (b9,a9)) by METRIC_1:def 1

          .= (the distance of M . (b9,a9))

          .= ( dist (b,a)) by A2;

          ( dist (a,b)) = (the distance of M . (a,b)) by A2

          .= ( dist (a9,b9));

          hence ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c))) by A3, A4, METRIC_1: 4;

        end;

        then

        reconsider MM as MetrSpace by METRIC_1: 6;

        now

          let x,y be Point of MM;

          

          thus (the distance of MM . (x,y)) = ( dist (x,y))

          .= (the distance of M . (x,y)) by A2;

        end;

        then

        reconsider MM as strict SubSpace of M by Def1;

        take MM;

        thus thesis;

      end;

      uniqueness

      proof

        let S1,S2 be strict SubSpace of M;

        assume that

         A5: the carrier of S1 = A and

         A6: the carrier of S2 = A;

        now

          let a,b be Element of A;

          

          thus (the distance of S1 . (a,b)) = (the distance of M . (a,b)) by A5, Def1

          .= (the distance of S2 . (a,b)) by A6, Def1;

        end;

        hence thesis by A5, A6, BINOP_1: 2;

      end;

    end

    registration

      let M be non empty MetrSpace, A be non empty Subset of M;

      cluster (M | A) -> non empty;

      coherence by Def2;

    end

    definition

      let a,b be Real;

      assume

       A1: a <= b;

      :: TOPMETR:def3

      func Closed-Interval-MSpace (a,b) -> strict non empty SubSpace of RealSpace means

      : Def3: for P be non empty Subset of RealSpace st P = [.a, b.] holds it = ( RealSpace | P);

      existence

      proof

        reconsider P = [.a, b.] as Subset of RealSpace ;

        reconsider P as non empty Subset of RealSpace by A1, XXREAL_1: 1;

        take ( RealSpace | P);

        thus thesis;

      end;

      uniqueness

      proof

        reconsider P = [.a, b.] as Subset of RealSpace ;

        reconsider P as non empty Subset of RealSpace by A1, XXREAL_1: 1;

        let S1,S2 be strict non empty SubSpace of RealSpace ;

        assume that

         A2: for P be non empty Subset of RealSpace st P = [.a, b.] holds S1 = ( RealSpace | P) and

         A3: for P be non empty Subset of RealSpace st P = [.a, b.] holds S2 = ( RealSpace | P);

        

        thus S1 = ( RealSpace | P) by A2

        .= S2 by A3;

      end;

    end

    theorem :: TOPMETR:10

    

     Th10: a <= b implies the carrier of ( Closed-Interval-MSpace (a,b)) = [.a, b.]

    proof

      assume

       A1: a <= b;

      then

      reconsider P = [.a, b.] as non empty Subset of RealSpace by XXREAL_1: 1;

      

      thus the carrier of ( Closed-Interval-MSpace (a,b)) = the carrier of ( RealSpace | P) by A1, Def3

      .= [.a, b.] by Def2;

    end;

    reserve F,G for Subset-Family of M;

    definition

      let M be MetrStruct, F be Subset-Family of M;

      :: TOPMETR:def4

      attr F is being_ball-family means for P be set holds P in F implies ex p be Point of M, r st P = ( Ball (p,r));

    end

    theorem :: TOPMETR:11

    

     Th11: for p,q be Point of RealSpace , x,y be Real holds x = p & y = q implies ( dist (p,q)) = |.(x - y).| by METRIC_1:def 12;

    theorem :: TOPMETR:12

    for M be MetrStruct holds the carrier of M = the carrier of ( TopSpaceMetr M) & the topology of ( TopSpaceMetr M) = ( Family_open_set M);

    theorem :: TOPMETR:13

    

     Th13: ( TopSpaceMetr A) is SubSpace of ( TopSpaceMetr M)

    proof

      set T = ( TopSpaceMetr M), R = ( TopSpaceMetr A);

      thus ( [#] R) c= ( [#] T) by Def1;

      let P be Subset of R;

      thus P in the topology of R implies ex Q be Subset of T st Q in the topology of T & P = (Q /\ ( [#] R))

      proof

        set QQ = { ( Ball (x,r)) where x be Point of M, r be Real : x in P & r > 0 & (( Ball (x,r)) /\ the carrier of A) c= P };

        for X be set st X in QQ holds X c= the carrier of M

        proof

          let X be set;

          assume X in QQ;

          then ex x be Point of M, r be Real st X = ( Ball (x,r)) & x in P & r > 0 & (( Ball (x,r)) /\ the carrier of A) c= P;

          hence thesis;

        end;

        then

        reconsider Q = ( union QQ) as Subset of M by ZFMISC_1: 76;

        reconsider Q9 = Q as Subset of T;

        assume P in the topology of R;

        then

         A1: P in ( Family_open_set A);

        

         A2: P c= (Q9 /\ ( [#] R))

        proof

          reconsider P9 = P as Subset of A;

          let a be object;

          assume

           A3: a in P;

          then

          reconsider x = a as Point of A;

          reconsider x9 = x as Point of M by Th8;

          consider r such that

           A4: r > 0 and

           A5: ( Ball (x,r)) c= P9 by A1, A3, PCOMPS_1:def 4;

          ( Ball (x,r)) = (( Ball (x9,r)) /\ the carrier of A) by Th9;

          then

           A6: ( Ball (x9,r)) in QQ by A3, A4, A5;

          x9 in ( Ball (x9,r)) by A4, TBSP_1: 11;

          then a in Q9 by A6, TARSKI:def 4;

          hence thesis by A3, XBOOLE_0:def 4;

        end;

        take Q9;

        for x be Point of M st x in Q holds ex r st r > 0 & ( Ball (x,r)) c= Q

        proof

          let x be Point of M;

          assume x in Q;

          then

          consider Y be set such that

           A7: x in Y and

           A8: Y in QQ by TARSKI:def 4;

          consider x9 be Point of M, r be Real such that

           A9: Y = ( Ball (x9,r)) and x9 in P and r > 0 and (( Ball (x9,r)) /\ the carrier of A) c= P by A8;

          consider p be Real such that

           A10: p > 0 and

           A11: ( Ball (x,p)) c= ( Ball (x9,r)) by A7, A9, PCOMPS_1: 27;

          take p;

          thus p > 0 by A10;

          Y c= Q by A8, ZFMISC_1: 74;

          hence thesis by A9, A11;

        end;

        then Q in ( Family_open_set M) by PCOMPS_1:def 4;

        hence Q9 in the topology of T;

        (Q9 /\ ( [#] R)) c= P

        proof

          let a be object;

          assume

           A12: a in (Q9 /\ ( [#] R));

          then a in Q9 by XBOOLE_0:def 4;

          then

          consider Y be set such that

           A13: a in Y and

           A14: Y in QQ by TARSKI:def 4;

          consider x be Point of M, r be Real such that

           A15: Y = ( Ball (x,r)) and x in P and r > 0 and

           A16: (( Ball (x,r)) /\ the carrier of A) c= P by A14;

          a in (( Ball (x,r)) /\ the carrier of A) by A12, A13, A15, XBOOLE_0:def 4;

          hence thesis by A16;

        end;

        hence P = (Q9 /\ ( [#] R)) by A2, XBOOLE_0:def 10;

      end;

      reconsider P9 = P as Subset of A;

      given Q be Subset of T such that

       A17: Q in the topology of T and

       A18: P = (Q /\ ( [#] R));

      reconsider Q9 = Q as Subset of M;

      for p be Point of A st p in P9 holds ex r st r > 0 & ( Ball (p,r)) c= P9

      proof

        let p be Point of A;

        reconsider p9 = p as Point of M by Th8;

        assume p in P9;

        then

         A19: p9 in Q9 by A18, XBOOLE_0:def 4;

        Q9 in ( Family_open_set M) by A17;

        then

        consider r such that

         A20: r > 0 and

         A21: ( Ball (p9,r)) c= Q9 by A19, PCOMPS_1:def 4;

        ( Ball (p,r)) = (( Ball (p9,r)) /\ the carrier of A) by Th9;

        then ( Ball (p,r)) c= (Q /\ the carrier of A) by A21, XBOOLE_1: 26;

        then ( Ball (p,r)) c= (Q /\ the carrier of R);

        hence thesis by A18, A20;

      end;

      then P in ( Family_open_set A) by PCOMPS_1:def 4;

      hence thesis;

    end;

    theorem :: TOPMETR:14

    

     Th14: for r be Real holds for M be triangle MetrStruct, p be Point of M holds for P be Subset of ( TopSpaceMetr M) st P = ( Ball (p,r)) holds P is open by PCOMPS_1: 29;

    theorem :: TOPMETR:15

    

     Th15: for P be Subset of ( TopSpaceMetr M) holds P is open iff for p be Point of M st p in P holds ex r be Real st r > 0 & ( Ball (p,r)) c= P by PCOMPS_1:def 4;

    definition

      let M be MetrStruct;

      :: TOPMETR:def5

      attr M is compact means ( TopSpaceMetr M) is compact;

    end

    theorem :: TOPMETR:16

    M is compact iff for F st F is being_ball-family & F is Cover of M holds ex G st G c= F & G is Cover of M & G is finite

    proof

      thus M is compact implies for F st F is being_ball-family & F is Cover of M holds ex G st G c= F & G is Cover of M & G is finite

      proof

        set TM = ( TopSpaceMetr M);

        assume M is compact;

        then

         A1: ( TopSpaceMetr M) is compact;

        let F;

        reconsider TF = F as Subset-Family of TM;

        assume that

         A2: F is being_ball-family and

         A3: F is Cover of M;

        

         A4: TF is open

        proof

          let P be Subset of TM;

          reconsider P9 = P as Subset of M;

          assume P in TF;

          then ex p, r st P9 = ( Ball (p,r)) by A2;

          hence thesis by Th14;

        end;

        the carrier of M c= ( union F) by A3, SETFAM_1:def 11;

        then the carrier of TM c= ( union TF);

        then TF is Cover of TM by SETFAM_1:def 11;

        then

        consider TG be Subset-Family of TM such that

         A5: TG c= TF and

         A6: TG is Cover of TM and

         A7: TG is finite by A1, A4, COMPTS_1:def 1;

        reconsider G = TG as Subset-Family of M;

        take G;

        the carrier of TM c= ( union TG) by A6, SETFAM_1:def 11;

        then the carrier of M c= ( union G);

        hence thesis by A5, A7, SETFAM_1:def 11;

      end;

      thus (for F st F is being_ball-family & F is Cover of M holds ex G st G c= F & G is Cover of M & G is finite) implies M is compact

      proof

        set TM = ( TopSpaceMetr M);

        assume

         A8: for F st F is being_ball-family & F is Cover of M holds ex G st G c= F & G is Cover of M & G is finite;

        now

          let F be Subset-Family of TM;

          set Z = { ( Ball (p,r)) where p be Point of M, r be Real : ex P be Subset of TM st P in F & ( Ball (p,r)) c= P };

          Z c= ( bool the carrier of M)

          proof

            let a be object;

            assume a in Z;

            then ex p be Point of M, r be Real st a = ( Ball (p,r)) & ex P be Subset of TM st P in F & ( Ball (p,r)) c= P;

            hence thesis;

          end;

          then

          reconsider Z as Subset-Family of M;

          assume that

           A9: F is Cover of TM and

           A10: F is open;

          the carrier of M c= ( union Z)

          proof

            let a be object;

            assume a in the carrier of M;

            then

            reconsider p = a as Point of M;

            the carrier of TM c= ( union F) & the carrier of TM = the carrier of M by A9, SETFAM_1:def 11;

            then p in ( union F);

            then

            consider P be set such that

             A11: p in P and

             A12: P in F by TARSKI:def 4;

            reconsider P as Subset of TM by A12;

            P is open by A10, A12;

            then

            consider r be Real such that

             A13: r > 0 and

             A14: ( Ball (p,r)) c= P by A11, Th15;

            reconsider r9 = r as Element of REAL by XREAL_0:def 1;

            

             A15: a in ( Ball (p,r)) by A13, TBSP_1: 11;

            ( Ball (p,r9)) in Z by A12, A14;

            hence thesis by A15, TARSKI:def 4;

          end;

          then

           A16: Z is Cover of M by SETFAM_1:def 11;

          reconsider F9 = F as non empty Subset-Family of TM by A9, TOPS_2: 3;

          defpred X[ object, object] means ex D1,D2 be set st D1 = $1 & D2 = $2 & D1 c= D2;

          Z is being_ball-family

          proof

            let P be set;

            assume P in Z;

            then ex p be Point of M, r be Real st P = ( Ball (p,r)) & ex P be Subset of TM st P in F & ( Ball (p,r)) c= P;

            hence thesis;

          end;

          then

          consider G be Subset-Family of M such that

           A17: G c= Z and

           A18: G is Cover of M and

           A19: G is finite by A8, A16;

          

           A20: for a be object st a in G holds ex u be object st u in F9 & X[a, u]

          proof

            let a be object;

            assume a in G;

            then a in Z by A17;

            then

            consider p be Point of M, r be Real such that

             A21: ( Ball (p,r)) = a and

             A22: ex P be Subset of TM st P in F & ( Ball (p,r)) c= P;

            consider P be Subset of TM such that

             A23: P in F & ( Ball (p,r)) c= P by A22;

            take P;

            thus thesis by A21, A23;

          end;

          consider f be Function of G, F9 such that

           A24: for a be object st a in G holds X[a, (f . a)] from FUNCT_2:sch 1( A20);

          reconsider GG = ( rng f) as Subset-Family of TM by TOPS_2: 2;

          take GG;

          thus GG c= F;

          the carrier of TM c= ( union GG)

          proof

            

             A25: the carrier of TM = the carrier of M & the carrier of M c= ( union G) by A18, SETFAM_1:def 11;

            let a be object;

            assume a in the carrier of TM;

            then

            consider P be set such that

             A26: a in P and

             A27: P in G by A25, TARSKI:def 4;

             X[P, (f . P)] by A24, A27;

            then

             A28: P c= (f . P);

            ( dom f) = G by FUNCT_2:def 1;

            then (f . P) in GG by A27, FUNCT_1:def 3;

            hence thesis by A26, A28, TARSKI:def 4;

          end;

          hence GG is Cover of TM by SETFAM_1:def 11;

          ( dom f) = G by FUNCT_2:def 1;

          hence GG is finite by A19, FINSET_1: 8;

        end;

        then TM is compact by COMPTS_1:def 1;

        hence thesis;

      end;

    end;

    definition

      :: TOPMETR:def6

      func R^1 -> TopSpace equals ( TopSpaceMetr RealSpace );

      correctness ;

    end

    registration

      cluster R^1 -> strict non empty;

      coherence ;

    end

    theorem :: TOPMETR:17

    the carrier of R^1 = REAL ;

    definition

      let a,b be Real;

      :: TOPMETR:def7

      func Closed-Interval-TSpace (a,b) -> strict non empty SubSpace of R^1 equals ( TopSpaceMetr ( Closed-Interval-MSpace (a,b)));

      coherence by Th13;

    end

    theorem :: TOPMETR:18

    

     Th18: a <= b implies the carrier of ( Closed-Interval-TSpace (a,b)) = [.a, b.] by Th10;

    theorem :: TOPMETR:19

    

     Th19: a <= b implies for P be Subset of R^1 st P = [.a, b.] holds ( Closed-Interval-TSpace (a,b)) = ( R^1 | P)

    proof

      assume

       A1: a <= b;

      let P be Subset of R^1 ;

      assume P = [.a, b.];

      then ( [#] ( Closed-Interval-TSpace (a,b))) = P by A1, Th18;

      hence thesis by PRE_TOPC:def 5;

    end;

    theorem :: TOPMETR:20

    

     Th20: ( Closed-Interval-TSpace ( 0 ,1)) = I[01]

    proof

      reconsider P = [. 0 , 1.] as Subset of R^1 ;

      set TR = ( TopSpaceMetr RealSpace );

      reconsider P9 = P as Subset of TR;

      

      thus ( Closed-Interval-TSpace ( 0 ,1)) = (TR | P9) by Th19

      .= I[01] by BORSUK_1:def 13;

    end;

    definition

      :: original: I[01]

      redefine

      func I[01] -> SubSpace of R^1 ;

      coherence by Th20;

    end

    

     Lm2: for r be Real holds r >= 0 & (a + r) <= b implies a <= b

    proof

      let r be Real;

      assume r >= 0 & (a + r) <= b;

      then ((a + r) - r) <= (b - r) & (b - r) <= b by XREAL_1: 9, XREAL_1: 43;

      hence thesis by XXREAL_0: 2;

    end;

    theorem :: TOPMETR:21

    for f be Function of R^1 , R^1 st ex a,b be Real st for x be Real holds (f . x) = ((a * x) + b) holds f is continuous

    proof

      let f be Function of R^1 , R^1 ;

      given a,b be Real such that

       A1: for x be Real holds (f . x) = ((a * x) + b);

      for W be Point of R^1 , G be a_neighborhood of (f . W) holds ex H be a_neighborhood of W st (f .: H) c= G

      proof

        let W be Point of R^1 , G be a_neighborhood of (f . W);

        reconsider Y = (f . W) as Point of RealSpace ;

        

         A2: (f . W) in ( Int G) by CONNSP_2:def 1;

        then

        consider Q be Subset of R^1 such that

         A3: Q is open and

         A4: Q c= G and

         A5: (f . W) in Q by TOPS_1: 22;

        consider r be Real such that

         A6: r > 0 and

         A7: ( Ball (Y,r)) c= Q by A3, A5, Th15;

        now

          per cases ;

            suppose

             A8: a = 0 ;

            set H = ( [#] R^1 );

            W in H;

            then W in ( Int H) by TOPS_1: 23;

            then

            reconsider H as a_neighborhood of W by CONNSP_2:def 1;

            for y be object holds y in {b} iff ex x be object st x in ( dom f) & x in H & y = (f . x)

            proof

              let y be object;

              thus y in {b} implies ex x be object st x in ( dom f) & x in H & y = (f . x)

              proof

                assume

                 A9: y in {b};

                take 0 ;

                ( dom f) = the carrier of R^1 by FUNCT_2:def 1;

                then ( In ( 0 , REAL )) in ( dom f) & ( In ( 0 , REAL )) in H;

                hence 0 in ( dom f) & 0 in H;

                

                thus (f . 0 ) = (( 0 * 0 ) + b) by A1, A8

                .= y by A9, TARSKI:def 1;

              end;

              given x be object such that

               A10: x in ( dom f) and x in H and

               A11: y = (f . x);

              reconsider x as Real by A10;

              y = (( 0 * x) + b) by A1, A8, A11

              .= b;

              hence thesis by TARSKI:def 1;

            end;

            then

             A12: (f .: H) = {b} by FUNCT_1:def 6;

            reconsider W9 = W as Real;

            

             A13: ( Int G) c= G by TOPS_1: 16;

            (f . W) = (( 0 * W9) + b) by A1, A8

            .= b;

            then (f .: H) c= G by A2, A12, A13, ZFMISC_1: 31;

            hence thesis;

          end;

            suppose

             A14: a <> 0 ;

            reconsider W9 = W as Point of RealSpace ;

            set d = (r / (2 * |.a.|));

            reconsider H = ( Ball (W9,d)) as Subset of R^1 ;

            H is open by Th14;

            then

             A15: ( Int H) = H by TOPS_1: 23;

             |.a.| > 0 by A14, COMPLEX1: 47;

            then (2 * |.a.|) > 0 by XREAL_1: 129;

            then W in ( Int H) by A6, A15, TBSP_1: 11, XREAL_1: 139;

            then

            reconsider H as a_neighborhood of W by CONNSP_2:def 1;

            

             A16: (f .: H) c= ( Ball (Y,r))

            proof

              reconsider W99 = W9 as Real;

              let y be object;

              reconsider Y9 = Y as Real;

              assume y in (f .: H);

              then

              consider x be object such that

               A17: x in ( dom f) and

               A18: x in H and

               A19: y = (f . x) by FUNCT_1:def 6;

              reconsider x9 = x as Point of RealSpace by A18;

              reconsider y9 = y as Element of REAL by A17, A19, FUNCT_2: 5;

              reconsider x99 = x9 as Real;

              reconsider yy = y9 as Point of RealSpace ;

              

               A20: |.a.| > 0 by A14, COMPLEX1: 47;

              ( dist (W9,x9)) < d by A18, METRIC_1: 11;

              then |.(W99 - x99).| < d by Th11;

              then ( |.a.| * |.(W99 - x99).|) < ( |.a.| * d) by A20, XREAL_1: 68;

              then |.(a * (W99 - x99)).| < ( |.a.| * d) by COMPLEX1: 65;

              then |.(((a * W99) + b) - ((a * x99) + b)).| < ( |.a.| * d);

              then |.(Y9 - ((a * x99) + b)).| < ( |.a.| * d) by A1;

              then

               A21: |.(Y9 - y9).| < ( |.a.| * d) by A1, A19;

               |.a.| <> 0 by A14, ABSVALUE: 2;

              then

               A22: ( |.a.| * d) = (r / 2) by XCMPLX_1: 92;

              ((r / 2) + (r / 2)) = r & (r / 2) >= 0 by A6, XREAL_1: 136;

              then |.(Y9 - y9).| < r by A21, A22, Lm2;

              then ( dist (Y,yy)) < r by Th11;

              hence thesis by METRIC_1: 11;

            end;

            ( Ball (Y,r)) c= G by A4, A7;

            hence thesis by A16, XBOOLE_1: 1;

          end;

        end;

        hence thesis;

      end;

      hence thesis by BORSUK_1:def 1;

    end;

    theorem :: TOPMETR:22

    for T be non empty TopSpace, A,B be Subset of T st A c= B holds (T | A) is SubSpace of (T | B)

    proof

      let T be non empty TopSpace, A,B be Subset of T;

      assume A c= B;

      then (A \/ B) = B by XBOOLE_1: 12;

      hence thesis by Th4;

    end;

    theorem :: TOPMETR:23

    

     Th23: for a,b,d,e be Real, B be Subset of ( Closed-Interval-TSpace (d,e)) st d <= a & a <= b & b <= e & B = [.a, b.] holds ( Closed-Interval-TSpace (a,b)) = (( Closed-Interval-TSpace (d,e)) | B)

    proof

      let a,b,d,e be Real, B be Subset of ( Closed-Interval-TSpace (d,e));

      assume that

       A1: d <= a and

       A2: a <= b and

       A3: b <= e and

       A4: B = [.a, b.];

      a <= e by A2, A3, XXREAL_0: 2;

      then

       A5: a in [.d, e.] by A1, XXREAL_1: 1;

      

       A6: d <= b by A1, A2, XXREAL_0: 2;

      then

      reconsider A = [.d, e.] as non empty Subset of R^1 by A3, XXREAL_1: 1;

      b in [.d, e.] by A3, A6, XXREAL_1: 1;

      then

       A7: [.a, b.] c= [.d, e.] by A5, XXREAL_2:def 12;

      reconsider B2 = [.a, b.] as non empty Subset of R^1 by A2, XXREAL_1: 1;

      

       A8: ( Closed-Interval-TSpace (a,b)) = ( R^1 | B2) by A2, Th19;

      ( Closed-Interval-TSpace (d,e)) = ( R^1 | A) by A3, A6, Th19, XXREAL_0: 2;

      hence thesis by A4, A8, A7, PRE_TOPC: 7;

    end;

    theorem :: TOPMETR:24

    for a,b be Real, B be Subset of I[01] st 0 <= a & a <= b & b <= 1 & B = [.a, b.] holds ( Closed-Interval-TSpace (a,b)) = ( I[01] | B) by Th20, Th23;

    definition

      let T be 1-sorted;

      :: TOPMETR:def8

      attr T is real-membered means

      : Def8: the carrier of T is real-membered;

    end

    registration

      cluster I[01] -> real-membered;

      coherence by BORSUK_1: 40;

    end

    registration

      cluster non empty real-membered for 1-sorted;

      existence

      proof

        take I[01] ;

        thus thesis;

      end;

    end

    registration

      let S be real-membered 1-sorted;

      cluster the carrier of S -> real-membered;

      coherence by Def8;

    end

    registration

      cluster R^1 -> real-membered;

      coherence ;

    end

    registration

      cluster strict non empty real-membered for TopSpace;

      existence

      proof

        take I[01] ;

        thus thesis;

      end;

    end

    registration

      let T be real-membered TopStruct;

      cluster -> real-membered for SubSpace of T;

      coherence

      proof

        let R be SubSpace of T;

        let x be object;

        the carrier of R c= the carrier of T by BORSUK_1: 1;

        hence thesis;

      end;

    end

    registration

      cluster RealSpace -> real-membered;

      coherence ;

    end