weierstr.miz



    begin

    theorem :: WEIERSTR:1

    

     Th1: for M be MetrSpace, x1,x2 be Point of M, r1,r2 be Real holds ex x be Point of M, r be Real st (( Ball (x1,r1)) \/ ( Ball (x2,r2))) c= ( Ball (x,r))

    proof

      let M be MetrSpace;

      let x1,x2 be Point of M;

      let r1,r2 be Real;

      reconsider x = x1 as Point of M;

      reconsider r = (( |.r1.| + |.r2.|) + ( dist (x1,x2))) as Real;

      take x;

      take r;

      for a be object holds a in (( Ball (x1,r1)) \/ ( Ball (x2,r2))) implies a in ( Ball (x,r))

      proof

        let a be object;

        assume

         A1: a in (( Ball (x1,r1)) \/ ( Ball (x2,r2)));

        then

        reconsider a as Point of M;

        now

          per cases by A1, XBOOLE_0:def 3;

            case

             A2: a in ( Ball (x1,r1));

            r1 <= |.r1.| & 0 <= |.r2.| by ABSVALUE: 4, COMPLEX1: 46;

            then

             A3: (r1 + 0 ) <= ( |.r1.| + |.r2.|) by XREAL_1: 7;

            

             A4: ( dist (x,a)) < r1 by A2, METRIC_1: 11;

             0 <= ( dist (x1,x2)) by METRIC_1: 5;

            then (r1 + 0 ) <= (( |.r1.| + |.r2.|) + ( dist (x1,x2))) by A3, XREAL_1: 7;

            then (( dist (x,a)) - r) < (r1 - r1) by A4, XREAL_1: 14;

            then

             A5: ((( dist (x,a)) - r) + r) < ( 0 + r) by XREAL_1: 8;

            M is non empty by A2;

            hence thesis by A5, METRIC_1: 11;

          end;

            case

             A6: a in ( Ball (x2,r2));

            then ( dist (x2,a)) < r2 by METRIC_1: 11;

            then (( dist (x2,a)) - |.r2.|) < (r2 - r2) by ABSVALUE: 4, XREAL_1: 14;

            then ( dist (x,a)) <= (( dist (x1,x2)) + ( dist (x2,a))) & ((( dist (x2,a)) - |.r2.|) + |.r2.|) < ( 0 + |.r2.|) by METRIC_1: 4, XREAL_1: 8;

            then (( dist (x,a)) - |.r2.|) < ((( dist (x1,x2)) + ( dist (x2,a))) - ( dist (x2,a))) by XREAL_1: 15;

            then ((( dist (x,a)) - |.r2.|) - |.r1.|) < (( dist (x1,x2)) - 0 ) by COMPLEX1: 46, XREAL_1: 14;

            then

             A7: ((( dist (x,a)) - ( |.r1.| + |.r2.|)) + ( |.r1.| + |.r2.|)) < (( |.r1.| + |.r2.|) + ( dist (x1,x2))) by XREAL_1: 8;

            M is non empty by A6;

            hence thesis by A7, METRIC_1: 11;

          end;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: WEIERSTR:2

    

     Th2: for M be MetrSpace, n be Nat, F be Subset-Family of M, p be FinSequence st F is being_ball-family & ( rng p) = F & ( dom p) = ( Seg (n + 1)) holds ex G be Subset-Family of M st (G is finite & G is being_ball-family & ex q be FinSequence st ( rng q) = G & ( dom q) = ( Seg n) & ex x be Point of M st ex r be Real st ( union F) c= (( union G) \/ ( Ball (x,r))))

    proof

      let M be MetrSpace;

      let n be Nat;

      let F be Subset-Family of M;

      let p be FinSequence;

      assume that

       A1: F is being_ball-family and

       A2: ( rng p) = F and

       A3: ( dom p) = ( Seg (n + 1));

      (n + 1) in ( dom p) by A3, FINSEQ_1: 4;

      then (p . (n + 1)) in F by A2, FUNCT_1:def 3;

      then

      consider x be Point of M such that

       A4: ex r be Real st (p . (n + 1)) = ( Ball (x,r)) by A1, TOPMETR:def 4;

      consider r be Real such that

       A5: (p . (n + 1)) = ( Ball (x,r)) by A4;

      reconsider q = (p | ( Seg n)) as FinSequence by FINSEQ_1: 15;

      

       A6: ( rng q) c= ( rng p) by RELAT_1: 70;

      then

      reconsider G = ( rng q) as Subset-Family of M by A2, XBOOLE_1: 1;

      reconsider G as Subset-Family of M;

      ( len p) = (n + 1) by A3, FINSEQ_1:def 3;

      then n <= ( len p) by NAT_1: 11;

      then

       A7: ( dom q) = ( Seg n) by FINSEQ_1: 17;

      then

       A8: (( dom q) \/ {(n + 1)}) = ( dom p) by A3, FINSEQ_1: 9;

      

       A9: ex x be Point of M st ex r be Real st ( union F) c= (( union G) \/ ( Ball (x,r)))

      proof

        take x;

        reconsider r as Real;

        take r;

        ( union F) c= (( union G) \/ ( Ball (x,r)))

        proof

          let t be object;

          assume t in ( union F);

          then

          consider A be set such that

           A10: t in A and

           A11: A in F by TARSKI:def 4;

          consider s be object such that

           A12: s in ( dom p) and

           A13: A = (p . s) by A2, A11, FUNCT_1:def 3;

          now

            per cases by A8, A12, XBOOLE_0:def 3;

              case s in ( dom q);

              then (q . s) in G & (q . s) = A by A13, FUNCT_1: 47, FUNCT_1:def 3;

              then

               A14: t in ( union G) by A10, TARSKI:def 4;

              ( union G) c= (( union G) \/ ( Ball (x,r))) by XBOOLE_1: 7;

              hence thesis by A14;

            end;

              case s in {(n + 1)};

              then (p . s) = ( Ball (x,r)) by A5, TARSKI:def 1;

              hence thesis by A10, A13, XBOOLE_0:def 3;

            end;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      take G;

      for x be set holds x in G implies ex y be Point of M st ex r be Real st x = ( Ball (y,r)) by A1, A2, A6, TOPMETR:def 4;

      hence thesis by A7, A9, TOPMETR:def 4;

    end;

    theorem :: WEIERSTR:3

    

     Th3: for M be MetrSpace, F be Subset-Family of M st F is finite & F is being_ball-family holds ex x be Point of M, r be Real st ( union F) c= ( Ball (x,r))

    proof

      let M be MetrSpace;

      let F be Subset-Family of M;

      assume that

       A1: F is finite and

       A2: F is being_ball-family;

      consider p be FinSequence such that

       A3: ( rng p) = F by A1, FINSEQ_1: 52;

      

       A4: for F be Subset-Family of M st F is finite & F is being_ball-family holds for n be Nat holds for p be FinSequence st ( rng p) = F & ( dom p) = ( Seg n) holds ex x be Point of M, r be Real st ( union F) c= ( Ball (x,r))

      proof

        defpred P[ Nat] means for F be Subset-Family of M st (F is finite & F is being_ball-family) holds for n be Nat st n = $1 holds for p be FinSequence st (( rng p) = F & ( dom p) = ( Seg n)) holds (ex x be Point of M st ex r be Real st ( union F) c= ( Ball (x,r)));

        

         A5: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A6: P[k];

          let F be Subset-Family of M;

          assume that F is finite and

           A7: F is being_ball-family;

          let n be Nat;

          assume

           A8: n = (k + 1);

          let p be FinSequence;

          assume ( rng p) = F & ( dom p) = ( Seg n);

          then

          consider F1 be Subset-Family of M such that

           A9: F1 is finite & F1 is being_ball-family and

           A10: ex p1 be FinSequence st ( rng p1) = F1 & ( dom p1) = ( Seg k) & ex x2 be Point of M st ex r2 be Real st ( union F) c= (( union F1) \/ ( Ball (x2,r2))) by A7, A8, Th2;

          consider x1 be Point of M such that

           A11: ex r be Real st ( union F1) c= ( Ball (x1,r)) by A6, A9, A10;

          consider x2 be Point of M such that

           A12: ex r2 be Real st ( union F) c= (( union F1) \/ ( Ball (x2,r2))) by A10;

          consider r2 be Real such that

           A13: ( union F) c= (( union F1) \/ ( Ball (x2,r2))) by A12;

          consider r1 be Real such that

           A14: ( union F1) c= ( Ball (x1,r1)) by A11;

          consider x be Point of M such that

           A15: ex r be Real st (( Ball (x1,r1)) \/ ( Ball (x2,r2))) c= ( Ball (x,r)) by Th1;

          take x;

          consider r be Real such that

           A16: (( Ball (x1,r1)) \/ ( Ball (x2,r2))) c= ( Ball (x,r)) by A15;

          reconsider r as Real;

          take r;

          (( union F1) \/ ( Ball (x2,r2))) c= (( Ball (x1,r1)) \/ ( Ball (x2,r2))) by A14, XBOOLE_1: 9;

          then ( union F) c= (( Ball (x1,r1)) \/ ( Ball (x2,r2))) by A13;

          hence thesis by A16;

        end;

        

         A17: P[ 0 ]

        proof

          let F be Subset-Family of M;

          assume that F is finite and F is being_ball-family;

          let n be Nat;

          assume n = 0 ;

          then

           A18: ( Seg n) = {} ;

          for p be FinSequence st ( rng p) = F & ( dom p) = ( Seg n) holds ex x be Point of M st ex r be Real st ( union F) c= ( Ball (x,r))

          proof

            set x = the Point of M;

            let p be FinSequence;

            assume

             A19: ( rng p) = F & ( dom p) = ( Seg n);

            take x, 0 ;

            ( union F) = {} by A19, A18, RELAT_1: 42, ZFMISC_1: 2;

            hence thesis;

          end;

          hence thesis;

        end;

        for n be Nat holds P[n] from NAT_1:sch 2( A17, A5);

        hence thesis;

      end;

      ex n be Nat st ( dom p) = ( Seg n) by FINSEQ_1:def 2;

      hence thesis by A2, A4, A3;

    end;

    theorem :: WEIERSTR:4

    

     Th4: for T,S be non empty TopSpace, f be Function of T, S, B be Subset-Family of S st f is continuous & B is open holds (f " B) is open

    proof

      let T,S be non empty TopSpace;

      let f be Function of T, S;

      let B be Subset-Family of S;

      assume that

       A1: f is continuous and

       A2: B is open;

      for P be Subset of T holds P in (f " B) implies P is open

      proof

        let P be Subset of T;

        assume

         A3: P in (f " B);

        thus P is open

        proof

          consider C be Subset of S such that

           A4: C in B and

           A5: P = (f " C) by A3, FUNCT_2:def 9;

          reconsider C as Subset of S;

          ( [#] S) <> {} & C is open by A2, A4, TOPS_2:def 1;

          hence thesis by A1, A5, TOPS_2: 43;

        end;

      end;

      hence thesis by TOPS_2:def 1;

    end;

    theorem :: WEIERSTR:5

    for T,S be non empty TopSpace holds for f be Function of T, S holds for Q be Subset-Family of S holds Q is finite implies (f " Q) is finite

    proof

      let T,S be non empty TopSpace;

      let f be Function of T, S;

      let Q be Subset-Family of S;

      defpred EF[ Subset of ( [#] S), Subset of ( [#] T)] means for s,t be set holds ($1 = s & $2 = t implies t = (f " s));

      assume Q is finite;

      then

      consider s be FinSequence such that

       A1: ( rng s) = Q by FINSEQ_1: 52;

      

       A2: for x be Subset of ( [#] S) holds ex y be Subset of ( [#] T) st EF[x, y]

      proof

        let x be Subset of ( [#] S);

        reconsider x as set;

        set y = (f " x);

        reconsider y as Subset of ( [#] T);

        take y;

        thus thesis;

      end;

      consider F be Function of ( bool ( [#] S)), ( bool ( [#] T)) such that

       A3: for x be Subset of ( [#] S) holds EF[x, (F . x) qua Subset of ( [#] T)] from FUNCT_2:sch 3( A2);

      ( dom F) = ( bool ( [#] S)) by FUNCT_2:def 1;

      then

      reconsider q = (F * s) as FinSequence by A1, FINSEQ_1: 16;

      for x be object holds x in (F .: Q) iff x in (f " Q)

      proof

        let x be object;

        

         A4: ( dom F) = ( bool ( [#] S)) by FUNCT_2:def 1;

        thus x in (F .: Q) implies x in (f " Q)

        proof

          assume x in (F .: Q);

          then

          consider y be object such that

           A5: y in ( dom F) and

           A6: y in Q & x = (F . y) by FUNCT_1:def 6;

          reconsider y as Subset of S by A5;

          (F . y) = (f " y) by A3;

          hence thesis by A6, FUNCT_2:def 9;

        end;

        assume

         A7: x in (f " Q);

        then

        reconsider x as Subset of T;

        consider y be Subset of S such that

         A8: y in Q and

         A9: x = (f " y) by A7, FUNCT_2:def 9;

        x = (F . y) by A3, A9;

        hence thesis by A8, A4, FUNCT_1:def 6;

      end;

      then

       A10: (F .: Q) = (f " Q) by TARSKI: 2;

      ex q be FinSequence st ( rng q) = (f " Q)

      proof

        take q;

        thus thesis by A1, A10, RELAT_1: 127;

      end;

      hence thesis;

    end;

    theorem :: WEIERSTR:6

    for T,S be non empty TopSpace holds for f be Function of T, S holds for P be Subset-Family of T holds P is finite implies (f .: P) is finite

    proof

      let T,S be non empty TopSpace;

      let f be Function of T, S;

      let P be Subset-Family of T;

      defpred EF[ Subset of ( [#] T), Subset of ( [#] S)] means for s,t be set holds ($1 = s & $2 = t implies t = (f .: s));

      assume P is finite;

      then

      consider s be FinSequence such that

       A1: ( rng s) = P by FINSEQ_1: 52;

      

       A2: for x be Subset of ( [#] T) holds ex y be Subset of ( [#] S) st EF[x, y]

      proof

        let x be Subset of ( [#] T);

        reconsider x as set;

        set y = (f .: x);

        reconsider y as Subset of ( [#] S);

        take y;

        thus thesis;

      end;

      consider F be Function of ( bool ( [#] T)), ( bool ( [#] S)) such that

       A3: for x be Subset of ( [#] T) holds EF[x, (F . x) qua Subset of ( [#] S)] from FUNCT_2:sch 3( A2);

      ( dom F) = ( bool ( [#] T)) by FUNCT_2:def 1;

      then

      reconsider q = (F * s) as FinSequence by A1, FINSEQ_1: 16;

      for x be object holds x in (F .: P) iff x in (f .: P)

      proof

        let x be object;

        thus x in (F .: P) implies x in (f .: P)

        proof

          assume x in (F .: P);

          then

          consider y be object such that

           A4: y in ( dom F) and

           A5: y in P & x = (F . y) by FUNCT_1:def 6;

          reconsider y as Subset of T by A4;

          (F . y) = (f .: y) by A3;

          hence thesis by A5, FUNCT_2:def 10;

        end;

        thus x in (f .: P) implies x in (F .: P)

        proof

          assume

           A6: x in (f .: P);

          then

          reconsider x as Subset of S;

          consider y be Subset of T such that

           A7: y in P and

           A8: x = (f .: y) by A6, FUNCT_2:def 10;

          

           A9: ( dom F) = ( bool ( [#] T)) by FUNCT_2:def 1;

          x = (F . y) by A3, A8;

          hence thesis by A7, A9, FUNCT_1:def 6;

        end;

      end;

      then

       A10: (F .: P) = (f .: P) by TARSKI: 2;

      ex q be FinSequence st ( rng q) = (f .: P)

      proof

        take q;

        thus thesis by A1, A10, RELAT_1: 127;

      end;

      hence thesis;

    end;

    theorem :: WEIERSTR:7

    

     Th7: for T,S be non empty TopSpace holds for f be Function of T, S holds for P be Subset of T holds for F be Subset-Family of S holds (ex B be Subset-Family of T st (B c= (f " F) & B is Cover of P & B is finite)) implies ex G be Subset-Family of S st G c= F & G is Cover of (f .: P) & G is finite

    proof

      let T,S be non empty TopSpace;

      let f be Function of T, S;

      let P be Subset of T;

      let F be Subset-Family of S;

      given B be Subset-Family of T such that

       A1: B c= (f " F) and

       A2: B is Cover of P and

       A3: B is finite;

      

       A4: P c= ( union B) by A2, SETFAM_1:def 11;

      now

        per cases ;

          case

           A5: P <> {} ;

          thus ex G be Subset-Family of S st G c= F & G is Cover of (f .: P) & G is finite

          proof

            consider s be FinSequence such that

             A6: ( rng s) = B by A3, FINSEQ_1: 52;

            B <> {} by A4, A5, ZFMISC_1: 2;

            then

            consider D be non empty set such that

             A7: D = B;

            defpred P0[ Element of D, Subset of ( [#] S)] means for x be Element of D st $1 = x holds for y be Subset of ( [#] S) st $2 = y holds (y in F & x = (f " y));

            

             A8: for x be Element of D holds ex y be Subset of ( [#] S) st P0[x, y]

            proof

              let x be Element of D;

              

               A9: x in B by A7;

              then

              reconsider x as Subset of T;

              consider y be Subset of S such that

               A10: y in F & x = (f " y) by A1, A9, FUNCT_2:def 9;

              reconsider y as Subset of ( [#] S);

              take y;

              thus thesis by A10;

            end;

            consider F0 be Function of D, ( bool ( [#] S)) such that

             A11: for x be Element of D holds P0[x, (F0 . x) qua Subset of ( [#] S)] from FUNCT_2:sch 3( A8);

            

             A12: for x be Element of D holds (F0 . x) in F & x = (f " (F0 . x)) by A11;

            reconsider F0 as Function of B, ( bool ( [#] S)) by A7;

            

             A13: ( dom F0) = B by FUNCT_2:def 1;

            then

            reconsider q = (F0 * s) as FinSequence by A6, FINSEQ_1: 16;

            set G = ( rng q);

            

             A14: G c= F

            proof

              let x be object;

              assume x in G;

              then

              consider y be object such that

               A15: y in ( dom q) & x = (q . y) by FUNCT_1:def 3;

              (s . y) in B & x = (F0 . (s . y)) by A13, A15, FUNCT_1: 11, FUNCT_1: 12;

              hence thesis by A7, A12;

            end;

            then

            reconsider G as Subset-Family of S by XBOOLE_1: 1;

            reconsider G as Subset-Family of S;

            take G;

            for x be object holds x in (f .: P) implies x in ( union G)

            proof

              let x be object;

              assume

               A16: x in (f .: P);

              ex A be set st x in A & A in G

              proof

                consider y be object such that

                 A17: y in ( dom f) and

                 A18: y in P and

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

                consider C be set such that

                 A20: y in C and

                 A21: C in B by A4, A18, TARSKI:def 4;

                C = (f " (F0 . C)) by A7, A12, A21;

                then

                 A22: x in (f .: (f " (F0 . C))) by A17, A19, A20, FUNCT_1:def 6;

                set A = (F0 . C);

                take A;

                (f .: (f " (F0 . C))) c= (F0 . C) & G = ( rng F0) by A6, A13, FUNCT_1: 75, RELAT_1: 28;

                hence thesis by A21, A22, FUNCT_2: 4;

              end;

              hence thesis by TARSKI:def 4;

            end;

            then (f .: P) c= ( union G);

            hence thesis by A14, SETFAM_1:def 11;

          end;

          hence thesis;

        end;

          case

           A23: P = {} ;

          ex G be Subset-Family of S st G c= F & G is Cover of (f .: P) & G is finite

          proof

            set G = {} ;

            reconsider G as Subset-Family of S by XBOOLE_1: 2;

            reconsider G as Subset-Family of S;

            take G;

            (f .: P) = {}

            proof

              assume (f .: P) <> {} ;

              then

              consider x be object such that

               A24: x in (f .: P) by XBOOLE_0:def 1;

              ex z be object st z in ( dom f) & z in P & x = (f . z) by A24, FUNCT_1:def 6;

              hence contradiction by A23;

            end;

            hence thesis by SETFAM_1:def 11, ZFMISC_1: 2;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    begin

    theorem :: WEIERSTR:8

    

     Th8: for T,S be non empty TopSpace holds for f be Function of T, S holds for P be Subset of T holds P is compact & f is continuous implies (f .: P) is compact

    proof

      let T,S be non empty TopSpace;

      let f be Function of T, S;

      let P be Subset of T;

      assume that

       A1: P is compact and

       A2: f is continuous;

      P c= ( [#] T);

      then

       A3: P c= ( dom f) by FUNCT_2:def 1;

      for F0 be Subset-Family of S st F0 is Cover of (f .: P) & F0 is open holds ex G be Subset-Family of S st G c= F0 & G is Cover of (f .: P) & G is finite

      proof

        let F0 be Subset-Family of S;

        assume that

         A4: F0 is Cover of (f .: P) and

         A5: F0 is open;

        set B0 = (f " F0);

        

         A6: (f .: P) c= ( union F0) by A4, SETFAM_1:def 11;

        P c= ( union B0)

        proof

          let x be object;

          thus x in P implies x in ( union B0)

          proof

            

             A7: (f " ( union F0)) c= ( union (f " F0))

            proof

              let y be object;

              assume

               A8: y in (f " ( union F0));

              thus y in ( union (f " F0))

              proof

                (f . y) in ( union F0) by A8, FUNCT_1:def 7;

                then

                consider Q be set such that

                 A9: (f . y) in Q & Q in F0 by TARSKI:def 4;

                

                 A10: y in ( dom f) by A8, FUNCT_1:def 7;

                ex Z be set st y in Z & Z in (f " F0)

                proof

                  set Z = (f " Q);

                  take Z;

                  thus thesis by A10, A9, FUNCT_1:def 7, FUNCT_2:def 9;

                end;

                hence thesis by TARSKI:def 4;

              end;

            end;

            assume

             A11: x in P;

            then

             A12: (f . x) in (f .: P) by A3, FUNCT_1:def 6;

            reconsider x as Point of T by A11;

            

             A13: (f . x) in ( union F0) by A6, A12;

            

             A14: (f " {(f . x)}) c= (f " ( union F0))

            proof

              let y be object;

              assume

               A15: y in (f " {(f . x)});

              then (f . y) in {(f . x)} by FUNCT_1:def 7;

              then

               A16: (f . y) in ( union F0) by A13, TARSKI:def 1;

              y in ( dom f) by A15, FUNCT_1:def 7;

              hence thesis by A16, FUNCT_1:def 7;

            end;

            (f . x) in {(f . x)} by TARSKI:def 1;

            then x in (f " {(f . x)}) by A3, A11, FUNCT_1:def 7;

            then x in (f " ( union F0)) by A14;

            hence thesis by A7;

          end;

        end;

        then

         A17: B0 is Cover of P by SETFAM_1:def 11;

        B0 is open by A2, A5, Th4;

        then ex B be Subset-Family of T st B c= B0 & B is Cover of P & B is finite by A1, A17, COMPTS_1:def 4;

        then

        consider G be Subset-Family of S such that

         A18: G c= F0 & G is Cover of (f .: P) & G is finite by Th7;

        take G;

        thus thesis by A18;

      end;

      hence thesis by COMPTS_1:def 4;

    end;

    theorem :: WEIERSTR:9

    for T be non empty TopSpace holds for f be Function of T, R^1 holds for P be Subset of T holds P is compact & f is continuous implies (f .: P) is compact by Th8;

    theorem :: WEIERSTR:10

    for f be Function of ( TOP-REAL 2), R^1 holds for P be Subset of ( TOP-REAL 2) holds P is compact & f is continuous implies (f .: P) is compact by Th8;

    definition

      let P be Subset of R^1 ;

      :: WEIERSTR:def1

      func [#] (P) -> Subset of REAL equals P;

      correctness by TOPMETR: 17;

    end

    theorem :: WEIERSTR:11

    

     Th11: for P be Subset of R^1 holds P is compact implies ( [#] P) is real-bounded

    proof

      let P be Subset of R^1 ;

      assume

       A1: P is compact;

      thus ( [#] P) is real-bounded

      proof

        now

          per cases ;

            case ( [#] P) <> {} ;

            set r0 = 1;

            defpred P[ Subset of R^1 ] means ex x be Point of RealSpace st x in ( [#] P) & $1 = ( Ball (x,r0));

            consider R be Subset-Family of R^1 such that

             A2: for A be Subset of R^1 holds A in R iff P[A] from SUBSET_1:sch 3;

            for x be object holds x in ( [#] P) implies x in ( union R)

            proof

              let x be object;

              assume

               A3: x in ( [#] P);

              then

              reconsider x as Point of RealSpace by METRIC_1:def 13;

              consider A be Subset of RealSpace such that

               A4: A = ( Ball (x,r0));

               R^1 = TopStruct (# the carrier of RealSpace , ( Family_open_set RealSpace ) #) by PCOMPS_1:def 5, TOPMETR:def 6;

              then

              reconsider A as Subset of R^1 ;

              ex A be set st x in A & A in R

              proof

                take A;

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

                hence thesis by A2, A3, A4, METRIC_1: 11;

              end;

              hence thesis by TARSKI:def 4;

            end;

            then ( [#] P) c= ( union R);

            then

             A5: R is Cover of P by SETFAM_1:def 11;

            for A be Subset of R^1 holds A in R implies A is open

            proof

              let A be Subset of R^1 ;

              assume A in R;

              then ex x be Point of RealSpace st x in ( [#] P) & A = ( Ball (x,r0)) by A2;

              hence thesis by TOPMETR: 14, TOPMETR:def 6;

            end;

            then R is open by TOPS_2:def 1;

            then

            consider R0 be Subset-Family of R^1 such that

             A6: R0 c= R and

             A7: R0 is Cover of P and

             A8: R0 is finite by A1, A5, COMPTS_1:def 4;

            

             A9: P c= ( union R0) by A7, SETFAM_1:def 11;

            

             A10: for A be set holds A in R0 implies ex x be Point of RealSpace , r be Real st A = ( Ball (x,r))

            proof

              let A be set;

              assume

               A11: A in R0;

              then

              reconsider A as Subset of R^1 ;

              consider x be Point of RealSpace such that x in ( [#] P) and

               A12: A = ( Ball (x,r0)) by A2, A6, A11;

              take x;

              take r0;

              thus thesis by A12;

            end;

             R^1 = TopStruct (# the carrier of RealSpace , ( Family_open_set RealSpace ) #) by PCOMPS_1:def 5, TOPMETR:def 6;

            then

            reconsider R0 as Subset-Family of RealSpace ;

            R0 is being_ball-family by A10, TOPMETR:def 4;

            then

            consider x1 be Point of RealSpace such that

             A13: ex r1 be Real st ( union R0) c= ( Ball (x1,r1)) by A8, Th3;

            consider r1 be Real such that

             A14: ( union R0) c= ( Ball (x1,r1)) by A13;

            

             A15: ( [#] P) c= ( Ball (x1,r1)) by A9, A14;

            reconsider x1 as Element of REAL by METRIC_1:def 13;

            

             A16: for p be Element of REAL holds p in ( [#] P) implies (x1 - r1) <= p & p <= (x1 + r1)

            proof

              let p be Element of REAL ;

              reconsider a = x1, b = p as Element of RealSpace by METRIC_1:def 13;

              assume p in ( [#] P);

              then ( dist (a,b)) < r1 by A15, METRIC_1: 11;

              then

               A17: |.(x1 - p).| < r1 by TOPMETR: 11;

              then ( - r1) <= (x1 - p) by ABSVALUE: 5;

              then (( - r1) + p) <= x1 by XREAL_1: 19;

              then

               A18: p <= (x1 - ( - r1)) by XREAL_1: 19;

              (x1 - p) <= r1 by A17, ABSVALUE: 5;

              then x1 <= (p + r1) by XREAL_1: 20;

              hence thesis by A18, XREAL_1: 20;

            end;

            (x1 - r1) is LowerBound of ( [#] P)

            proof

              let r be ExtReal;

              thus thesis by A16;

            end;

            then

             A19: ( [#] P) is bounded_below;

            (x1 + r1) is UpperBound of ( [#] P)

            proof

              let r be ExtReal;

              thus thesis by A16;

            end;

            then ( [#] P) is bounded_above;

            hence thesis by A19;

          end;

            case

             A20: ( [#] P) = {} ;

             0 is LowerBound of ( [#] P)

            proof

              let r be ExtReal;

              thus thesis by A20;

            end;

            then

             A21: ( [#] P) is bounded_below;

             0 is UpperBound of ( [#] P)

            proof

              let r be ExtReal;

              thus thesis by A20;

            end;

            then ( [#] P) is bounded_above;

            hence thesis by A21;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: WEIERSTR:12

    

     Th12: for P be Subset of R^1 holds P is compact implies ( [#] P) is closed

    proof

      let P be Subset of R^1 ;

      assume

       A1: P is compact;

      now

        per cases ;

          case

           A2: ( [#] P) <> {} ;

          

           A3: R^1 is T_2 by PCOMPS_1: 34, TOPMETR:def 6;

          for s1 be Real_Sequence st ( rng s1) c= ( [#] P) & s1 is convergent holds ( lim s1) in ( [#] P)

          proof

            let s1 be Real_Sequence;

            assume that

             A4: ( rng s1) c= ( [#] P) and

             A5: s1 is convergent;

            set x = ( lim s1);

            x in REAL by XREAL_0:def 1;

            then

            reconsider x as Point of R^1 by TOPMETR: 17;

            thus ( lim s1) in ( [#] P)

            proof

              assume not ( lim s1) in ( [#] P);

              then x in (P ` ) by SUBSET_1: 29;

              then

              consider Otx,OtP be Subset of R^1 such that

               A6: Otx is open and OtP is open and

               A7: x in Otx and

               A8: P c= OtP & Otx misses OtP by A1, A2, A3, COMPTS_1: 6;

              

               A9: R^1 = TopStruct (# the carrier of RealSpace , ( Family_open_set RealSpace ) #) by PCOMPS_1:def 5, TOPMETR:def 6;

              then

              reconsider x as Point of RealSpace ;

              consider r be Real such that

               A10: r > 0 and

               A11: ( Ball (x,r)) c= Otx by A6, A7, TOPMETR: 15, TOPMETR:def 6;

              reconsider r as Real;

              

               A12: ( Ball (x,r)) = { q where q be Element of RealSpace : ( dist (x,q)) < r } by METRIC_1: 17;

              ( rng s1) misses Otx by A4, A8, XBOOLE_1: 1, XBOOLE_1: 63;

              then

               A13: ( Ball (x,r)) misses ( rng s1) by A11, XBOOLE_1: 63;

               not ex n be Nat st for m be Nat st n <= m holds |.((s1 . m) - ( lim s1)).| < r

              proof

                given n be Nat such that

                 A14: for m be Nat st n <= m holds |.((s1 . m) - ( lim s1)).| < r;

                set m = (n + 1);

                reconsider ls = ( lim s1) as Element of REAL by XREAL_0:def 1;

                 |.((s1 . m) - ls).| < r by A14, NAT_1: 11;

                then ( real_dist . ((s1 . m),ls)) < r by METRIC_1:def 12;

                then

                 A15: ( real_dist . (ls,(s1 . m))) < r by METRIC_1: 9;

                reconsider y = (s1 . m) as Element of RealSpace by A9, TOPMETR: 17;

                

                 A16: (s1 . m) in ( rng s1) by FUNCT_2: 4;

                ( dist (x,y)) = (the distance of RealSpace . (x,y)) by METRIC_1:def 1;

                then y in ( Ball (x,r)) by A12, A15, METRIC_1:def 13;

                then y in (( Ball (x,r)) /\ ( rng s1)) by A16, XBOOLE_0:def 4;

                hence thesis by A13, XBOOLE_0:def 7;

              end;

              hence thesis by A5, A10, SEQ_2:def 7;

            end;

          end;

          hence thesis by RCOMP_1:def 4;

        end;

          case

           A17: ( [#] P) = {} ;

          for s1 be Real_Sequence st ( rng s1) c= ( [#] P) & s1 is convergent holds ( lim s1) in ( [#] P)

          proof

            let s1 be Real_Sequence;

            assume that

             A18: ( rng s1) c= ( [#] P) and s1 is convergent;

             0 in NAT ;

            hence thesis by A17, A18, FUNCT_2: 4;

          end;

          hence thesis by RCOMP_1:def 4;

        end;

      end;

      hence thesis;

    end;

    theorem :: WEIERSTR:13

    

     Th13: for P be Subset of R^1 holds P is compact implies ( [#] P) is compact

    proof

      let P be Subset of R^1 ;

      assume

       A1: P is compact;

      now

        per cases ;

          case ( [#] P) <> {} ;

          ( [#] P) is real-bounded by A1, Th11;

          hence thesis by A1, Th12, RCOMP_1: 11;

        end;

          case

           A2: ( [#] P) = {} ;

          assume not ( [#] P) is compact;

          then

           A3: ex s1 be Real_Sequence st ( rng s1) c= ( [#] P) & not (ex s2 be Real_Sequence st s2 is subsequence of s1 & s2 is convergent & ( lim s2) in ( [#] P)) by RCOMP_1:def 3;

           0 in NAT ;

          hence thesis by A2, A3, FUNCT_2: 4;

        end;

      end;

      hence thesis;

    end;

    

     Lm1: for T be non empty TopSpace holds for f be Function of T, R^1 holds for P be Subset of T holds P <> {} & P is compact & f is continuous implies ex x1,x2 be Point of T st x1 in P & x2 in P & (f . x1) = ( upper_bound ( [#] (f .: P))) & (f . x2) = ( lower_bound ( [#] (f .: P)))

    proof

      let T be non empty TopSpace;

      let f be Function of T, R^1 ;

      let P be Subset of T;

      assume that

       A1: P <> {} and

       A2: P is compact & f is continuous;

      

       A3: ( [#] (f .: P)) <> {}

      proof

        consider x be object such that

         A4: x in P by A1, XBOOLE_0:def 1;

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

        then (f . x) in (f .: P) by A4, FUNCT_1:def 6;

        hence thesis;

      end;

      consider y1,y2 be Real such that

       A5: y1 = ( upper_bound ( [#] (f .: P))) and

       A6: y2 = ( lower_bound ( [#] (f .: P)));

      

       A7: ( [#] (f .: P)) is compact by A2, Th8, Th13;

      then y1 in ( [#] (f .: P)) by A3, A5, RCOMP_1: 14;

      then

      consider x1 be object such that

       A8: x1 in ( dom f) and

       A9: x1 in P & y1 = (f . x1) by FUNCT_1:def 6;

      y2 in ( [#] (f .: P)) by A3, A6, A7, RCOMP_1: 14;

      then

      consider x2 be object such that

       A10: x2 in ( dom f) and

       A11: x2 in P & y2 = (f . x2) by FUNCT_1:def 6;

      reconsider x1, x2 as Point of T by A8, A10;

      take x1;

      take x2;

      thus thesis by A5, A6, A9, A11;

    end;

    definition

      let P be Subset of R^1 ;

      :: WEIERSTR:def2

      func upper_bound (P) -> Real equals ( upper_bound ( [#] P));

      correctness ;

      :: WEIERSTR:def3

      func lower_bound (P) -> Real equals ( lower_bound ( [#] P));

      correctness ;

    end

    ::$Notion-Name

    theorem :: WEIERSTR:14

    

     Th14: for T be non empty TopSpace holds for f be Function of T, R^1 holds for P be Subset of T holds P <> {} & P is compact & f is continuous implies ex x1 be Point of T st x1 in P & (f . x1) = ( upper_bound (f .: P))

    proof

      let T be non empty TopSpace;

      let f be Function of T, R^1 ;

      let P be Subset of T;

      assume P <> {} & P is compact & f is continuous;

      then

      consider x1,x2 be Point of T such that

       A1: x1 in P and x2 in P and

       A2: (f . x1) = ( upper_bound ( [#] (f .: P))) and (f . x2) = ( lower_bound ( [#] (f .: P))) by Lm1;

      take x1;

      thus thesis by A1, A2;

    end;

    ::$Notion-Name

    theorem :: WEIERSTR:15

    

     Th15: for T be non empty TopSpace holds for f be Function of T, R^1 holds for P be Subset of T holds P <> {} & P is compact & f is continuous implies ex x2 be Point of T st x2 in P & (f . x2) = ( lower_bound (f .: P))

    proof

      let T be non empty TopSpace;

      let f be Function of T, R^1 ;

      let P be Subset of T;

      assume P <> {} & P is compact & f is continuous;

      then

      consider x1,x2 be Point of T such that x1 in P and

       A1: x2 in P and (f . x1) = ( upper_bound ( [#] (f .: P))) and

       A2: (f . x2) = ( lower_bound ( [#] (f .: P))) by Lm1;

      take x2;

      thus thesis by A1, A2;

    end;

    begin

    definition

      let M be non empty MetrSpace;

      let x be Point of M;

      :: WEIERSTR:def4

      func dist (x) -> Function of ( TopSpaceMetr M), R^1 means

      : Def4: for y be Point of M holds (it . y) = ( dist (y,x));

      existence

      proof

        defpred EF[ Element of M, Element of R^1 ] means for s be Element of M holds for t be Element of R^1 holds ($1 = s & $2 = t implies t = ( dist (s,x)));

        

         A1: for s be Element of M holds ex t be Element of R^1 st EF[s, t]

        proof

          let s be Element of M;

          ( dist (s,x)) in REAL by XREAL_0:def 1;

          then

          reconsider t = ( dist (s,x)) as Element of R^1 by TOPMETR: 17;

          take t;

          thus thesis;

        end;

        consider F be Function of the carrier of M, the carrier of R^1 such that

         A2: for x be Element of M holds EF[x, (F . x)] from FUNCT_2:sch 3( A1);

        

         A3: for y be Point of M holds (F . y) = ( dist (y,x)) by A2;

        ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

        then

        reconsider F as Function of ( TopSpaceMetr M), R^1 ;

        take F;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( TopSpaceMetr M), R^1 ;

        assume

         A4: for y be Point of M holds (F1 . y) = ( dist (y,x));

        assume

         A5: for y be Point of M holds (F2 . y) = ( dist (y,x));

        for y be object st y in the carrier of ( TopSpaceMetr M) holds (F1 . y) = (F2 . y)

        proof

          let y be object;

          

           A6: ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

          assume y in the carrier of ( TopSpaceMetr M);

          then

          reconsider y as Point of M by A6;

          (F1 . y) = ( dist (y,x)) by A4

          .= (F2 . y) by A5;

          hence thesis;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: WEIERSTR:16

    

     Th16: for M be non empty MetrSpace holds for x be Point of M holds ( dist x) is continuous

    proof

      let M be non empty MetrSpace;

      let x be Point of M;

      

       A1: for P be Subset of R^1 st P is open holds (( dist x) " P) is open

      proof

        let P be Subset of R^1 ;

        assume

         A2: P is open;

        for p be Point of M st p in (( dist x) " P) holds ex r be Real st r > 0 & ( Ball (p,r)) c= (( dist x) " P)

        proof

          let p be Point of M;

          ( dist (p,x)) in REAL by XREAL_0:def 1;

          then

          consider y be Point of RealSpace such that

           A3: y = ( dist (p,x)) by METRIC_1:def 13;

          assume p in (( dist x) " P);

          then

           A4: (( dist x) . p) in P by FUNCT_1:def 7;

          reconsider P as Subset of ( TopSpaceMetr RealSpace ) by TOPMETR:def 6;

          y in P by A4, A3, Def4;

          then

          consider r be Real such that

           A5: r > 0 and

           A6: ( Ball (y,r)) c= P by A2, TOPMETR: 15, TOPMETR:def 6;

          reconsider r as Real;

          take r;

          ( Ball (p,r)) c= (( dist x) " P)

          proof

            let z be object;

            assume

             A7: z in ( Ball (p,r));

            then

            reconsider z as Point of M;

            ( dist (z,x)) in REAL by XREAL_0:def 1;

            then

            consider q be Point of RealSpace such that

             A8: q = ( dist (z,x)) by METRIC_1:def 13;

            ( dist (p,z)) < r by A7, METRIC_1: 11;

            then ( |.(( dist (p,x)) - ( dist (z,x))).| + ( dist (p,z))) < (r + ( dist (p,z))) by METRIC_6: 1, XREAL_1: 8;

            then |.(( dist (p,x)) - ( dist (z,x))).| < r by XREAL_1: 6;

            then ( dist (y,q)) < r by A3, A8, TOPMETR: 11;

            then q in ( Ball (y,r)) by METRIC_1: 11;

            then q in P by A6;

            then

             A9: (( dist x) . z) in P by A8, Def4;

            ( dom ( dist x)) = the carrier of ( TopSpaceMetr M) by FUNCT_2:def 1;

            then ( dom ( dist x)) = the carrier of M by TOPMETR: 12;

            hence thesis by A9, FUNCT_1:def 7;

          end;

          hence thesis by A5;

        end;

        hence (( dist x) " P) is open by TOPMETR: 15;

      end;

      ( [#] R^1 ) <> {} ;

      hence thesis by A1, TOPS_2: 43;

    end;

    theorem :: WEIERSTR:17

    for M be non empty MetrSpace holds for x be Point of M holds for P be Subset of ( TopSpaceMetr M) holds P <> {} & P is compact implies ex x1 be Point of ( TopSpaceMetr M) st x1 in P & (( dist x) . x1) = ( upper_bound (( dist x) .: P)) by Th14, Th16;

    theorem :: WEIERSTR:18

    for M be non empty MetrSpace holds for x be Point of M holds for P be Subset of ( TopSpaceMetr M) holds P <> {} & P is compact implies ex x2 be Point of ( TopSpaceMetr M) st x2 in P & (( dist x) . x2) = ( lower_bound (( dist x) .: P)) by Th15, Th16;

    definition

      let M be non empty MetrSpace;

      let P be Subset of ( TopSpaceMetr M);

      :: WEIERSTR:def5

      func dist_max (P) -> Function of ( TopSpaceMetr M), R^1 means

      : Def5: for x be Point of M holds (it . x) = ( upper_bound (( dist x) .: P));

      existence

      proof

        defpred EF[ Element of M, Element of R^1 ] means for s be Element of M holds for t be Element of R^1 holds ($1 = s & $2 = t implies t = ( upper_bound (( dist s) .: P)));

        

         A1: for s be Element of M holds ex t be Element of R^1 st EF[s, t]

        proof

          let s be Element of M;

          set t = ( upper_bound (( dist s) .: P));

          t in REAL by XREAL_0:def 1;

          then

          reconsider t as Element of R^1 by TOPMETR: 17;

          take t;

          thus thesis;

        end;

        consider F be Function of the carrier of M, the carrier of R^1 such that

         A2: for x be Element of M holds EF[x, (F . x)] from FUNCT_2:sch 3( A1);

        

         A3: for y be Point of M holds (F . y) = ( upper_bound (( dist y) .: P)) by A2;

        ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

        then

        reconsider F as Function of ( TopSpaceMetr M), R^1 ;

        take F;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( TopSpaceMetr M), R^1 ;

        assume

         A4: for y be Point of M holds (F1 . y) = ( upper_bound (( dist y) .: P));

        assume

         A5: for y be Point of M holds (F2 . y) = ( upper_bound (( dist y) .: P));

        for y be object st y in the carrier of ( TopSpaceMetr M) holds (F1 . y) = (F2 . y)

        proof

          let y be object;

          

           A6: ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

          assume y in the carrier of ( TopSpaceMetr M);

          then

          reconsider y as Point of M by A6;

          (F1 . y) = ( upper_bound (( dist y) .: P)) by A4

          .= (F2 . y) by A5;

          hence thesis;

        end;

        hence thesis by FUNCT_2: 12;

      end;

      :: WEIERSTR:def6

      func dist_min (P) -> Function of ( TopSpaceMetr M), R^1 means

      : Def6: for x be Point of M holds (it . x) = ( lower_bound (( dist x) .: P));

      existence

      proof

        defpred EF[ Element of M, Element of R^1 ] means for s be Element of M holds for t be Element of R^1 holds ($1 = s & $2 = t implies t = ( lower_bound (( dist s) .: P)));

        

         A7: for s be Element of M holds ex t be Element of R^1 st EF[s, t]

        proof

          let s be Element of M;

          set t = ( lower_bound (( dist s) .: P));

          t in REAL by XREAL_0:def 1;

          then

          reconsider t as Element of R^1 by TOPMETR: 17;

          take t;

          thus thesis;

        end;

        consider F be Function of the carrier of M, the carrier of R^1 such that

         A8: for x be Element of M holds EF[x, (F . x)] from FUNCT_2:sch 3( A7);

        

         A9: for y be Point of M holds (F . y) = ( lower_bound (( dist y) .: P)) by A8;

        ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

        then

        reconsider F as Function of ( TopSpaceMetr M), R^1 ;

        take F;

        thus thesis by A9;

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( TopSpaceMetr M), R^1 ;

        assume

         A10: for y be Point of M holds (F1 . y) = ( lower_bound (( dist y) .: P));

        assume

         A11: for y be Point of M holds (F2 . y) = ( lower_bound (( dist y) .: P));

        for y be object st y in the carrier of ( TopSpaceMetr M) holds (F1 . y) = (F2 . y)

        proof

          let y be object;

          

           A12: ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

          assume y in the carrier of ( TopSpaceMetr M);

          then

          reconsider y as Point of M by A12;

          (F1 . y) = ( lower_bound (( dist y) .: P)) by A10

          .= (F2 . y) by A11;

          hence thesis;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: WEIERSTR:19

    

     Th19: for M be non empty MetrSpace holds for P be Subset of ( TopSpaceMetr M) st P is compact holds for p1,p2 be Point of M holds p1 in P implies ( dist (p1,p2)) <= ( upper_bound (( dist p2) .: P)) & ( lower_bound (( dist p2) .: P)) <= ( dist (p1,p2))

    proof

      let M be non empty MetrSpace;

      let P be Subset of ( TopSpaceMetr M);

      assume

       A1: P is compact;

      let p1,p2 be Point of M;

      ( dist p2) is continuous by Th16;

      then ( [#] (( dist p2) .: P)) is real-bounded by A1, Th8, Th11;

      then

       A2: ( [#] (( dist p2) .: P)) is bounded_above & ( [#] (( dist p2) .: P)) is bounded_below;

      assume

       A3: p1 in P;

      ( dist (p1,p2)) = (( dist p2) . p1) & ( dom ( dist p2)) = the carrier of ( TopSpaceMetr M) by Def4, FUNCT_2:def 1;

      then ( dist (p1,p2)) in ( [#] (( dist p2) .: P)) by A3, FUNCT_1:def 6;

      hence thesis by A2, SEQ_4:def 1, SEQ_4:def 2;

    end;

    theorem :: WEIERSTR:20

    

     Th20: for M be non empty MetrSpace holds for P be Subset of ( TopSpaceMetr M) st P <> {} & P is compact holds for p1,p2 be Point of M holds |.(( upper_bound (( dist p1) .: P)) - ( upper_bound (( dist p2) .: P))).| <= ( dist (p1,p2))

    proof

      let M be non empty MetrSpace;

      let P be Subset of ( TopSpaceMetr M);

      assume that

       A1: P <> {} and

       A2: P is compact;

      let p1,p2 be Point of M;

      consider x1 be Point of ( TopSpaceMetr M) such that

       A3: x1 in P and

       A4: (( dist p1) . x1) = ( upper_bound (( dist p1) .: P)) by A1, A2, Th14, Th16;

      

       A5: ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

      then

      reconsider x1 as Point of M;

      consider x2 be Point of ( TopSpaceMetr M) such that

       A6: x2 in P and

       A7: (( dist p2) . x2) = ( upper_bound (( dist p2) .: P)) by A1, A2, Th14, Th16;

      reconsider x2 as Point of M by A5;

      

       A8: ( dist (x2,p2)) = ( upper_bound (( dist p2) .: P)) by A7, Def4;

      (( dist p1) . x1) = ( dist (x1,p1)) by Def4;

      then ( dist (x2,p2)) <= (( dist (x2,p1)) + ( dist (p1,p2))) & ( dist (x2,p1)) <= ( dist (x1,p1)) by A2, A4, A6, Th19, METRIC_1: 4;

      then (( dist (x2,p2)) - ( dist (x1,p1))) <= ((( dist (x2,p1)) + ( dist (p1,p2))) - ( dist (x2,p1))) by XREAL_1: 13;

      then

       A9: ( - ( dist (p1,p2))) <= ( - (( dist (x2,p2)) - ( dist (x1,p1)))) by XREAL_1: 24;

      (( dist p2) . x2) = ( dist (x2,p2)) by Def4;

      then ( dist (x1,p1)) <= (( dist (x1,p2)) + ( dist (p2,p1))) & ( dist (x1,p2)) <= ( dist (x2,p2)) by A2, A3, A7, Th19, METRIC_1: 4;

      then

       A10: (( dist (x1,p1)) - ( dist (x2,p2))) <= ((( dist (x1,p2)) + ( dist (p1,p2))) - ( dist (x1,p2))) by XREAL_1: 13;

      ( dist (x1,p1)) = ( upper_bound (( dist p1) .: P)) by A4, Def4;

      hence thesis by A8, A10, A9, ABSVALUE: 5;

    end;

    theorem :: WEIERSTR:21

    for M be non empty MetrSpace holds for P be Subset of ( TopSpaceMetr M) st P <> {} & P is compact holds for p1,p2 be Point of M holds for x1,x2 be Real holds x1 = (( dist_max P) . p1) & x2 = (( dist_max P) . p2) implies |.(x1 - x2).| <= ( dist (p1,p2))

    proof

      let M be non empty MetrSpace;

      let P be Subset of ( TopSpaceMetr M);

      assume

       A1: P <> {} & P is compact;

      let p1,p2 be Point of M;

      let x1,x2 be Real;

      assume

       A2: x1 = (( dist_max P) . p1) & x2 = (( dist_max P) . p2);

      (( dist_max P) . p1) = ( upper_bound (( dist p1) .: P)) & (( dist_max P) . p2) = ( upper_bound (( dist p2) .: P)) by Def5;

      hence thesis by A1, A2, Th20;

    end;

    theorem :: WEIERSTR:22

    

     Th22: for M be non empty MetrSpace holds for P be Subset of ( TopSpaceMetr M) st P <> {} & P is compact holds for p1,p2 be Point of M holds |.(( lower_bound (( dist p1) .: P)) - ( lower_bound (( dist p2) .: P))).| <= ( dist (p1,p2))

    proof

      let M be non empty MetrSpace;

      let P be Subset of ( TopSpaceMetr M);

      assume that

       A1: P <> {} and

       A2: P is compact;

      let p1,p2 be Point of M;

      consider x1 be Point of ( TopSpaceMetr M) such that

       A3: x1 in P and

       A4: (( dist p1) . x1) = ( lower_bound (( dist p1) .: P)) by A1, A2, Th15, Th16;

      

       A5: ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

      then

      reconsider x1 as Point of M;

      consider x2 be Point of ( TopSpaceMetr M) such that

       A6: x2 in P and

       A7: (( dist p2) . x2) = ( lower_bound (( dist p2) .: P)) by A1, A2, Th15, Th16;

      reconsider x2 as Point of M by A5;

      

       A8: ( dist (x2,p2)) = ( lower_bound (( dist p2) .: P)) by A7, Def4;

      (( dist p2) . x2) = ( dist (x2,p2)) by Def4;

      then ( dist (x1,p2)) <= (( dist (x1,p1)) + ( dist (p1,p2))) & ( dist (x2,p2)) <= ( dist (x1,p2)) by A2, A3, A7, Th19, METRIC_1: 4;

      then ( dist (x2,p2)) <= (( dist (x1,p1)) + ( dist (p1,p2))) by XXREAL_0: 2;

      then (( dist (x2,p2)) - ( dist (x1,p1))) <= ( dist (p1,p2)) by XREAL_1: 20;

      then

       A9: ( - ( dist (p1,p2))) <= ( - (( dist (x2,p2)) - ( dist (x1,p1)))) by XREAL_1: 24;

      (( dist p1) . x1) = ( dist (x1,p1)) by Def4;

      then ( dist (x2,p1)) <= (( dist (x2,p2)) + ( dist (p2,p1))) & ( dist (x1,p1)) <= ( dist (x2,p1)) by A2, A4, A6, Th19, METRIC_1: 4;

      then ( dist (x1,p1)) <= (( dist (x2,p2)) + ( dist (p1,p2))) by XXREAL_0: 2;

      then

       A10: (( dist (x1,p1)) - ( dist (x2,p2))) <= ( dist (p1,p2)) by XREAL_1: 20;

      ( dist (x1,p1)) = ( lower_bound (( dist p1) .: P)) by A4, Def4;

      hence thesis by A8, A10, A9, ABSVALUE: 5;

    end;

    theorem :: WEIERSTR:23

    for M be non empty MetrSpace holds for P be Subset of ( TopSpaceMetr M) st P <> {} & P is compact holds for p1,p2 be Point of M holds for x1,x2 be Real holds x1 = (( dist_min P) . p1) & x2 = (( dist_min P) . p2) implies |.(x1 - x2).| <= ( dist (p1,p2))

    proof

      let M be non empty MetrSpace;

      let P be Subset of ( TopSpaceMetr M);

      assume

       A1: P <> {} & P is compact;

      let p1,p2 be Point of M;

      let x1,x2 be Real;

      assume

       A2: x1 = (( dist_min P) . p1) & x2 = (( dist_min P) . p2);

      (( dist_min P) . p1) = ( lower_bound (( dist p1) .: P)) & (( dist_min P) . p2) = ( lower_bound (( dist p2) .: P)) by Def6;

      hence thesis by A1, A2, Th22;

    end;

    

     Lm2: ( [#] R^1 ) <> {} ;

    theorem :: WEIERSTR:24

    

     Th24: for M be non empty MetrSpace holds for X be Subset of ( TopSpaceMetr M) st X <> {} & X is compact holds ( dist_max X) is continuous

    proof

      let M be non empty MetrSpace;

      let X be Subset of ( TopSpaceMetr M);

      assume

       A1: X <> {} & X is compact;

      for P be Subset of R^1 st P is open holds (( dist_max X) " P) is open

      proof

        let P be Subset of R^1 ;

        assume

         A2: P is open;

        for p be Point of M st p in (( dist_max X) " P) holds ex r be Real st r > 0 & ( Ball (p,r)) c= (( dist_max X) " P)

        proof

          let p be Point of M;

          set y = ( upper_bound (( dist p) .: X));

          y in REAL by XREAL_0:def 1;

          then

          reconsider y as Point of RealSpace by METRIC_1:def 13;

          assume p in (( dist_max X) " P);

          then

           A3: (( dist_max X) . p) in P by FUNCT_1:def 7;

          reconsider P as Subset of ( TopSpaceMetr RealSpace ) by TOPMETR:def 6;

          y in P by A3, Def5;

          then

          consider r be Real such that

           A4: r > 0 and

           A5: ( Ball (y,r)) c= P by A2, TOPMETR: 15, TOPMETR:def 6;

          reconsider r as Real;

          take r;

          ( Ball (p,r)) c= (( dist_max X) " P)

          proof

            let z be object;

            assume

             A6: z in ( Ball (p,r));

            then

            reconsider z as Point of M;

            set q = ( upper_bound (( dist z) .: X));

            q in REAL by XREAL_0:def 1;

            then

            reconsider q as Point of RealSpace by METRIC_1:def 13;

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

            then ( |.(( upper_bound (( dist p) .: X)) - ( upper_bound (( dist z) .: X))).| + ( dist (p,z))) < (r + ( dist (p,z))) by A1, Th20, XREAL_1: 8;

            then |.(( upper_bound (( dist p) .: X)) - ( upper_bound (( dist z) .: X))).| < r by XREAL_1: 6;

            then ( dist (y,q)) < r by TOPMETR: 11;

            then

             A7: q in ( Ball (y,r)) by METRIC_1: 11;

            ( dom ( dist_max X)) = the carrier of ( TopSpaceMetr M) by FUNCT_2:def 1;

            then

             A8: ( dom ( dist_max X)) = the carrier of M by TOPMETR: 12;

            q = (( dist_max X) . z) by Def5;

            hence thesis by A5, A7, A8, FUNCT_1:def 7;

          end;

          hence thesis by A4;

        end;

        hence thesis by TOPMETR: 15;

      end;

      hence thesis by Lm2, TOPS_2: 43;

    end;

    theorem :: WEIERSTR:25

    for M be non empty MetrSpace holds for P,Q be Subset of ( TopSpaceMetr M) holds P <> {} & P is compact & Q <> {} & Q is compact implies ex x1 be Point of ( TopSpaceMetr M) st x1 in Q & (( dist_max P) . x1) = ( upper_bound (( dist_max P) .: Q)) by Th14, Th24;

    theorem :: WEIERSTR:26

    for M be non empty MetrSpace holds for P,Q be Subset of ( TopSpaceMetr M) holds P <> {} & P is compact & Q <> {} & Q is compact implies ex x2 be Point of ( TopSpaceMetr M) st x2 in Q & (( dist_max P) . x2) = ( lower_bound (( dist_max P) .: Q)) by Th15, Th24;

    theorem :: WEIERSTR:27

    

     Th27: for M be non empty MetrSpace holds for X be Subset of ( TopSpaceMetr M) st X <> {} & X is compact holds ( dist_min X) is continuous

    proof

      let M be non empty MetrSpace;

      let X be Subset of ( TopSpaceMetr M);

      assume

       A1: X <> {} & X is compact;

      for P be Subset of R^1 st P is open holds (( dist_min X) " P) is open

      proof

        let P be Subset of R^1 ;

        assume

         A2: P is open;

        for p be Point of M st p in (( dist_min X) " P) holds ex r be Real st r > 0 & ( Ball (p,r)) c= (( dist_min X) " P)

        proof

          let p be Point of M;

          assume

           A3: p in (( dist_min X) " P);

          ex r be Real st r > 0 & ( Ball (p,r)) c= (( dist_min X) " P)

          proof

            

             A4: (( dist_min X) . p) in P by A3, FUNCT_1:def 7;

            reconsider P as Subset of ( TopSpaceMetr RealSpace ) by TOPMETR:def 6;

            set y = ( lower_bound (( dist p) .: X));

            y in REAL by XREAL_0:def 1;

            then

            reconsider y as Point of RealSpace by METRIC_1:def 13;

            y in P by A4, Def6;

            then

            consider r be Real such that

             A5: r > 0 and

             A6: ( Ball (y,r)) c= P by A2, TOPMETR: 15, TOPMETR:def 6;

            reconsider r as Real;

            take r;

            ( Ball (p,r)) c= (( dist_min X) " P)

            proof

              let z be object;

              assume

               A7: z in ( Ball (p,r));

              then

              reconsider z as Point of M;

              set q = ( lower_bound (( dist z) .: X));

              q in REAL by XREAL_0:def 1;

              then

              reconsider q as Point of RealSpace by METRIC_1:def 13;

              ( dist (p,z)) < r by A7, METRIC_1: 11;

              then ( |.(( lower_bound (( dist p) .: X)) - ( lower_bound (( dist z) .: X))).| + ( dist (p,z))) < (r + ( dist (p,z))) by A1, Th22, XREAL_1: 8;

              then |.(( lower_bound (( dist p) .: X)) - ( lower_bound (( dist z) .: X))).| < r by XREAL_1: 6;

              then ( dist (y,q)) < r by TOPMETR: 11;

              then

               A8: q in ( Ball (y,r)) by METRIC_1: 11;

              ( dom ( dist_min X)) = the carrier of ( TopSpaceMetr M) by FUNCT_2:def 1;

              then

               A9: ( dom ( dist_min X)) = the carrier of M by TOPMETR: 12;

              q = (( dist_min X) . z) by Def6;

              hence thesis by A6, A8, A9, FUNCT_1:def 7;

            end;

            hence thesis by A5;

          end;

          hence thesis;

        end;

        hence (( dist_min X) " P) is open by TOPMETR: 15;

      end;

      hence thesis by Lm2, TOPS_2: 43;

    end;

    theorem :: WEIERSTR:28

    for M be non empty MetrSpace holds for P,Q be Subset of ( TopSpaceMetr M) holds P <> {} & P is compact & Q <> {} & Q is compact implies ex x1 be Point of ( TopSpaceMetr M) st x1 in Q & (( dist_min P) . x1) = ( upper_bound (( dist_min P) .: Q)) by Th14, Th27;

    theorem :: WEIERSTR:29

    for M be non empty MetrSpace holds for P,Q be Subset of ( TopSpaceMetr M) holds P <> {} & P is compact & Q <> {} & Q is compact implies ex x2 be Point of ( TopSpaceMetr M) st x2 in Q & (( dist_min P) . x2) = ( lower_bound (( dist_min P) .: Q)) by Th15, Th27;

    definition

      let M be non empty MetrSpace;

      let P,Q be Subset of ( TopSpaceMetr M);

      :: WEIERSTR:def7

      func min_dist_min (P,Q) -> Real equals ( lower_bound (( dist_min P) .: Q));

      correctness ;

      :: WEIERSTR:def8

      func max_dist_min (P,Q) -> Real equals ( upper_bound (( dist_min P) .: Q));

      correctness ;

      :: WEIERSTR:def9

      func min_dist_max (P,Q) -> Real equals ( lower_bound (( dist_max P) .: Q));

      correctness ;

      :: WEIERSTR:def10

      func max_dist_max (P,Q) -> Real equals ( upper_bound (( dist_max P) .: Q));

      correctness ;

    end

    theorem :: WEIERSTR:30

    for M be non empty MetrSpace holds for P,Q be Subset of ( TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1,x2 be Point of M st x1 in P & x2 in Q & ( dist (x1,x2)) = ( min_dist_min (P,Q))

    proof

      let M be non empty MetrSpace;

      let P,Q be Subset of ( TopSpaceMetr M);

      assume that

       A1: P <> {} & P is compact and

       A2: Q <> {} & Q is compact;

      consider x2 be Point of ( TopSpaceMetr M) such that

       A3: x2 in Q and

       A4: (( dist_min P) . x2) = ( lower_bound (( dist_min P) .: Q)) by A1, A2, Th15, Th27;

      

       A5: ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

      then

      reconsider x2 as Point of M;

      consider x1 be Point of ( TopSpaceMetr M) such that

       A6: x1 in P and

       A7: (( dist x2) . x1) = ( lower_bound (( dist x2) .: P)) by A1, Th15, Th16;

      reconsider x1 as Point of M by A5;

      take x1;

      take x2;

      ( dist (x1,x2)) = (( dist x2) . x1) by Def4

      .= ( lower_bound (( dist_min P) .: Q)) by A4, A7, Def6;

      hence thesis by A3, A6;

    end;

    theorem :: WEIERSTR:31

    for M be non empty MetrSpace holds for P,Q be Subset of ( TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1,x2 be Point of M st x1 in P & x2 in Q & ( dist (x1,x2)) = ( min_dist_max (P,Q))

    proof

      let M be non empty MetrSpace;

      let P,Q be Subset of ( TopSpaceMetr M);

      assume that

       A1: P <> {} & P is compact and

       A2: Q <> {} & Q is compact;

      consider x2 be Point of ( TopSpaceMetr M) such that

       A3: x2 in Q and

       A4: (( dist_max P) . x2) = ( lower_bound (( dist_max P) .: Q)) by A1, A2, Th15, Th24;

      

       A5: ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

      then

      reconsider x2 as Point of M;

      consider x1 be Point of ( TopSpaceMetr M) such that

       A6: x1 in P and

       A7: (( dist x2) . x1) = ( upper_bound (( dist x2) .: P)) by A1, Th14, Th16;

      reconsider x1 as Point of M by A5;

      take x1;

      take x2;

      ( dist (x1,x2)) = (( dist x2) . x1) by Def4

      .= ( lower_bound (( dist_max P) .: Q)) by A4, A7, Def5;

      hence thesis by A3, A6;

    end;

    theorem :: WEIERSTR:32

    for M be non empty MetrSpace holds for P,Q be Subset of ( TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1,x2 be Point of M st x1 in P & x2 in Q & ( dist (x1,x2)) = ( max_dist_min (P,Q))

    proof

      let M be non empty MetrSpace;

      let P,Q be Subset of ( TopSpaceMetr M);

      assume that

       A1: P <> {} & P is compact and

       A2: Q <> {} & Q is compact;

      consider x2 be Point of ( TopSpaceMetr M) such that

       A3: x2 in Q and

       A4: (( dist_min P) . x2) = ( upper_bound (( dist_min P) .: Q)) by A1, A2, Th14, Th27;

      

       A5: ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

      then

      reconsider x2 as Point of M;

      consider x1 be Point of ( TopSpaceMetr M) such that

       A6: x1 in P and

       A7: (( dist x2) . x1) = ( lower_bound (( dist x2) .: P)) by A1, Th15, Th16;

      reconsider x1 as Point of M by A5;

      take x1;

      take x2;

      ( dist (x1,x2)) = (( dist x2) . x1) by Def4

      .= ( upper_bound (( dist_min P) .: Q)) by A4, A7, Def6;

      hence thesis by A3, A6;

    end;

    theorem :: WEIERSTR:33

    for M be non empty MetrSpace holds for P,Q be Subset of ( TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1,x2 be Point of M st x1 in P & x2 in Q & ( dist (x1,x2)) = ( max_dist_max (P,Q))

    proof

      let M be non empty MetrSpace;

      let P,Q be Subset of ( TopSpaceMetr M);

      assume that

       A1: P <> {} & P is compact and

       A2: Q <> {} & Q is compact;

      consider x2 be Point of ( TopSpaceMetr M) such that

       A3: x2 in Q and

       A4: (( dist_max P) . x2) = ( upper_bound (( dist_max P) .: Q)) by A1, A2, Th14, Th24;

      

       A5: ( TopSpaceMetr M) = TopStruct (# the carrier of M, ( Family_open_set M) #) by PCOMPS_1:def 5;

      then

      reconsider x2 as Point of M;

      consider x1 be Point of ( TopSpaceMetr M) such that

       A6: x1 in P and

       A7: (( dist x2) . x1) = ( upper_bound (( dist x2) .: P)) by A1, Th14, Th16;

      reconsider x1 as Point of M by A5;

      take x1;

      take x2;

      ( dist (x1,x2)) = (( dist x2) . x1) by Def4

      .= ( upper_bound (( dist_max P) .: Q)) by A4, A7, Def5;

      hence thesis by A3, A6;

    end;

    theorem :: WEIERSTR:34

    for M be non empty MetrSpace holds for P,Q be Subset of ( TopSpaceMetr M) st P is compact & Q is compact holds for x1,x2 be Point of M st x1 in P & x2 in Q holds ( min_dist_min (P,Q)) <= ( dist (x1,x2)) & ( dist (x1,x2)) <= ( max_dist_max (P,Q))

    proof

      let M be non empty MetrSpace;

      let P,Q be Subset of ( TopSpaceMetr M);

      assume that

       A1: P is compact and

       A2: Q is compact;

      let x1,x2 be Point of M;

      assume that

       A3: x1 in P and

       A4: x2 in Q;

      ( dist_max P) is continuous by A1, A3, Th24;

      then ( [#] (( dist_max P) .: Q)) is real-bounded by A2, Th8, Th11;

      then

       A5: ( [#] (( dist_max P) .: Q)) is bounded_above;

      x2 in the carrier of M;

      then x2 in the carrier of ( TopSpaceMetr M) by TOPMETR: 12;

      then (( dist_min P) . x2) in the carrier of R^1 by FUNCT_2: 5;

      then

      consider z be Real such that

       A6: z = (( dist_min P) . x2);

      ( dist_min P) is continuous by A1, A3, Th27;

      then ( [#] (( dist_min P) .: Q)) is real-bounded by A2, Th8, Th11;

      then

       A7: ( [#] (( dist_min P) .: Q)) is bounded_below;

      ( dom ( dist_min P)) = the carrier of ( TopSpaceMetr M) by FUNCT_2:def 1;

      then z in ( [#] (( dist_min P) .: Q)) by A4, A6, FUNCT_1:def 6;

      then

       A8: ( lower_bound (( dist_min P) .: Q)) <= z by A7, SEQ_4:def 2;

      x2 in the carrier of M;

      then x2 in the carrier of ( TopSpaceMetr M) by TOPMETR: 12;

      then (( dist_max P) . x2) in the carrier of R^1 by FUNCT_2: 5;

      then

      consider y be Real such that

       A9: y = (( dist_max P) . x2);

      ( dom ( dist_max P)) = the carrier of ( TopSpaceMetr M) by FUNCT_2:def 1;

      then y in ( [#] (( dist_max P) .: Q)) by A4, A9, FUNCT_1:def 6;

      then

       A10: y <= ( upper_bound (( dist_max P) .: Q)) by A5, SEQ_4:def 1;

      

       A11: ( lower_bound (( dist x2) .: P)) = z by A6, Def6;

      

       A12: ( upper_bound (( dist x2) .: P)) = y by A9, Def5;

      ( dist (x1,x2)) <= ( upper_bound (( dist x2) .: P)) & ( lower_bound (( dist x2) .: P)) <= ( dist (x1,x2)) by A1, A3, Th19;

      hence thesis by A12, A10, A11, A8, XXREAL_0: 2;

    end;