ali2.miz



    begin

    definition

      let M be non empty MetrSpace;

      let f be Function of M, M;

      :: ALI2:def1

      attr f is contraction means

      : Def1: ex L be Real st 0 < L & L < 1 & for x,y be Point of M holds ( dist ((f . x),(f . y))) <= (L * ( dist (x,y)));

    end

    registration

      let M be non empty MetrSpace;

      cluster constant -> contraction for Function of M, M;

      coherence

      proof

        let f be Function of M, M such that

         A1: f is constant;

        take (1 / 2);

        thus 0 < (1 / 2) & (1 / 2) < 1;

        let z,y be Point of M;

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

        then (f . z) = (f . y) by A1, FUNCT_1:def 10;

        then

         A2: ( dist ((f . z),(f . y))) = 0 by METRIC_1: 1;

        ( dist (z,y)) >= 0 by METRIC_1: 5;

        hence thesis by A2;

      end;

    end

    registration

      let M be non empty MetrSpace;

      cluster constant for Function of M, M;

      existence

      proof

        (M --> the Point of M) is constant;

        hence thesis;

      end;

    end

    definition

      let M be non empty MetrSpace;

      mode Contraction of M is contraction Function of M, M;

    end

    ::$Notion-Name

    theorem :: ALI2:1

    for M be non empty MetrSpace holds for f be Contraction of M st ( TopSpaceMetr M) is compact holds ex c be Point of M st (f . c) = c & for x be Point of M st (f . x) = x holds x = c

    proof

      let M be non empty MetrSpace;

      let f be Contraction of M;

      set x0 = the Point of M;

      set a = ( dist (x0,(f . x0)));

      consider L be Real such that

       A1: 0 < L and

       A2: L < 1 and

       A3: for x,y be Point of M holds ( dist ((f . x),(f . y))) <= (L * ( dist (x,y))) by Def1;

      assume

       A4: ( TopSpaceMetr M) is compact;

      now

        deffunc F( Nat) = (L to_power ($1 + 1));

        defpred P[ set] means ex n be Nat st $1 = { x where x be Point of M : ( dist (x,(f . x))) <= (a * (L to_power n)) };

        assume a <> 0 ;

        consider F be Subset-Family of ( TopSpaceMetr M) such that

         A5: for B be Subset of ( TopSpaceMetr M) holds B in F iff P[B] from SUBSET_1:sch 3;

        defpred P[ Point of M] means ( dist ($1,(f . $1))) <= (a * (L to_power ( 0 + 1)));

        

         A6: F is closed

        proof

          let B be Subset of ( TopSpaceMetr M);

          

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

          then

          reconsider V = (B ` ) as Subset of M;

          assume B in F;

          then

          consider n be Nat such that

           A8: B = { x where x be Point of M : ( dist (x,(f . x))) <= (a * (L to_power n)) } by A5;

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

          proof

            let x be Point of M;

            assume x in V;

            then not x in B by XBOOLE_0:def 5;

            then ( dist (x,(f . x))) > (a * (L to_power n)) by A8;

            then

             A9: (( dist (x,(f . x))) - (a * (L to_power n))) > 0 by XREAL_1: 50;

            take r = ((( dist (x,(f . x))) - (a * (L to_power n))) / 2);

            thus r > 0 by A9, XREAL_1: 215;

            let z be object;

            assume

             A10: z in ( Ball (x,r));

            then

            reconsider y = z as Point of M;

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

            then (2 * ( dist (x,y))) < (2 * r) by XREAL_1: 68;

            then

             A11: (( dist (y,(f . y))) + (2 * ( dist (x,y)))) < (( dist (y,(f . y))) + (2 * r)) by XREAL_1: 6;

            (( dist (x,y)) + ( dist (y,(f . y)))) >= ( dist (x,(f . y))) by METRIC_1: 4;

            then

             A12: ((( dist (x,y)) + ( dist (y,(f . y)))) + ( dist ((f . y),(f . x)))) >= (( dist (x,(f . y))) + ( dist ((f . y),(f . x)))) by XREAL_1: 6;

            ( dist ((f . y),(f . x))) <= (L * ( dist (y,x))) & (L * ( dist (y,x))) <= ( dist (y,x)) by A2, A3, METRIC_1: 5, XREAL_1: 153;

            then ( dist ((f . y),(f . x))) <= ( dist (y,x)) by XXREAL_0: 2;

            then (( dist ((f . y),(f . x))) + ( dist (y,x))) <= (( dist (y,x)) + ( dist (y,x))) by XREAL_1: 6;

            then

             A13: (( dist (y,(f . y))) + (( dist (y,x)) + ( dist ((f . y),(f . x))))) <= (( dist (y,(f . y))) + (2 * ( dist (y,x)))) by XREAL_1: 7;

            (( dist (x,(f . y))) + ( dist ((f . y),(f . x)))) >= ( dist (x,(f . x))) by METRIC_1: 4;

            then ((( dist (y,(f . y))) + ( dist (x,y))) + ( dist ((f . y),(f . x)))) >= ( dist (x,(f . x))) by A12, XXREAL_0: 2;

            then (( dist (y,(f . y))) + (2 * ( dist (x,y)))) >= ( dist (x,(f . x))) by A13, XXREAL_0: 2;

            then (( dist (x,(f . x))) - (2 * r)) = (a * (L to_power n)) & (( dist (y,(f . y))) + (2 * r)) > ( dist (x,(f . x))) by A11, XXREAL_0: 2;

            then not ex x be Point of M st y = x & ( dist (x,(f . x))) <= (a * (L to_power n)) by XREAL_1: 19;

            then not y in B by A8;

            hence thesis by A7, SUBSET_1: 29;

          end;

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

          then (B ` ) is open by A7, PRE_TOPC:def 2;

          hence thesis by TOPS_1: 3;

        end;

        

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

        

         A15: { x where x be Point of M : P[x] } is Subset of M from DOMAIN_1:sch 7;

        F is centered

        proof

          thus F <> {} by A5, A14, A15;

          defpred P[ Nat] means { x where x be Point of M : ( dist (x,(f . x))) <= (a * (L to_power $1)) } <> {} ;

          let G be set such that

           A16: G <> {} and

           A17: G c= F and

           A18: G is finite;

          G is c=-linear

          proof

            let B,C be set;

            assume that

             A19: B in G and

             A20: C in G;

            B in F by A17, A19;

            then

            consider n be Nat such that

             A21: B = { x where x be Point of M : ( dist (x,(f . x))) <= (a * (L to_power n)) } by A5;

            C in F by A17, A20;

            then

            consider m be Nat such that

             A22: C = { x where x be Point of M : ( dist (x,(f . x))) <= (a * (L to_power m)) } by A5;

            

             A23: for n,m be Nat st n <= m holds (L to_power m) <= (L to_power n)

            proof

              let n,m be Nat such that

               A24: n <= m;

              per cases by A24, XXREAL_0: 1;

                suppose n < m;

                hence thesis by A1, A2, POWER: 40;

              end;

                suppose n = m;

                hence thesis;

              end;

            end;

            

             A25: for n,m be Nat st n <= m holds (a * (L to_power m)) <= (a * (L to_power n))

            proof

              

               A26: a >= 0 by METRIC_1: 5;

              let n,m be Nat;

              assume n <= m;

              hence thesis by A23, A26, XREAL_1: 64;

            end;

            now

              per cases ;

                case

                 A27: n <= m;

                thus C c= B

                proof

                  let y be object;

                  assume y in C;

                  then

                  consider x be Point of M such that

                   A28: y = x and

                   A29: ( dist (x,(f . x))) <= (a * (L to_power m)) by A22;

                  (a * (L to_power m)) <= (a * (L to_power n)) by A25, A27;

                  then ( dist (x,(f . x))) <= (a * (L to_power n)) by A29, XXREAL_0: 2;

                  hence thesis by A21, A28;

                end;

              end;

                case

                 A30: m <= n;

                thus B c= C

                proof

                  let y be object;

                  assume y in B;

                  then

                  consider x be Point of M such that

                   A31: y = x and

                   A32: ( dist (x,(f . x))) <= (a * (L to_power n)) by A21;

                  (a * (L to_power n)) <= (a * (L to_power m)) by A25, A30;

                  then ( dist (x,(f . x))) <= (a * (L to_power m)) by A32, XXREAL_0: 2;

                  hence thesis by A22, A31;

                end;

              end;

            end;

            hence B c= C or C c= B;

          end;

          then

          consider m be set such that

           A33: m in G and

           A34: for C be set st C in G holds m c= C by A16, A18, FINSET_1: 11;

          

           A35: m c= ( meet G) by A16, A34, SETFAM_1: 5;

          

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

          proof

            let k be Nat;

            set z = the Element of { x where x be Point of M : ( dist (x,(f . x))) <= (a * (L to_power k)) };

            

             A37: (L * (a * (L to_power k))) = (a * (L * (L to_power k)))

            .= (a * ((L to_power k) * (L to_power 1))) by POWER: 25

            .= (a * (L to_power (k + 1))) by A1, POWER: 27;

            assume { x where x be Point of M : ( dist (x,(f . x))) <= (a * (L to_power k)) } <> {} ;

            then z in { x where x be Point of M : ( dist (x,(f . x))) <= (a * (L to_power k)) };

            then

            consider y be Point of M such that y = z and

             A38: ( dist (y,(f . y))) <= (a * (L to_power k));

            

             A39: ( dist ((f . y),(f . (f . y)))) <= (L * ( dist (y,(f . y)))) by A3;

            (L * ( dist (y,(f . y)))) <= (L * (a * (L to_power k))) by A1, A38, XREAL_1: 64;

            then ( dist ((f . y),(f . (f . y)))) <= (a * (L to_power (k + 1))) by A37, A39, XXREAL_0: 2;

            then (f . y) in { x where x be Point of M : ( dist (x,(f . x))) <= (a * (L to_power (k + 1))) };

            hence thesis;

          end;

          ( dist (x0,(f . x0))) = (a * 1)

          .= (a * (L to_power 0 )) by POWER: 24;

          then x0 in { x where x be Point of M : ( dist (x,(f . x))) <= (a * (L to_power 0 )) };

          then

           A40: P[ 0 ];

          

           A41: for k be Nat holds P[k] from NAT_1:sch 2( A40, A36);

          m in F by A17, A33;

          then m <> {} by A5, A41;

          hence thesis by A35;

        end;

        then ( meet F) <> {} by A4, A6, COMPTS_1: 4;

        then

        consider c9 be Point of ( TopSpaceMetr M) such that

         A42: c9 in ( meet F) by SUBSET_1: 4;

        reconsider c = c9 as Point of M by A14;

        reconsider dc = ( dist (c,(f . c))) as Element of REAL by XREAL_0:def 1;

        set r = ( seq_const ( dist (c,(f . c))));

        consider s9 be Real_Sequence such that

         A43: for n be Nat holds (s9 . n) = F(n) from SEQ_1:sch 1;

        set s = (a (#) s9);

        ( lim s9) = 0 by A1, A2, A43, SERIES_1: 1;

        

        then

         A44: ( lim s) = (a * 0 ) by A1, A2, A43, SEQ_2: 8, SERIES_1: 1

        .= 0 ;

         A45:

        now

          let n be Nat;

          defpred P[ Point of M] means ( dist ($1,(f . $1))) <= (a * (L to_power (n + 1)));

          set B = { x where x be Point of M : P[x] };

          B is Subset of M from DOMAIN_1:sch 7;

          then B in F by A5, A14;

          then c in B by A42, SETFAM_1:def 1;

          then

           A46: ex x be Point of M st c = x & ( dist (x,(f . x))) <= (a * (L to_power (n + 1)));

          (s . n) = (a * (s9 . n)) by SEQ_1: 9

          .= (a * (L to_power (n + 1))) by A43;

          hence (r . n) <= (s . n) by A46, SEQ_1: 57;

        end;

        s is convergent by A1, A2, A43, SEQ_2: 7, SERIES_1: 1;

        then

         A47: ( lim r) <= ( lim s) by A45, SEQ_2: 18;

        (r . 0 ) = ( dist (c,(f . c))) by SEQ_1: 57;

        then ( dist (c,(f . c))) <= 0 by A44, A47, SEQ_4: 25;

        then ( dist (c,(f . c))) = 0 by METRIC_1: 5;

        hence ex c be Point of M st ( dist (c,(f . c))) = 0 ;

      end;

      then

      consider c be Point of M such that

       A48: ( dist (c,(f . c))) = 0 ;

      take c;

      thus

       A49: (f . c) = c by A48, METRIC_1: 2;

      let x be Point of M;

      assume

       A50: (f . x) = x;

      

       A51: ( dist (x,c)) >= 0 by METRIC_1: 5;

      assume x <> c;

      then ( dist (x,c)) <> 0 by METRIC_1: 2;

      then (L * ( dist (x,c))) < ( dist (x,c)) by A2, A51, XREAL_1: 157;

      hence contradiction by A3, A49, A50;

    end;