:: by Hideki Sakurai , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received August 6, 2012

:: Copyright (c) 2012-2018 Association of Mizar Users

definition

let X, Y be non empty NORMSTR ;

let x be Point of X;

let y be Point of Y;

:: original: [

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

coherence

[x,y] is Point of [:X,Y:] by ZFMISC_1:87;

end;
let x be Point of X;

let y be Point of Y;

:: original: [

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

coherence

[x,y] is Point of [:X,Y:] by ZFMISC_1:87;

definition

let X, Y be non empty NORMSTR ;

let seqx be sequence of X;

let seqy be sequence of Y;

:: original: <:

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

coherence

<:seqx,seqy:> is sequence of [:X,Y:]

end;
let seqx be sequence of X;

let seqy be sequence of Y;

:: original: <:

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

coherence

<:seqx,seqy:> is sequence of [:X,Y:]

proof end;

theorem Th1: :: LOPBAN_7:1

for X, Y being RealLinearSpace

for T being LinearOperator of X,Y st T is bijective holds

( T " is LinearOperator of Y,X & rng (T ") = the carrier of X )

for T being LinearOperator of X,Y st T is bijective holds

( T " is LinearOperator of Y,X & rng (T ") = the carrier of X )

proof end;

theorem :: LOPBAN_7:2

for X, Y being LinearTopSpace

for T being LinearOperator of X,Y

for S being Function of Y,X st T is bijective & T is open & S = T " holds

( S is LinearOperator of Y,X & S is onto & S is continuous )

for T being LinearOperator of X,Y

for S being Function of Y,X st T is bijective & T is open & S = T " holds

( S is LinearOperator of Y,X & S is onto & S is continuous )

proof end;

theorem Th4: :: LOPBAN_7:4

for X, Y being RealNormSpace

for f being LinearOperator of X,Y

for x being Point of X holds

( f is_continuous_in x iff f is_continuous_in 0. X )

for f being LinearOperator of X,Y

for x being Point of X holds

( f is_continuous_in x iff f is_continuous_in 0. X )

proof end;

theorem Th5: :: LOPBAN_7:5

for X, Y being RealNormSpace

for f being LinearOperator of X,Y holds

( f is_continuous_on the carrier of X iff f is_continuous_in 0. X )

for f being LinearOperator of X,Y holds

( f is_continuous_on the carrier of X iff f is_continuous_in 0. X )

proof end;

theorem Th6: :: LOPBAN_7:6

for X, Y being RealNormSpace

for f being LinearOperator of X,Y holds

( f is Lipschitzian iff f is_continuous_on the carrier of X )

for f being LinearOperator of X,Y holds

( f is Lipschitzian iff f is_continuous_on the carrier of X )

proof end;

:: Banach's Continuous Inverse Theorem

theorem Th7: :: LOPBAN_7:7

for X, Y being RealBanachSpace

for T being Lipschitzian LinearOperator of X,Y st T is bijective holds

T " is Lipschitzian LinearOperator of Y,X

for T being Lipschitzian LinearOperator of X,Y st T is bijective holds

T " is Lipschitzian LinearOperator of Y,X

proof end;

theorem Th8: :: LOPBAN_7:8

for X, Y being RealNormSpace

for seqx being sequence of X

for seqy being sequence of Y

for x being Point of X

for y being 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] ) )

for seqx being sequence of X

for seqy being sequence of Y

for x being Point of X

for y being 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 end;

definition
end;

:: deftheorem defines graph LOPBAN_7:def 1 :

for X, Y being RealNormSpace

for T being PartFunc of X,Y holds graph T = T;

for X, Y being RealNormSpace

for T being PartFunc of X,Y holds graph T = T;

registration

let X, Y be RealNormSpace;

let T be non empty PartFunc of X,Y;

correctness

coherence

not graph T is empty ;

;

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

correctness

coherence

not graph T is empty ;

;

registration

let X, Y be RealNormSpace;

let T be LinearOperator of X,Y;

correctness

coherence

graph T is linearly-closed ;

end;
let T be LinearOperator of X,Y;

correctness

coherence

graph T is linearly-closed ;

proof end;

definition

let X, Y be RealNormSpace;

let T be LinearOperator of X,Y;

coherence

the normF of [:X,Y:] | (graph T) is Function of (graph T),REAL;

;

end;
let T be LinearOperator of X,Y;

func graphNrm T -> Function of (graph T),REAL equals :: LOPBAN_7:def 2

the normF of [:X,Y:] | (graph T);

correctness the normF of [:X,Y:] | (graph T);

coherence

the normF of [:X,Y:] | (graph T) is Function of (graph T),REAL;

;

:: deftheorem defines graphNrm LOPBAN_7:def 2 :

for X, Y being RealNormSpace

for T being LinearOperator of X,Y holds graphNrm T = the normF of [:X,Y:] | (graph T);

for X, Y being RealNormSpace

for T being LinearOperator of X,Y holds graphNrm T = the normF of [:X,Y:] | (graph T);

:: deftheorem defines closed LOPBAN_7:def 3 :

for X, Y being RealNormSpace

for T being PartFunc of X,Y holds

( T is closed iff graph T is closed );

for X, Y being RealNormSpace

for T being PartFunc of X,Y holds

( T is closed iff graph T is closed );

definition

let X, Y be RealNormSpace;

let T be LinearOperator of X,Y;

coherence

