lopban_7.miz



    begin

    definition

      let X,Y be non empty NORMSTR, x be Point of X, y be Point of Y;

      :: original: [

      redefine

      func [x,y] -> Point of [:X, Y:] ;

      coherence by ZFMISC_1: 87;

    end

    definition

      let X,Y be non empty NORMSTR, seqx be sequence of X, seqy be sequence of Y;

      :: original: <:

      redefine

      func <:seqx,seqy:> -> sequence of [:X, Y:] ;

      coherence

      proof

         <:seqx, seqy:> is Function of NAT , [:the carrier of X, the carrier of Y:];

        hence thesis;

      end;

    end

    theorem :: LOPBAN_7:1

    

     Th1: for X,Y be RealLinearSpace, T be LinearOperator of X, Y st T is bijective holds (T " ) is LinearOperator of Y, X & ( rng (T " )) = the carrier of X

    proof

      let X,Y be RealLinearSpace, T be LinearOperator of X, Y;

      assume

       A1: T is bijective;

      

       A2: ( rng T) = the carrier of Y by A1, FUNCT_2:def 3;

      

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

      (T " ) is LinearOperator of Y, X

      proof

        reconsider T1 = (T " ) as Function of Y, X by A1, A2, FUNCT_2: 25;

        

         A4: T1 is additive

        proof

          let y1,y2 be Point of Y;

          consider x1,x2 be Point of X such that

           A5: (T1 . y1) = x1 & (T1 . y2) = x2;

          

           A6: (T . x1) = y1 & (T . x2) = y2 by A5, A1, A2, FUNCT_1: 32;

          (x1 + x2) = (T1 . (T . (x1 + x2))) by A1, FUNCT_1: 32, A3

          .= (T1 . (y1 + y2)) by A6, VECTSP_1:def 20;

          hence thesis by A5;

        end;

        T1 is homogeneous

        proof

          let y1 be Point of Y, r be Real;

          set x1 = (T1 . y1);

          (r * x1) = (T1 . (T . (r * x1))) by A1, FUNCT_1: 32, A3

          .= (T1 . (r * (T . x1))) by LOPBAN_1:def 5

          .= (T1 . (r * y1)) by A1, A2, FUNCT_1: 32;

          hence thesis;

        end;

        hence thesis by A4;

      end;

      hence thesis by A1, FUNCT_1: 33, A3;

    end;

    theorem :: LOPBAN_7:2

    for X,Y be non empty LinearTopSpace, T be LinearOperator of X, Y, S be Function of Y, X st T is bijective open & S = (T " ) holds S is LinearOperator of Y, X & S is onto continuous

    proof

      let X,Y be non empty LinearTopSpace, T be LinearOperator of X, Y, S be Function of Y, X;

      assume

       A1: T is bijective open & S = (T " );

      then

       A2: (T " ) is LinearOperator of Y, X & (T " ) is one-to-one & ( rng (T " )) = the carrier of X by Th1;

      

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

      S is continuous

      proof

        now

          let A be Subset of X;

          assume

           A4: A is open;

          (S " A) = ((S " ) .: A) by A1, FUNCT_1: 85

          .= (T .: A) by A1, FUNCT_1: 43;

          hence (S " A) is open by A4, A1, T_0TOPSP:def 2;

        end;

        hence thesis by A3, TOPS_2: 43;

      end;

      hence thesis by A2, A1;

    end;

    theorem :: LOPBAN_7:3

    

     Th3: for X,Y be RealNormSpace, f be LinearOperator of X, Y holds ( 0. Y) = (f . ( 0. X))

    proof

      let X,Y be RealNormSpace, f be LinearOperator of X, Y;

      ((f /. ( 0. X)) + ( 0. Y)) = (f /. ( 0. X)) by RLVECT_1: 4

      .= (f /. (( 0. X) + ( 0. X))) by RLVECT_1: 4

      .= ((f /. ( 0. X)) + (f /. ( 0. X))) by VECTSP_1:def 20;

      hence thesis by RLVECT_1: 8;

    end;

    theorem :: LOPBAN_7:4

    

     Th4: for X,Y be RealNormSpace, f be LinearOperator of X, Y, x be Point of X holds f is_continuous_in x iff f is_continuous_in ( 0. X)

    proof

      let X,Y be RealNormSpace, f be LinearOperator of X, Y, x be Point of X;

      

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

      

       A2: ( 0. Y) = (f /. ( 0. X)) by Th3;

      hereby

        assume

         A3: f is_continuous_in x;

        now

          let r be Real;

          assume 0 < r;

          then

          consider s be Real such that

           A4: 0 < s & for x1 be Point of X st x1 in ( dom f) & ||.(x1 - x).|| < s holds ||.((f /. x1) - (f /. x)).|| < r by A3, NFCONT_1: 7;

          take s;

          thus 0 < s by A4;

          let x1 be Point of X;

          assume

           A5: x1 in ( dom f) & ||.(x1 - ( 0. X)).|| < s;

          set y1 = (x1 + x);

          

           A6: (y1 - x) = (x1 + (x - x)) by RLVECT_1: 28

          .= (x1 + ( 0. X)) by RLVECT_1: 15

          .= x1 by RLVECT_1: 4;

          then

           A7: ||.(y1 - x).|| < s by A5, RLVECT_1: 13;

          ((f /. y1) - (f /. x)) = ((f . y1) + (( - 1) * (f . x))) by RLVECT_1: 16

          .= ((f . y1) + (f . (( - 1) * x))) by LOPBAN_1:def 5

          .= (f . (y1 + (( - 1) * x))) by VECTSP_1:def 20

          .= (f . (y1 - x)) by RLVECT_1: 16

          .= ((f /. x1) - (f /. ( 0. X))) by A6, A2, RLVECT_1: 13;

          hence ||.((f /. x1) - (f /. ( 0. X))).|| < r by A7, A4, A1;

        end;

        hence f is_continuous_in ( 0. X) by A1, NFCONT_1: 7;

      end;

      assume

       A8: f is_continuous_in ( 0. X);

      now

        let r be Real;

        assume 0 < r;

        then

        consider s be Real such that

         A9: 0 < s & for x1 be Point of X st x1 in ( dom f) & ||.(x1 - ( 0. X)).|| < s holds ||.((f /. x1) - (f /. ( 0. X))).|| < r by A8, NFCONT_1: 7;

        take s;

        thus 0 < s by A9;

        thus for x1 be Point of X st x1 in ( dom f) & ||.(x1 - x).|| < s holds ||.((f /. x1) - (f /. x)).|| < r

        proof

          let x1 be Point of X;

          assume

           A10: x1 in ( dom f) & ||.(x1 - x).|| < s;

          set y1 = (x1 - x);

          

           A11: ||.(y1 - ( 0. X)).|| < s by A10, RLVECT_1: 13;

          ((f /. y1) - (f /. ( 0. X))) = (f . y1) by A2, RLVECT_1: 13

          .= (f . (x1 + (( - 1) * x))) by RLVECT_1: 16

          .= ((f . x1) + (f . (( - 1) * x))) by VECTSP_1:def 20

          .= ((f . x1) + (( - 1) * (f . x))) by LOPBAN_1:def 5

          .= ((f . x1) - (f . x)) by RLVECT_1: 16;

          hence ||.((f /. x1) - (f /. x)).|| < r by A11, A9, A1;

        end;

      end;

      hence f is_continuous_in x by A1, NFCONT_1: 7;

    end;

    theorem :: LOPBAN_7:5

    

     Th5: for X,Y be RealNormSpace, f be LinearOperator of X, Y holds f is_continuous_on the carrier of X iff f is_continuous_in ( 0. X)

    proof

      let X,Y be RealNormSpace, f be LinearOperator of X, Y;

      

       A1: (f | the carrier of X) = f;

      

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

      now

        assume

         A3: f is_continuous_in ( 0. X);

        for x be Point of X st x in the carrier of X holds (f | the carrier of X) is_continuous_in x by A3, Th4;

        hence f is_continuous_on the carrier of X by A2, NFCONT_1:def 7;

      end;

      hence thesis by A1, NFCONT_1:def 7;

    end;

    theorem :: LOPBAN_7:6

    

     Th6: for X,Y be RealNormSpace, f be LinearOperator of X, Y holds f is Lipschitzian iff f is_continuous_on the carrier of X

    proof

      let X,Y be RealNormSpace, f be LinearOperator of X, Y;

      hereby

        assume

         A1: f is Lipschitzian;

        

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

        consider K be Real such that

         A3: 0 <= K & for x be VECTOR of X holds ||.(f . x).|| <= (K * ||.x.||) by A1;

        now

          let x,y be Point of X;

          assume x in the carrier of X & y in the carrier of X;

          ((f /. x) - (f /. y)) = ((f . x) + (( - 1) * (f . y))) by RLVECT_1: 16;

          then ((f /. x) - (f /. y)) = ((f . x) + (f . (( - 1) * y))) by LOPBAN_1:def 5;

          then ((f /. x) - (f /. y)) = (f . (x + (( - 1) * y))) by VECTSP_1:def 20;

          then

           A4: ((f /. x) - (f /. y)) = (f . (x + ( - y))) by RLVECT_1: 16;

           ||.((f /. x) - (f /. y)).|| <= ((K * ||.(x - y).||) + ||.(x - y).||) by A3, A4, XREAL_1: 38;

          hence ||.((f /. x) - (f /. y)).|| <= ((K + 1) * ||.(x - y).||);

        end;

        hence f is_continuous_on the carrier of X by NFCONT_1: 45, A2, A3, NFCONT_1:def 9;

      end;

      assume

       A5: f is_continuous_on the carrier of X;

      

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

      (f | the carrier of X) = f;

      then f is_continuous_in ( 0. X) by A5, NFCONT_1:def 7;

      then

      consider s be Real such that

       A7: 0 < s & for x1 be Point of X st x1 in ( dom f) & ||.(x1 - ( 0. X)).|| < s holds ||.((f /. x1) - (f /. ( 0. X))).|| < 1 by NFCONT_1: 7;

      set r1 = (2 / s);

      now

        let x1 be VECTOR of X;

        

         A8: ( 0. Y) = (f /. ( 0. X)) by Th3;

        per cases ;

          suppose x1 = ( 0. X);

          hence ||.(f . x1).|| <= (r1 * ||.x1.||) by A7, A8;

        end;

          suppose

           A9: x1 <> ( 0. X);

          then

           A10: ||.x1.|| <> 0 by NORMSP_0:def 5;

          set r3 = ((s / 2) / ||.x1.||);

           0 < (s / 2) by A7, XREAL_1: 215;

          then

           A11: 0 < r3 by A10, XREAL_1: 139;

          set x2 = (r3 * x1);

          

           A12: (1 / r3) = ( ||.x1.|| / (s / 2)) by XCMPLX_1: 57

          .= ( ||.x1.|| * (2 / s)) by XCMPLX_1: 79;

           ||.x2.|| = ( |.r3.| * ||.x1.||) by NORMSP_1:def 1

          .= (r3 * ||.x1.||) by A7, ABSVALUE:def 1

          .= (s / 2) by A9, NORMSP_0:def 5, XCMPLX_1: 87;

          then ||.x2.|| < s by A7, XREAL_1: 216;

          then ||.(x2 - ( 0. X)).|| < s by RLVECT_1: 13;

          then

           A13: ||.((f /. x2) - (f /. ( 0. X))).|| < 1 by A6, A7;

           ||.(f /. x2).|| = ||.(r3 * (f . x1)).|| by LOPBAN_1:def 5

          .= ( |.r3.| * ||.(f . x1).||) by NORMSP_1:def 1

          .= (r3 * ||.(f . x1).||) by A7, ABSVALUE:def 1;

          then (r3 * ||.(f . x1).||) < 1 by A13, A8, RLVECT_1: 13;

          hence ||.(f . x1).|| <= (r1 * ||.x1.||) by A12, A11, XREAL_1: 81;

        end;

      end;

      hence f is Lipschitzian by A7;

    end;

    theorem :: LOPBAN_7:7

    

     Th7: for X,Y be RealBanachSpace, T be Lipschitzian LinearOperator of X, Y st T is bijective holds (T " ) is Lipschitzian LinearOperator of Y, X

    proof

      let X,Y be RealBanachSpace, T be Lipschitzian LinearOperator of X, Y;

      assume

       A1: T is bijective;

      

       A2: the carrier of ( LinearTopSpaceNorm X) = the carrier of X & the carrier of ( LinearTopSpaceNorm Y) = the carrier of Y by NORMSP_2:def 4;

      then

      reconsider S = T as Function of ( LinearTopSpaceNorm X), ( LinearTopSpaceNorm Y);

      reconsider T2 = (T " ) as LinearOperator of Y, X by Th1, A1;

      reconsider T3 = T2 as Function of ( LinearTopSpaceNorm Y), ( LinearTopSpaceNorm X) by A2;

      

       A3: T3 is continuous

      proof

        

         A4: ( [#] ( LinearTopSpaceNorm Y)) <> {} & ( [#] ( LinearTopSpaceNorm X)) <> {} ;

        now

          let A be Subset of ( LinearTopSpaceNorm X);

          assume

           A5: A is open;

          (T3 " A) = ((T3 " ) .: A) by A1, FUNCT_1: 85

          .= (S .: A) by A1, FUNCT_1: 43;

          hence (T3 " A) is open by A5, A2, A1, LOPBAN_6: 16, T_0TOPSP:def 2;

        end;

        hence thesis by A4, TOPS_2: 43;

      end;

      

       A6: ( dom T2) = the carrier of Y by FUNCT_2:def 1;

      now

        let x be Point of Y;

        assume x in the carrier of Y;

        reconsider xt = x as Point of ( LinearTopSpaceNorm Y) by NORMSP_2:def 4;

        

         A7: T3 is_continuous_at xt by A3, TMAP_1: 44;

        reconsider x1 = x as Point of ( TopSpaceNorm Y);

        reconsider T4 = T2 as Function of ( TopSpaceNorm Y), ( TopSpaceNorm X);

        T4 is_continuous_at x1 by A7, NORMSP_2: 35;

        hence (T2 | the carrier of Y) is_continuous_in x by NORMSP_2: 18;

      end;

      hence thesis by Th6, A6, NFCONT_1:def 7;

    end;

    theorem :: LOPBAN_7:8

    

     Th8: for X,Y be RealNormSpace, seqx be sequence of X, seqy be sequence of Y, x be Point of X, y be Point of Y holds (seqx is convergent & ( lim seqx) = x & seqy is convergent & ( lim seqy) = y) iff <:seqx, seqy:> is convergent & ( lim <:seqx, seqy:>) = [x, y]

    proof

      let X,Y be RealNormSpace, seqx be sequence of X, seqy be sequence of Y, x be Point of X, y be Point of Y;

      set seq = <:seqx, seqy:>;

      set v = [x, y];

      hereby

        assume

         A1: seqx is convergent & ( lim seqx) = x & seqy is convergent & ( lim seqy) = y;

        

         A2: for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.((seq . n) - v).|| < r

        proof

          let r1 be Real;

          assume

           A3: 0 < r1;

          set r = (r1 / 2);

          

           A4: 0 < r & r < r1 by A3, XREAL_1: 215, XREAL_1: 216;

          set r2 = (r / 2);

          

           A5: 0 < r2 & r2 < r by A4, XREAL_1: 215, XREAL_1: 216;

          then

          consider m1 be Nat such that

           A6: for n be Nat st m1 <= n holds ||.((seqx . n) - x).|| < r2 by A1, NORMSP_1:def 7;

          consider m2 be Nat such that

           A7: for n be Nat st m2 <= n holds ||.((seqy . n) - y).|| < r2 by A1, A5, NORMSP_1:def 7;

          reconsider m = ( max (m1,m2)) as Nat by TARSKI: 1;

          take m;

          let n be Nat;

          assume

           A8: m <= n;

          m1 <= m by XXREAL_0: 25;

          then

           A9: m1 <= n by A8, XXREAL_0: 2;

          m2 <= m by XXREAL_0: 25;

          then

           A10: m2 <= n by A8, XXREAL_0: 2;

          n in NAT by ORDINAL1:def 12;

          then

           A11: [(seqx . n), (seqy . n)] = (seq . n) by FUNCT_3: 59;

          

           A12: ( - v) = [( - x), ( - y)] by PRVECT_3: 18;

          ((seq . n) - v) = [((seqx . n) - x), ((seqy . n) - y)] by A11, A12, PRVECT_3: 18;

          then

          consider w be Element of ( REAL 2) such that

           A13: w = <* ||.((seqx . n) - x).||, ||.((seqy . n) - y).||*> & ||.((seq . n) - v).|| = |.w.| by PRVECT_3: 18;

          now

            let i be Element of NAT ;

            assume 1 <= i & i <= 2;

            then

             A14: i in ( Seg 2) by FINSEQ_1: 1;

            per cases by A14, FINSEQ_1: 2, TARSKI:def 2;

              suppose

               A15: i = 1;

              

               A16: (( proj (i,2)) . w) = (w . 1) by A15, PDIFF_1:def 1

              .= ||.((seqx . n) - x).|| by A13, FINSEQ_1: 44;

               |.(( proj (i,2)) . w).| = ||.((seqx . n) - x).|| by ABSVALUE:def 1, A16;

              hence |.(( proj (i,2)) . w).| <= r2 by A9, A6;

            end;

              suppose i = 2;

              

              then

               A17: (( proj (i,2)) . w) = (w . 2) by PDIFF_1:def 1

              .= ||.((seqy . n) - y).|| by A13, FINSEQ_1: 44;

               |.(( proj (i,2)) . w).| = ||.((seqy . n) - y).|| by ABSVALUE:def 1, A17;

              hence |.(( proj (i,2)) . w).| <= r2 by A10, A7;

            end;

          end;

          then |.w.| <= (2 * r2) by PDIFF_8: 17;

          hence ||.((seq . n) - v).|| < r1 by A13, A4, XXREAL_0: 2;

        end;

        hence seq is convergent;

        hence ( lim seq) = [x, y] by A2, NORMSP_1:def 7;

      end;

      assume

       A18: seq is convergent & ( lim seq) = [x, y];

      

       A19: for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.((seqx . n) - x).|| < r & ||.((seqy . n) - y).|| < r

      proof

        let r be Real;

        assume 0 < r;

        then

        consider m be Nat such that

         A20: for n be Nat st m <= n holds ||.((seq . n) - v).|| < r by A18, NORMSP_1:def 7;

        take m;

        let n be Nat;

        assume m <= n;

        then

         A21: ||.((seq . n) - v).|| < r by A20;

        n in NAT by ORDINAL1:def 12;

        then

         A22: [(seqx . n), (seqy . n)] = (seq . n) by FUNCT_3: 59;

        

         A23: ( - v) = [( - x), ( - y)] by PRVECT_3: 18;

        ((seq . n) - v) = [((seqx . n) - x), ((seqy . n) - y)] by A22, A23, PRVECT_3: 18;

        then

        consider w be Element of ( REAL 2) such that

         A24: w = <* ||.((seqx . n) - x).||, ||.((seqy . n) - y).||*> & ||.((seq . n) - v).|| = |.w.| by PRVECT_3: 18;

        (( proj (1,2)) . w) = (w . 1) by PDIFF_1:def 1

        .= ||.((seqx . n) - x).|| by A24, FINSEQ_1: 44;

        then |. ||.((seqx . n) - x).||.| <= |.w.| by PDIFF_8: 5;

        then ||.((seqx . n) - x).|| <= |.w.| by ABSVALUE:def 1;

        hence ||.((seqx . n) - x).|| < r by A24, A21, XXREAL_0: 2;

        (( proj (2,2)) . w) = (w . 2) by PDIFF_1:def 1

        .= ||.((seqy . n) - y).|| by A24, FINSEQ_1: 44;

        then |. ||.((seqy . n) - y).||.| <= |.w.| by PDIFF_8: 5;

        then ||.((seqy . n) - y).|| <= |.w.| by ABSVALUE:def 1;

        hence ||.((seqy . n) - y).|| < r by A24, A21, XXREAL_0: 2;

      end;

       A25:

      now

        let r be Real;

        assume 0 < r;

        then

        consider m be Nat such that

         A26: for n be Nat st m <= n holds ||.((seqx . n) - x).|| < r & ||.((seqy . n) - y).|| < r by A19;

        take m;

        thus for n be Nat st m <= n holds ||.((seqx . n) - x).|| < r by A26;

      end;

      hence seqx is convergent;

      hence ( lim seqx) = x by A25, NORMSP_1:def 7;

       A27:

      now

        let r be Real;

        assume 0 < r;

        then

        consider m be Nat such that

         A28: for n be Nat st m <= n holds ||.((seqx . n) - x).|| < r & ||.((seqy . n) - y).|| < r by A19;

        take m;

        thus for n be Nat st m <= n holds ||.((seqy . n) - y).|| < r by A28;

      end;

      hence seqy is convergent;

      hence ( lim seqy) = y by A27, NORMSP_1:def 7;

    end;

    definition

      let X,Y be RealNormSpace;

      let T be PartFunc of X, Y;

      :: LOPBAN_7:def1

      func graph (T) -> Subset of [:X, Y:] equals T;

      correctness ;

    end

    registration

      let X,Y be RealNormSpace;

      let T be non empty PartFunc of X, Y;

      cluster ( graph T) -> non empty;

      correctness ;

    end

    registration

      let X,Y be RealNormSpace, T be LinearOperator of X, Y;

      cluster ( graph T) -> linearly-closed;

      correctness

      proof

        set V = [:X, Y:];

        set W = ( graph T);

        hereby

          let v,u be VECTOR of V such that

           A1: v in W and

           A2: u in W;

          consider x1,y1 be object such that

           A3: v = [x1, y1] by RELAT_1:def 1;

          

           A4: x1 in ( dom T) & y1 = (T . x1) by FUNCT_1: 1, A3, A1;

          reconsider x1 as VECTOR of X by A3, ZFMISC_1: 87;

          reconsider y1 as VECTOR of Y by A3, ZFMISC_1: 87;

          consider x2,y2 be object such that

           A5: u = [x2, y2] by RELAT_1:def 1;

          reconsider x2 as VECTOR of X by A5, ZFMISC_1: 87;

          reconsider y2 as VECTOR of Y by A5, ZFMISC_1: 87;

          (x1 + x2) in the carrier of X;

          then

           A6: (x1 + x2) in ( dom T) by FUNCT_2:def 1;

          

           A7: (y1 + y2) = ((T . x1) + (T . x2)) by A4, FUNCT_1: 1, A5, A2

          .= (T . (x1 + x2)) by VECTSP_1:def 20;

           [(x1 + x2), (y1 + y2)] = (v + u) by PRVECT_3: 18, A3, A5;

          hence (v + u) in W by A7, A6, FUNCT_1: 1;

        end;

        let a be Real;

        let v be VECTOR of V;

        assume

         A8: v in W;

        consider x,y be object such that

         A9: v = [x, y] by RELAT_1:def 1;

        reconsider x as VECTOR of X by A9, ZFMISC_1: 87;

        reconsider y as VECTOR of Y by A9, ZFMISC_1: 87;

        (a * x) in the carrier of X;

        then

         A10: (a * x) in ( dom T) by FUNCT_2:def 1;

        

         A11: (a * y) = (a * (T . x)) by FUNCT_1: 1, A9, A8

        .= (T . (a * x)) by LOPBAN_1:def 5;

         [(a * x), (a * y)] = (a * v) by PRVECT_3: 18, A9;

        hence (a * v) in W by A11, A10, FUNCT_1: 1;

      end;

    end

    definition

      let X,Y be RealNormSpace;

      let T be LinearOperator of X, Y;

      :: LOPBAN_7:def2

      func graphNrm (T) -> Function of ( graph T), REAL equals (the normF of [:X, Y:] | ( graph T));

      correctness ;

    end

    definition

      let X,Y be RealNormSpace;

      let T be PartFunc of X, Y;

      :: LOPBAN_7:def3

      attr T is closed means ( graph T) is closed;

      correctness ;

    end

    definition

      let X,Y be RealNormSpace, T be LinearOperator of X, Y;

      :: LOPBAN_7:def4

      func graphNSP (T) -> non empty NORMSTR equals NORMSTR (# ( graph T), ( Zero_ (( graph T), [:X, Y:])), ( Add_ (( graph T), [:X, Y:])), ( Mult_ (( graph T), [:X, Y:])), ( graphNrm T) #);

      correctness ;

    end

    registration

      let X,Y be RealNormSpace, T be LinearOperator of X, Y;

      cluster ( graphNSP T) -> Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital;

      coherence

      proof

         the RLSStruct of ( graphNSP T) is RealLinearSpace by RSSPACE: 11;

        hence thesis by RSSPACE3: 2;

      end;

    end

    theorem :: LOPBAN_7:9

    

     Th9: for X,Y be RealNormSpace, T be LinearOperator of X, Y holds ( graphNSP T) is Subspace of [:X, Y:]

    proof

      let X,Y be RealNormSpace, T be LinearOperator of X, Y;

      set l = ( graphNSP T);

      reconsider W = the RLSStruct of l as Subspace of [:X, Y:] by RSSPACE: 11;

      

       A1: ( 0. l) = ( 0. W)

      .= ( 0. [:X, Y:]) by RLSUB_1:def 2;

      

       A2: the addF of l = (the addF of [:X, Y:] || the carrier of W) by RLSUB_1:def 2

      .= (the addF of [:X, Y:] || the carrier of l);

      the Mult of l = (the Mult of [:X, Y:] | [: REAL , the carrier of W:]) by RLSUB_1:def 2

      .= (the Mult of [:X, Y:] | [: REAL , the carrier of l:]);

      hence l is Subspace of [:X, Y:] by A1, A2, RLSUB_1:def 2;

    end;

    

     Lm1: for X,Y be RealNormSpace, T be LinearOperator of X, Y, x,y be Point of ( graphNSP T), a be Real holds ( ||.x.|| = 0 iff x = ( 0. ( graphNSP T))) & 0 <= ||.x.|| & ||.(x + y).|| <= ( ||.x.|| + ||.y.||) & ||.(a * x).|| = ( |.a.| * ||.x.||)

    proof

      let X,Y be RealNormSpace, T be LinearOperator of X, Y, x,y be Point of ( graphNSP T), a be Real;

      x in ( graph T) & y in ( graph T);

      then

      reconsider x1 = x, y1 = y as Point of [:X, Y:];

      set W = ( graphNSP T);

      set V = [:X, Y:];

      

       A1: W is Subspace of V by Th9;

      

       A2: ||.x.|| = ||.x1.|| by FUNCT_1: 49;

      

       A3: ||.y.|| = ||.y1.|| by FUNCT_1: 49;

      (x + y) = (x1 + y1) by A1, RLSUB_1: 13;

      then

       A4: ||.(x + y).|| = ||.(x1 + y1).|| by FUNCT_1: 49;

      (a * x) = (a * x1) by A1, RLSUB_1: 14;

      then

       A5: ||.(a * x).|| = ||.(a * x1).|| by FUNCT_1: 49;

      

       A6: ( 0. [:X, Y:]) = ( 0. ( graphNSP T)) by A1, RLSUB_1: 11;

       ||.x.|| = 0 iff ||.x1.|| = 0 by FUNCT_1: 49;

      hence ||.x.|| = 0 iff x = ( 0. ( graphNSP T)) by A6, NORMSP_0:def 5;

      thus 0 <= ||.x.|| by A2;

      thus ||.(x + y).|| <= ( ||.x.|| + ||.y.||) by A2, A3, A4, NORMSP_1:def 1;

      thus thesis by A2, A5, NORMSP_1:def 1;

    end;

    registration

      let X,Y be RealNormSpace, T be LinearOperator of X, Y;

      cluster ( graphNSP T) -> reflexive discerning RealNormSpace-like;

      coherence by Lm1;

    end

    theorem :: LOPBAN_7:10

    

     Th10: for X be RealNormSpace, Y be RealBanachSpace, X0 be Subset of Y st X is Subspace of Y & the carrier of X = X0 & the normF of X = (the normF of Y | the carrier of X) & X0 is closed holds X is complete

    proof

      let X be RealNormSpace, Y be RealBanachSpace, X0 be Subset of Y;

      assume

       A1: X is Subspace of Y & the carrier of X = X0 & the normF of X = (the normF of Y | the carrier of X) & X0 is closed;

      now

        let seq be sequence of X;

        assume

         A2: seq is Cauchy_sequence_by_Norm;

        ( rng seq) c= the carrier of Y by A1, XBOOLE_1: 1;

        then

        reconsider yseq = seq as sequence of Y by FUNCT_2: 6;

        for r be Real st r > 0 holds ex k be Nat st for n,m be Nat st n >= k & m >= k holds ||.((yseq . n) - (yseq . m)).|| < r

        proof

          let r be Real;

          assume r > 0 ;

          then

          consider k be Nat such that

           A3: for n,m be Nat st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r by RSSPACE3: 8, A2;

          take k;

          now

            let n,m be Nat;

            assume

             A4: n >= k & m >= k;

            ((seq . n) - (seq . m)) = ((yseq . n) - (yseq . m)) by A1, RLSUB_1: 16;

            then ||.((seq . n) - (seq . m)).|| = ||.((yseq . n) - (yseq . m)).|| by FUNCT_1: 49, A1;

            hence ||.((yseq . n) - (yseq . m)).|| < r by A4, A3;

          end;

          hence thesis;

        end;

        then

         A5: yseq is convergent by LOPBAN_1:def 15, RSSPACE3: 8;

        ( rng yseq) = ( rng seq);

        then

        reconsider lyseq = ( lim yseq) as Point of X by A1, A5, NFCONT_1:def 3;

        for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.((seq . n) - lyseq).|| < r

        proof

          let r be Real;

          assume 0 < r;

          then

          consider m be Nat such that

           A6: for n be Nat st m <= n holds ||.((yseq . n) - ( lim yseq)).|| < r by A5, NORMSP_1:def 7;

          take m;

          now

            let n be Nat;

            assume

             A7: m <= n;

            ((yseq . n) - ( lim yseq)) = ((seq . n) - lyseq) by A1, RLSUB_1: 16;

            then ||.((yseq . n) - ( lim yseq)).|| = ||.((seq . n) - lyseq).|| by FUNCT_1: 49, A1;

            hence ||.((seq . n) - lyseq).|| < r by A7, A6;

          end;

          hence thesis;

        end;

        hence seq is convergent;

      end;

      hence thesis;

    end;

    theorem :: LOPBAN_7:11

    

     Th11: for X,Y be RealBanachSpace, T be LinearOperator of X, Y st T is closed holds ( graphNSP T) is complete

    proof

      let X,Y be RealBanachSpace, T be LinearOperator of X, Y;

      ( graphNSP T) is Subspace of [:X, Y:] by Th9;

      hence thesis by Th10;

    end;

    theorem :: LOPBAN_7:12

    

     Th12: for X,Y be RealNormSpace, T be non empty PartFunc of X, Y holds T is closed iff for seq be sequence of X st ( rng seq) c= ( dom T) & seq is convergent & (T /* seq) is convergent holds ( lim seq) in ( dom T) & ( lim (T /* seq)) = (T . ( lim seq))

    proof

      let X,Y be RealNormSpace, T be non empty PartFunc of X, Y;

      hereby

        assume

         A1: T is closed;

        thus for seq be sequence of X st ( rng seq) c= ( dom T) & seq is convergent & (T /* seq) is convergent holds ( lim seq) in ( dom T) & ( lim (T /* seq)) = (T . ( lim seq))

        proof

          let seq be sequence of X;

          assume

           A2: ( rng seq) c= ( dom T) & seq is convergent & (T /* seq) is convergent;

          set s1 = <:seq, (T /* seq):>;

          

           A3: ( rng s1) c= ( graph T)

          proof

            let y be object;

            assume y in ( rng s1);

            then

            consider i be object such that

             A4: i in NAT & (s1 . i) = y by FUNCT_2: 11;

            

             A5: ((T /* seq) . i) = (T . (seq . i)) by A4, A2, FUNCT_2: 108;

            (seq . i) in ( rng seq) by A4, FUNCT_2: 4;

            then [(seq . i), ((T /* seq) . i)] in T by A5, FUNCT_1:def 2, A2;

            hence y in ( graph T) by A4, FUNCT_3: 59;

          end;

          ( lim seq) = ( lim seq) & ( lim (T /* seq)) = ( lim (T /* seq));

          then s1 is convergent & ( lim s1) = [( lim seq), ( lim (T /* seq))] by Th8, A2;

          then [( lim seq), ( lim (T /* seq))] in ( graph T) by A1, NFCONT_1:def 3, A3;

          hence ( lim seq) in ( dom T) & ( lim (T /* seq)) = (T . ( lim seq)) by FUNCT_1: 1;

        end;

      end;

      assume

       A6: for seq be sequence of X st ( rng seq) c= ( dom T) & seq is convergent & (T /* seq) is convergent holds ( lim seq) in ( dom T) & ( lim (T /* seq)) = (T . ( lim seq));

      for s1 be sequence of [:X, Y:] st ( rng s1) c= ( graph T) & s1 is convergent holds ( lim s1) in ( graph T)

      proof

        let s1 be sequence of [:X, Y:];

        assume

         A7: ( rng s1) c= ( graph T) & s1 is convergent;

        defpred Q0[ set, set] means [$2, (T . $2)] = (s1 . $1);

        

         A8: for i be Element of NAT holds ex x be Element of the carrier of X st Q0[i, x]

        proof

          let i be Element of NAT ;

          

           A9: (s1 . i) in ( rng s1) by FUNCT_2: 4;

          consider x be Point of X, y be Point of Y such that

           A10: (s1 . i) = [x, y] by PRVECT_3: 18;

          take x;

          thus thesis by A10, FUNCT_1: 1, A9, A7;

        end;

        consider seq be sequence of X such that

         A11: for x be Element of NAT holds Q0[x, (seq . x)] from FUNCT_2:sch 3( A8);

         A12:

        now

          let y be object;

          assume y in ( rng seq);

          then

          consider i be object such that

           A13: i in ( dom seq) & y = (seq . i) by FUNCT_1:def 3;

          

           A14: [(seq . i), (T . (seq . i))] = (s1 . i) by A13, A11;

          (s1 . i) in ( rng s1) by A13, FUNCT_2: 4;

          hence y in ( dom T) by A13, FUNCT_1: 1, A14, A7;

        end;

        then

         A15: ( rng seq) c= ( dom T);

        consider x be Point of X, y be Point of Y such that

         A16: ( lim s1) = [x, y] by PRVECT_3: 18;

        s1 = <:seq, (T /* seq):>

        proof

          let n be Element of NAT ;

          ((T /* seq) . n) = (T . (seq . n)) by A12, TARSKI:def 3, FUNCT_2: 108;

          

          hence (s1 . n) = [(seq . n), ((T /* seq) . n)] by A11

          .= ( <:seq, (T /* seq):> . n) by FUNCT_3: 59;

        end;

        then

         A17: seq is convergent & ( lim seq) = x & (T /* seq) is convergent & ( lim (T /* seq)) = y by A16, Th8, A7;

        ( lim seq) in ( dom T) & ( lim (T /* seq)) = (T . ( lim seq)) by A15, A6, A17;

        hence ( lim s1) in ( graph T) by A16, A17, FUNCT_1: 1;

      end;

      hence thesis by NFCONT_1:def 3;

    end;

    theorem :: LOPBAN_7:13

    for X,Y be RealNormSpace, T be non empty PartFunc of X, Y, T0 be LinearOperator of X, Y st T0 is Lipschitzian & ( dom T) is closed & T = T0 holds T is closed

    proof

      let X,Y be RealNormSpace, T be non empty PartFunc of X, Y, T0 be LinearOperator of X, Y;

      assume

       A1: T0 is Lipschitzian & ( dom T) is closed & T = T0;

      then

       A2: T is_continuous_in ( 0. X) by Th5, Th6;

      for seq be sequence of X st ( rng seq) c= ( dom T) & seq is convergent & (T /* seq) is convergent holds ( lim seq) in ( dom T) & ( lim (T /* seq)) = (T . ( lim seq))

      proof

        let seq be sequence of X;

        assume

         A3: ( rng seq) c= ( dom T) & seq is convergent & (T /* seq) is convergent;

        

         A4: T is_continuous_in ( lim seq) by A1, A2, Th4;

        (T /. ( lim seq)) = (T . ( lim seq)) by A1, A3, NFCONT_1:def 3, PARTFUN1:def 6;

        hence thesis by A3, A4, NFCONT_1:def 5;

      end;

      hence thesis by Th12;

    end;

    theorem :: LOPBAN_7:14

    for X,Y be RealNormSpace, T be non empty PartFunc of X, Y, S be non empty PartFunc of Y, X st T is closed & T is one-to-one & S = (T " ) holds S is closed

    proof

      let X,Y be RealNormSpace, T be non empty PartFunc of X, Y, S be non empty PartFunc of Y, X;

      assume

       A1: T is closed & T is one-to-one & S = (T " );

      

       A2: ( rng T) = ( dom S) & ( dom T) = ( rng S) by A1, FUNCT_1: 33;

      for seq be sequence of Y st ( rng seq) c= ( dom S) & seq is convergent & (S /* seq) is convergent holds ( lim seq) in ( dom S) & ( lim (S /* seq)) = (S . ( lim seq))

      proof

        let seq be sequence of Y;

        assume

         A3: ( rng seq) c= ( dom S) & seq is convergent & (S /* seq) is convergent;

        set seq1 = (S /* seq);

        

         A4: ( rng seq1) c= ( dom T)

        proof

          let x be object;

          assume x in ( rng seq1);

          then

          consider i be object such that

           A5: i in ( dom seq1) & x = (seq1 . i) by FUNCT_1:def 3;

          reconsider i as Nat by A5;

          (S . (seq . i)) in ( rng S) by FUNCT_1: 3, A3, NFCONT_1: 5;

          hence x in ( dom T) by A5, A2, A3, FUNCT_2: 108;

        end;

        

         A6: (T /* seq1) = seq

        proof

          now

            let n be Element of NAT ;

            thus ((T /* seq1) . n) = (seq . n)

            proof

              

               A7: (seq . n) in ( rng T) by A3, NFCONT_1: 5, A2;

              ((T /* seq1) . n) = (T . (seq1 . n)) by A4, FUNCT_2: 108

              .= (T . (S . (seq . n))) by A3, FUNCT_2: 108

              .= (seq . n) by A1, A7, FUNCT_1: 35;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        ( lim seq1) in ( dom T) & ( lim (T /* seq1)) = (T . ( lim (S /* seq))) by A1, A3, A4, A6, Th12;

        hence thesis by A2, A6, FUNCT_1: 3, A1, FUNCT_1: 34;

      end;

      hence thesis by Th12;

    end;

    theorem :: LOPBAN_7:15

    

     Th15: for X,Y be RealNormSpace, x be Point of X, y be Point of Y holds ||.x.|| <= ||. [x, y].|| & ||.y.|| <= ||. [x, y].||

    proof

      let X,Y be RealNormSpace, x be Point of X, y be Point of Y;

      consider w be Element of ( REAL 2) such that

       A1: w = <* ||.x.||, ||.y.||*> & ||. [x, y].|| = |.w.| by PRVECT_3: 18;

      (( proj (1,2)) . w) = (w . 1) by PDIFF_1:def 1

      .= ||.x.|| by A1, FINSEQ_1: 44;

      then |. ||.x.||.| <= |.w.| by PDIFF_8: 5;

      hence ||.x.|| <= ||. [x, y].|| by A1, ABSVALUE:def 1;

      (( proj (2,2)) . w) = (w . 2) by PDIFF_1:def 1

      .= ||.y.|| by A1, FINSEQ_1: 44;

      then |. ||.y.||.| <= |.w.| by PDIFF_8: 5;

      hence ||.y.|| <= ||. [x, y].|| by A1, ABSVALUE:def 1;

    end;

    registration

      let X,Y be RealBanachSpace;

      cluster closed -> Lipschitzian for LinearOperator of X, Y;

      coherence

      proof

        let T be LinearOperator of X, Y;

        assume

         A1: T is closed;

        defpred Q0[ object, object] means $1 = [$2, (T . $2)];

        

         A2: for z be object st z in the carrier of ( graphNSP T) holds ex x be object st x in the carrier of X & Q0[z, x]

        proof

          let z be object;

          assume

           A3: z in the carrier of ( graphNSP T);

          then

          consider x,y be object such that

           A4: z = [x, y] by RELAT_1:def 1;

          x in ( dom T) & y = (T . x) by FUNCT_1: 1, A4, A3;

          hence thesis by A4;

        end;

        consider J be Function of ( graphNSP T), X such that

         A5: for z be object st z in the carrier of ( graphNSP T) holds Q0[z, (J . z)] from FUNCT_2:sch 1( A2);

        

         A6: ( graphNSP T) is complete by Th11, A1;

        

         A7: ( graphNSP T) is Subspace of [:X, Y:] & the normF of ( graphNSP T) = (the normF of [:X, Y:] | the carrier of ( graphNSP T)) by Th9;

        

         A8: for x be VECTOR of ( graphNSP T), r be Real holds (J . (r * x)) = (r * (J . x))

        proof

          let x be VECTOR of ( graphNSP T), r be Real;

          

           A9: x = [(J . x), (T . (J . x))] by A5;

          

           A10: (r * x) = [(J . (r * x)), (T . (J . (r * x)))] by A5;

          x in ( graph T);

          then

          reconsider x1 = x as Point of [:X, Y:];

          (r * x1) = (r * x) by A7, RLSUB_1: 14;

          then (r * x) = [(r * (J . x)), (r * (T . (J . x)))] by PRVECT_3: 18, A9;

          hence (J . (r * x)) = (r * (J . x)) by A10, XTUPLE_0: 1;

        end;

        for x,y be VECTOR of ( graphNSP T) holds (J . (x + y)) = ((J . x) + (J . y))

        proof

          let x,y be VECTOR of ( graphNSP T);

          

           A11: x = [(J . x), (T . (J . x))] by A5;

          

           A12: y = [(J . y), (T . (J . y))] by A5;

          

           A13: (x + y) = [(J . (x + y)), (T . (J . (x + y)))] by A5;

          x in ( graph T) & y in ( graph T);

          then

          reconsider x1 = x, y1 = y as Point of [:X, Y:];

          (x1 + y1) = (x + y) by A7, RLSUB_1: 13;

          then (x + y) = [((J . x) + (J . y)), ((T . (J . x)) + (T . (J . y)))] by PRVECT_3: 18, A11, A12;

          hence (J . (x + y)) = ((J . x) + (J . y)) by A13, XTUPLE_0: 1;

        end;

        then

        reconsider J as LinearOperator of ( graphNSP T), X by A8, LOPBAN_1:def 5, VECTSP_1:def 20;

        J is Lipschitzian

        proof

           A14:

          now

            let x be Point of ( graphNSP T);

            x in ( graph T);

            then

            reconsider x1 = x as Point of [:X, Y:];

            

             A15: x1 = [(J . x), (T . (J . x))] by A5;

             ||.(J . x).|| <= ||.x1.|| by A15, Th15;

            hence ||.(J . x).|| <= (1 * ||.x.||) by FUNCT_1: 49;

          end;

          take 1;

          thus thesis by A14;

        end;

        then

        reconsider J as Lipschitzian LinearOperator of ( graphNSP T), X;

        now

          let x,y be object;

          assume

           A16: x in the carrier of ( graphNSP T) & y in the carrier of ( graphNSP T) & (J . x) = (J . y);

          then

          reconsider x1 = x as Point of ( graphNSP T);

          x1 = [(J . x1), (T . (J . x1))] by A5;

          hence x = y by A5, A16;

        end;

        then

         A17: J is one-to-one by FUNCT_2: 19;

        for y be object holds y in ( rng J) iff y in the carrier of X

        proof

          let y be object;

          now

            assume

             A18: y in the carrier of X;

            then

            reconsider y1 = y as Point of X;

            y1 in ( dom T) by A18, FUNCT_2:def 1;

            then

            reconsider x = [y1, (T . y1)] as Point of ( graphNSP T) by FUNCT_1: 1;

            x = [(J . x), (T . (J . x))] by A5;

            then y1 = (J . x) by XTUPLE_0: 1;

            hence y in ( rng J) by FUNCT_2: 112;

          end;

          hence thesis;

        end;

        then J is onto by TARSKI: 2;

        then

        reconsider L = (J " ) as Lipschitzian LinearOperator of X, ( graphNSP T) by A17, Th7, A6;

        consider K be Real such that

         A19: 0 <= K & for x be VECTOR of X holds ||.(L . x).|| <= (K * ||.x.||) by LOPBAN_1:def 8;

        now

          let y be Point of X;

          y in the carrier of X;

          then y in ( dom T) by FUNCT_2:def 1;

          then

          reconsider x = [y, (T . y)] as Point of ( graphNSP T) by FUNCT_1: 1;

          

           A20: x = [(J . x), (T . (J . x))] by A5;

          

           A21: ||.(L . y).|| <= (K * ||.y.||) by A19;

          x in the carrier of ( graphNSP T);

          then

           A22: x in ( dom J) by FUNCT_2:def 1;

          

           A23: (L . y) = (L . (J . x)) by XTUPLE_0: 1, A20

          .= x by FUNCT_1: 34, A17, A22;

          reconsider x1 = x as Point of [:X, Y:];

           ||.x1.|| = ||.x.|| by FUNCT_1: 49;

          then ||.(T . y).|| <= ||.(L . y).|| by A23, Th15;

          hence ||.(T . y).|| <= (K * ||.y.||) by A21, XXREAL_0: 2;

        end;

        hence T is Lipschitzian by A19;

      end;

    end