NORMSTR(# (graph T),(Zero_ ((graph T),[:X,Y:])),(Add_ ((graph T),[:X,Y:])),(Mult_ ((graph T),[:X,Y:])),(graphNrm T) #) is non empty NORMSTR ;

;

end;
let T be LinearOperator of X,Y;

func graphNSP T -> non empty NORMSTR equals :: LOPBAN_7:def 4

NORMSTR(# (graph T),(Zero_ ((graph T),[:X,Y:])),(Add_ ((graph T),[:X,Y:])),(Mult_ ((graph T),[:X,Y:])),(graphNrm T) #);

correctness NORMSTR(# (graph T),(Zero_ ((graph T),[:X,Y:])),(Add_ ((graph T),[:X,Y:])),(Mult_ ((graph T),[:X,Y:])),(graphNrm T) #);

coherence

NORMSTR(# (graph T),(Zero_ ((graph T),[:X,Y:])),(Add_ ((graph T),[:X,Y:])),(Mult_ ((graph T),[:X,Y:])),(graphNrm T) #) is non empty NORMSTR ;

;

:: deftheorem defines graphNSP LOPBAN_7:def 4 :

for X, Y being RealNormSpace

for T being LinearOperator of X,Y holds graphNSP T = NORMSTR(# (graph T),(Zero_ ((graph T),[:X,Y:])),(Add_ ((graph T),[:X,Y:])),(Mult_ ((graph T),[:X,Y:])),(graphNrm T) #);

for X, Y being RealNormSpace

for T being LinearOperator of X,Y holds graphNSP T = NORMSTR(# (graph T),(Zero_ ((graph T),[:X,Y:])),(Add_ ((graph T),[:X,Y:])),(Mult_ ((graph T),[:X,Y:])),(graphNrm T) #);

registration

let X, Y be RealNormSpace;

let T be LinearOperator of X,Y;

( graphNSP T is Abelian & graphNSP T is add-associative & graphNSP T is right_zeroed & graphNSP T is right_complementable & graphNSP T is scalar-distributive & graphNSP T is vector-distributive & graphNSP T is scalar-associative & graphNSP T is scalar-unital )

end;
let T be LinearOperator of X,Y;

cluster graphNSP T -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence ( graphNSP T is Abelian & graphNSP T is add-associative & graphNSP T is right_zeroed & graphNSP T is right_complementable & graphNSP T is scalar-distributive & graphNSP T is vector-distributive & graphNSP T is scalar-associative & graphNSP T is scalar-unital )

proof end;

theorem Th9: :: LOPBAN_7:9

for X, Y being RealNormSpace

for T being LinearOperator of X,Y holds graphNSP T is Subspace of [:X,Y:]

for T being LinearOperator of X,Y holds graphNSP T is Subspace of [:X,Y:]

proof end;

Lm1: for X, Y being RealNormSpace

for T being LinearOperator of X,Y

for x, y being Point of (graphNSP T)

for a being Real holds

( ( ||.x.|| = 0 implies x = 0. (graphNSP T) ) & ( x = 0. (graphNSP T) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )

proof end;

registration

let X, Y be RealNormSpace;

let T be LinearOperator of X,Y;

coherence

( graphNSP T is reflexive & graphNSP T is discerning & graphNSP T is RealNormSpace-like ) by Lm1;

end;
let T be LinearOperator of X,Y;

coherence

( graphNSP T is reflexive & graphNSP T is discerning & graphNSP T is RealNormSpace-like ) by Lm1;

theorem Th10: :: LOPBAN_7:10

for X being RealNormSpace

for Y being RealBanachSpace

for X0 being 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

for Y being RealBanachSpace

for X0 being 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 end;

theorem Th11: :: LOPBAN_7:11

for X, Y being RealBanachSpace

for T being LinearOperator of X,Y st T is closed holds

graphNSP T is complete

for T being LinearOperator of X,Y st T is closed holds

graphNSP T is complete

proof end;

theorem Th12: :: LOPBAN_7:12

for X, Y being RealNormSpace

for T being non empty PartFunc of X,Y holds

( T is closed iff for seq being 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 T being non empty PartFunc of X,Y holds

( T is closed iff for seq being 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 end;

theorem :: LOPBAN_7:13

for X, Y being RealNormSpace

for T being non empty PartFunc of X,Y

for T0 being LinearOperator of X,Y st T0 is Lipschitzian & dom T is closed & T = T0 holds

T is closed

for T being non empty PartFunc of X,Y

for T0 being LinearOperator of X,Y st T0 is Lipschitzian & dom T is closed & T = T0 holds

T is closed

proof end;

theorem :: LOPBAN_7:14

for X, Y being RealNormSpace

for T being non empty PartFunc of X,Y

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

S is closed

for T being non empty PartFunc of X,Y

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

S is closed

proof end;

:: The Closed Graph Theorem

theorem Th15: :: LOPBAN_7:15

for X, Y being RealNormSpace

for x being Point of X

for y being Point of Y holds

( ||.x.|| <= ||.[x,y].|| & ||.y.|| <= ||.[x,y].|| )

for x being Point of X

for y being Point of Y holds

( ||.x.|| <= ||.[x,y].|| & ||.y.|| <= ||.[x,y].|| )

proof end;

registration

let X, Y be RealBanachSpace;

for b_{1} being LinearOperator of X,Y st b_{1} is closed holds

b_{1} is Lipschitzian

end;
cluster Function-like quasi_total additive homogeneous closed -> Lipschitzian for LinearOperator of ,;

coherence for b

b

proof end;