:: Banach's Continuous Inverse Theorem and Closed Graph Theorem
:: by Hideki Sakurai , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 6, 2012
:: Copyright (c) 2012 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, CARD_1, XXREAL_0, ARYTM_3, RELAT_1, ARYTM_1, XBOOLE_0,
SUBSET_1, FUNCT_1, ZFMISC_1, NORMSP_1, RLSUB_1, RSSPACE, COHSP_1,
PRE_TOPC, METRIC_1, SUPINF_2, TARSKI, REAL_1, COMPLEX1, LOPBAN_1,
STRUCT_0, NORMSP_2, RCOMP_1, NAT_1, CARD_3, ORDINAL2, SEQ_2, RSSPACE3,
FUNCT_2, UNIALG_1, PARTFUN1, FCONT_1, CFCONT_1, RLVECT_1, TMAP_1,
MSSUBFAM, RELAT_2, RLTOPSP1, REWRITE1, FINSEQ_1, NORMSP_0, ALGSTR_0,
LOPBAN_7, REALSET1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, REALSET1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0,
COMPLEX1, FUNCT_3, FINSEQ_1, FINSEQ_2, STRUCT_0, ALGSTR_0, PRE_TOPC,
RLVECT_1, RLSUB_1, VECTSP_1, NORMSP_0, NORMSP_1, T_0TOPSP, TMAP_1,
RLTOPSP1, RSSPACE, EUCLID, RSSPACE3, LOPBAN_1, NFCONT_1, NORMSP_2,
PDIFF_1, PRVECT_3;
constructors REAL_1, PCOMPS_1, RUSUB_4, NFCONT_1, FUNCT_3, NEWTON, NORMSP_2,
RSSPACE3, T_0TOPSP, RELSET_1, TMAP_1, PRVECT_3, PDIFF_1, REALSET1;
registrations XREAL_0, XXREAL_0, ORDINAL1, RELSET_1, STRUCT_0, NAT_1,
NORMSP_1, NORMSP_2, FUNCT_1, FUNCT_2, LOPBAN_1, NORMSP_0, RELAT_1,
RLTOPSP1, PRVECT_3, NUMBERS, XBOOLE_0, VALUED_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, FUNCT_2, STRUCT_0, RLVECT_1, PCOMPS_1, NORMSP_0, NORMSP_1,
NORMSP_2, LOPBAN_1, VECTSP_1, PRVECT_3, RLSUB_1;
theorems TARSKI, XBOOLE_1, RLVECT_1, RELAT_1, RLSUB_1, ZFMISC_1, FUNCT_2,
XREAL_1, XCMPLX_1, NORMSP_1, NFCONT_1, XXREAL_0, FUNCT_1, ORDINAL1,
PARTFUN1, VECTSP_1, RSSPACE, NORMSP_2, FUNCT_3, ABSVALUE, PDIFF_8,
PDIFF_1, FINSEQ_1, XTUPLE_0, LOPBAN_1, NORMSP_0, LOPBAN_6, T_0TOPSP,
TOPS_2, TMAP_1, PRVECT_3, RSSPACE3;
schemes FUNCT_2;
begin
definition
let X,Y be non empty NORMSTR,
x be Point of X,
y be Point of Y;
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;
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 Lm010:
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 AS0: T is bijective;
AX0:rng T = the carrier of Y by AS0,FUNCT_2:def 3;
AX3: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 AS0,AX0,FUNCT_2:25;
ABX1: T1 is additive
proof
let y1,y2 be Point of Y;
consider x1,x2 be Point of X such that
AB10: T1.y1=x1 & T1.y2=x2;
AB30: T.x1=y1 & T.x2=y2 by AB10,AS0,AX0,FUNCT_1:32;
x1+x2 =T1.(T.(x1+x2)) by AS0,FUNCT_1:32, AX3
.=T1.(y1+y2) by AB30, VECTSP_1:def 20;
hence thesis by AB10;
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 AS0,FUNCT_1:32,AX3
.=T1.(r*T.x1) by LOPBAN_1:def 5
.=T1.(r*y1) by AS0,AX0,FUNCT_1:32;
hence thesis;
end;
hence thesis by ABX1;
end;
hence thesis by AS0,FUNCT_1:33,AX3;
end;
theorem
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 AS0: T is bijective open & S = T"; then
P1: T" is LinearOperator of Y,X & T" is one-to-one
& rng(T") = the carrier of X by Lm010;
A1: [#] Y<>{} & [#] X<>{};
S is continuous
proof
now let A be Subset of X;
assume X1:A is open;
S"A = S".:A by AS0,FUNCT_1:85
.=T.:A by AS0,FUNCT_1:43;
hence S"A is open by X1, AS0,T_0TOPSP:def 2;
end;
hence thesis by A1,TOPS_2:43;
end;
hence thesis by P1,AS0,FUNCT_2:def 3;
end;
theorem Lm01B:
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 Lm01A:
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 Lm01B;
hereby assume P1:f is_continuous_in x;
now let r be Real;
assume 0 < r;
then consider s be Real such that
P3: 0~~0.X;
then
C21A: ||.x1.|| <> 0 by NORMSP_0:def 5;
set r3= (s/2)/||.x1.||;
0 < s/2 by AX1,XREAL_1:215;
then
C22A: 0 < r3 by C21A,XREAL_1:139;
set x2=r3*x1;
C23: 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 AX1,ABSVALUE:def 1
.=s/2 by C21, NORMSP_0:def 5,XCMPLX_1:87;
then ||.x2.||~~~~{} & [#]LinearTopSpaceNorm X<>{};
now let A be Subset of LinearTopSpaceNorm X;
assume X1: A is open;
T3"A = T3".:A by AS0,FUNCT_1:85
.= S.:A by AS0,FUNCT_1:43;
hence T3"A is open by X1, AS1,AS0,LOPBAN_6:16,T_0TOPSP:def 2;
end;
hence thesis by A1,TOPS_2:43;
end;
AC60: 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;
KK: T3 is_continuous_at xt by AC30,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 KK,NORMSP_2:35;
hence T2| (the carrier of Y) is_continuous_in x by NORMSP_2:18;
end;
hence thesis by Lm01, AC60,NFCONT_1:def 7;
end;
theorem Lm200A:
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 P1:
seqx is convergent & lim seqx = x & seqy is convergent & lim seqy = y;
P60: for r be Real st 0 < r ex m be Nat
st for n be Nat st m <= n holds ||.(seq.n) - v.|| < r
proof
let r1 be Real;
assume P61: 0 < r1;
set r=r1/2;
Q61: 0 < r & r < r1 by P61,XREAL_1:215,216;
set r2=r/2;
P62:0 < r2 & r2 < r by Q61,XREAL_1:215,216;
then consider m1 be Nat such that
P63: for n be Nat
st m1 <= n holds ||.(seqx.n) - x .|| < r2 by P1,NORMSP_1:def 7;
consider m2 be Nat such that
P64: for n be Nat
st m2 <= n holds ||.(seqy.n) - y .|| < r2 by P1,P62,NORMSP_1:def 7;
take m=max(m1,m2);
let n be Nat;
assume P65: m <= n;
m1 <= m by XXREAL_0:25; then
P66: m1<= n by P65,XXREAL_0:2;
m2 <= m by XXREAL_0:25; then
P67: m2<= n by P65,XXREAL_0:2;
n in NAT by ORDINAL1:def 12; then
K5: [seqx.n,seqy.n] = seq.n by FUNCT_3:59;
J6: - v = [-x, -y] by PRVECT_3:18;
(seq.n) - v = [(seqx.n)-x,(seqy.n)-y] by K5,J6,PRVECT_3:18;
then consider w be Element of REAL 2 such that
K7: 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
K71: i in Seg 2 by FINSEQ_1:1;
per cases by K71,FINSEQ_1:2,TARSKI:def 2;
suppose K72: i=1;
K73:(proj (i,2)).w = w.1 by K72,PDIFF_1:def 1
.= ||. (seqx.n)-x .|| by K7,FINSEQ_1:44;
|. (proj (i,2)).w .| = ||. (seqx.n)-x .||
by ABSVALUE:def 1, K73;
hence |. (proj (i,2)).w .| <= r2 by P66, P63;
end;
suppose i=2; then
K74:(proj (i,2)).w = w.2 by PDIFF_1:def 1
.= ||. (seqy.n)-y .|| by K7,FINSEQ_1:44;
|. (proj (i,2)).w .| = ||. (seqy.n)-y .||
by ABSVALUE:def 1, K74;
hence |. (proj (i,2)).w .| <= r2 by P67,P64;
end;
end;
then |.w.| <= 2*(r2) by PDIFF_8:17;
hence ||. (seq.n) - v .|| < r1 by K7,Q61,XXREAL_0:2;
end;
hence seq is convergent by NORMSP_1:def 6;
hence lim seq = [x, y] by P60,NORMSP_1:def 7;
end;
assume
R1:seq is convergent & lim seq = [x,y];
P600: for r be Real st 0 < r 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
K2: for n be Nat st m <= n holds ||.(seq.n) - v.|| < r by R1,NORMSP_1:def 7;
take m;
let n be Nat;
assume m <= n; then
K4: ||.(seq.n) - v .|| < r by K2;
n in NAT by ORDINAL1:def 12; then
K5: [seqx.n,seqy.n ] = seq.n by FUNCT_3:59;
J6: - v = [-x,-y] by PRVECT_3:18;
(seq.n) - v = [(seqx.n)-x,(seqy.n)-y] by K5,J6,PRVECT_3:18;
then consider w be Element of REAL 2 such that
K7: 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 K7,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 K7,K4,XXREAL_0:2;
(proj (2,2)).w = w.2 by PDIFF_1:def 1
.= ||. (seqy.n)-y .|| by K7,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 K7,K4,XXREAL_0:2;
end;
P60 :now let r be Real;
assume 0 < r;
then consider m be Nat such that
P611: for n be Nat st m <= n holds
||.(seqx.n)-x.|| < r & ||.(seqy.n)-y.|| < r by P600;
take m;
thus for n be Nat st m <= n holds
||.(seqx.n) - x.|| < r by P611;
end;
hence seqx is convergent by NORMSP_1:def 6;
hence lim seqx = x by P60,NORMSP_1:def 7;
P70: now let r be Real;
assume 0 < r;
then consider m be Nat such that
P611: for n be Nat st m <= n holds
||.(seqx.n)-x.|| < r & ||.(seqy.n)-y.|| < r by P600;
take m;
thus for n be Nat st m <= n holds
||.(seqy.n)-y.|| < r by P611;
end;
hence seqy is convergent by NORMSP_1:def 6;
hence lim seqy = y by P70,NORMSP_1:def 7;
end;
definition
let X,Y be RealNormSpace;
let T be PartFunc of X, Y;
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
A4: v in W and
A5: u in W;
consider x1,y1 be set such that
R32: v = [x1,y1] by RELAT_1:def 1;
R34: x1 in dom T & y1 = T.x1 by FUNCT_1:1,R32,A4;
reconsider x1 as VECTOR of X by R32,ZFMISC_1:87;
reconsider y1 as VECTOR of Y by R32,ZFMISC_1:87;
consider x2,y2 be set such that
P32: u = [x2,y2] by RELAT_1:def 1;
reconsider x2 as VECTOR of X by P32,ZFMISC_1:87;
reconsider y2 as VECTOR of Y by P32,ZFMISC_1:87;
x1+x2 in the carrier of X; then
R35: x1+x2 in dom T by FUNCT_2:def 1;
R37: y1+y2 = (T.x1) +(T.x2) by R34,FUNCT_1:1,P32,A5
.= T.(x1+x2) by VECTSP_1:def 20;
[x1+x2,y1+y2 ] = v + u by PRVECT_3:18,R32,P32;
hence v+u in W by R37,R35,FUNCT_1:1;
end;
let a be Real;
let v be VECTOR of V;
assume R31: v in W;
consider x,y be set such that
R32: v = [x,y] by RELAT_1:def 1;
reconsider x as VECTOR of X by R32,ZFMISC_1:87;
reconsider y as VECTOR of Y by R32,ZFMISC_1:87;
a*x in the carrier of X; then
R35: a*x in dom T by FUNCT_2:def 1;
R37: a*y = a*(T.x) by FUNCT_1:1,R32,R31
.=T.(a*x) by LOPBAN_1:def 5;
[a*x,a*y ] = a*v by PRVECT_3:18,R32;
hence a*v in W by R37,R35,FUNCT_1:1;
end;
end;
definition
let X,Y be RealNormSpace;
let T be LinearOperator of X,Y;
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;
attr T is closed means :DefCL0:
graph(T) is closed;
correctness;
end;
definition
let X,Y be RealNormSpace, T be LinearOperator of X,Y;
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 Lm4000E:
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;
P2: 0.l = 0.W
.= 0.([:X,Y:]) by RLSUB_1:def 2;
P3: 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 P2,P3,RLSUB_1:def 2;
end;
Lm4000F:
for X,Y be RealNormSpace,
T be LinearOperator of X,Y,
x, y being 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:];
P0: W is Subspace of V by Lm4000E;
P1: ||.x.|| = ||.x1.|| by FUNCT_1:49;
P2: ||.y.|| = ||.y1.|| by FUNCT_1:49;
x+y = x1+y1 by P0,RLSUB_1:13; then
P30: ||. x+y .|| = ||. x1+y1 .|| by FUNCT_1:49;
a*x = a*x1 by P0,RLSUB_1:14; then
P40: ||. a*x .|| = ||. a*x1 .|| by FUNCT_1:49;
P5: 0.([:X,Y:]) = 0.(graphNSP(T)) by P0,RLSUB_1:11;
||.x.|| = 0 iff ||.x1.|| = 0 by FUNCT_1:49;
hence ||.x.|| = 0 iff x = 0.(graphNSP(T)) by P5, NORMSP_0:def 5;
thus 0 <= ||.x.|| by P1;
thus ||.x+y.|| <= ||.x.|| + ||.y.|| by P1,P2,P30, NORMSP_1:def 1;
thus thesis by P1,P40,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
proof
thus ||.0.(graphNSP(T)).|| = 0 by Lm4000F;
thus for x be Point of graphNSP(T) st
||.x.|| = 0 holds x = 0.(graphNSP(T)) by Lm4000F;
thus for x, y being Point of graphNSP(T), a be Real
holds ||.a * x.|| = |.a.| * ||.x.|| & ||.x + y
.|| <= ||.x.|| + ||.y.|| by Lm4000F;
end;
end;
theorem Lm4000G:
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 AS: 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 A2A: seq is Cauchy_sequence_by_Norm;
rng seq c= the carrier of Y by AS,XBOOLE_1:1; then
reconsider yseq=seq as sequence of Y by FUNCT_2:6;
for r be Real st r > 0 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
A20: for n, m be Nat st n >= k & m >= k
holds ||.(seq.n) - (seq.m).|| < r by RSSPACE3:8,A2A;
take k;
now let n, m be Nat;
assume A40: n >= k & m >= k;
(seq.n) - (seq.m) = (yseq.n) - (yseq.m) by AS,RLSUB_1:16;
then ||.(seq.n) - (seq.m).||
= ||.(yseq.n) - (yseq.m).|| by FUNCT_1:49,AS;
hence ||.(yseq.n) - (yseq.m).|| < r by A40,A20;
end;
hence thesis;
end; then
A3: yseq is convergent by LOPBAN_1:def 15, RSSPACE3:8;
rng yseq = rng seq;
then reconsider lyseq=lim yseq as Point of X by AS,A3,NFCONT_1:def 3;
for r be Real st 0 < r 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 A3,NORMSP_1:def 7;
take m;
now let n be Nat;
assume A8: m <= n;
(yseq.n) - (lim yseq) = (seq.n) - (lyseq) by AS,RLSUB_1:16;
then ||.(yseq.n) - (lim yseq).||
= ||.(seq.n) - (lyseq).|| by FUNCT_1:49,AS;
hence ||.(seq.n) - (lyseq).|| < r by A8,A6;
end;
hence thesis;
end;
hence seq is convergent by NORMSP_1:def 6;
end;
hence thesis by LOPBAN_1:def 15;
end;
theorem Lm4000H:
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 Lm4000E;
hence thesis by Lm4000G,DefCL0;
end;
theorem Lm200B:
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 P10: 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 P3: rng seq c= dom T & seq is convergent & T/*seq is convergent;
set s1 = <:seq,T/*seq:>;
P5: rng s1 c= graph(T)
proof
let y be element;
assume y in rng s1;
then consider i be set
such that P52: i in NAT & s1.i = y by FUNCT_2:11;
P55: (T/*seq).i = T.(seq.i) by P52,P3,FUNCT_2:108;
seq.i in rng seq by P52,FUNCT_2:4;
then [seq.i,(T/*seq).i ] in T by P55,FUNCT_1:def 2,P3;
hence y in graph(T) by P52,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 Lm200A,P3;
then [lim seq, lim (T/*seq) ] in graph(T)
by P10,DefCL0,NFCONT_1:def 3,P5;
hence lim seq in dom T & lim (T/*seq)= T.(lim seq) by FUNCT_1:1;
end;
end;
assume
R1: 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 R2: rng s1 c= graph(T) & s1 is convergent;
defpred Q0[set,set] means [$2,T.$2] = s1.$1;
R30: for i being Element of NAT ex x being Element of
the carrier of X st Q0[i,x]
proof
let i be Element of NAT;
X3: s1.i in rng s1 by FUNCT_2:4;
consider x be Point of X,y be Point of Y such that
P50: s1.i =[x,y] by PRVECT_3:18;
take x;
thus thesis by P50,FUNCT_1:1,X3,R2;
end;
consider seq be sequence of X such that
P41: for x being Element of NAT holds Q0[x,seq.x] from FUNCT_2:sch 3(R30);
XX1: now let y be element;
assume y in rng seq; then
consider i be set such that
X02: i in dom seq & y=seq. i by FUNCT_1:def 3;
X1: [seq.i,T.(seq.i) ] = s1.i by X02,P41;
s1.i in rng s1 by X02,FUNCT_2:4;
hence y in dom T by X02,FUNCT_1:1, X1,R2;
end; then
X0:rng seq c= dom T by TARSKI:def 3;
consider x be Point of X,y be Point of Y such that
P50: 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 XX1,TARSKI:def 3,FUNCT_2:108;
hence s1.n = [seq.n,(T/*seq).n] by P41
.= <:seq,T/*seq:>.n by FUNCT_3:59;
end; then
R4: seq is convergent & lim seq = x
& T/*seq is convergent & lim (T/*seq) = y by P50,Lm200A,R2;
lim seq in dom T & lim (T/*seq)= T.(lim seq) by X0,R1,R4;
hence lim s1 in graph(T) by P50,R4,FUNCT_1:1;
end;
hence thesis by DefCL0,NFCONT_1:def 3;
end;
theorem
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
P100:T0 is Lipschitzian & dom T is closed & T=T0; then
P120:T is_continuous_in 0.X by Lm01C,Lm01;
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
P200: rng seq c= dom T & seq is convergent & T/*seq is convergent;
P310:T is_continuous_in lim seq by P100,P120,Lm01A;
T/.(lim seq)=T.(lim seq) by P100,P200,NFCONT_1:def 3,PARTFUN1:def 6;
hence thesis by P200,P310, NFCONT_1:def 5;
end;
hence thesis by Lm200B;
end;
theorem
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
P100:T is closed & T is one-to-one & S=T";
P240: rng T = dom S & dom T = rng S by P100, 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
P300: rng seq c= dom S & seq is convergent & S/*seq is convergent;
set seq1=S/*seq;
P380: rng seq1 c= dom T
proof
let x be element;
assume x in rng seq1;
then consider i be set such that
PX20: i in dom seq1 & x=seq1.i by FUNCT_1:def 3;
reconsider i as Nat by PX20;
S.(seq.i) in rng S by FUNCT_1:3, P300,NFCONT_1:5;
hence x in dom T by PX20, P240, P300,FUNCT_2:108;
end;
P450:T/*seq1=seq
proof
now
let n be Element of NAT;
thus (T/*seq1).n = seq.n
proof
PZ10: seq.n in rng T by P300,NFCONT_1:5,P240;
(T/*seq1).n= T.(seq1.n) by P380,FUNCT_2:108
.= T.(S.(seq.n)) by P300,FUNCT_2:108
.= seq.n by P100,PZ10,FUNCT_1:35;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
lim seq1 in dom T & lim (T/*seq1)=T.(lim S/*seq)
by P100,P300,P380,P450,Lm200B;
hence thesis by P240,P450,FUNCT_1:3,P100,FUNCT_1:34;
end;
hence thesis by Lm200B;
end;
:: The Closed Graph Theorem
theorem Lm400X:
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
P63: w=<* ||.x.||,||.y.|| *> & ||.[x,y].|| = |.w.| by PRVECT_3:18;
(proj (1,2)).w = w.1 by PDIFF_1:def 1
.= ||.x.|| by P63,FINSEQ_1:44;
then |. ||.x.|| .| <= |.w.| by PDIFF_8:5;
hence ||.x.|| <= ||.[x,y].|| by P63, ABSVALUE:def 1;
(proj (2,2)).w = w.2 by PDIFF_1:def 1
.= ||.y.|| by P63,FINSEQ_1:44;
then |. ||.y.|| .| <= |.w.| by PDIFF_8:5;
hence ||.y.|| <= ||.[x,y].|| by P63, 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
P100: T is closed;
defpred Q0[set,set] means $1=[$2,T.$2];
P3: for z be set st z in the carrier of graphNSP(T) ex x be set
st x in the carrier of X & Q0[z,x]
proof
let z be set;
assume
R31:z in the carrier of graphNSP(T);
then consider x,y be set such that
R32: z = [x,y] by RELAT_1:def 1;
x in dom T & y = T.x by FUNCT_1:1,R32,R31;
hence thesis by R32;
end;
consider J be Function of graphNSP(T), X such that
P4: for z be set st z in the carrier of graphNSP(T) holds Q0[z,J.z]
from FUNCT_2:sch 1(P3);
P5: graphNSP(T) is complete by Lm4000H, P100;
X1: graphNSP(T) is Subspace of [:X,Y:]
& the normF of graphNSP(T) = (the normF of [:X,Y:] )
| (the carrier of graphNSP(T)) by Lm4000E;
P6: for x being VECTOR of graphNSP(T),
r being Real holds J.(r*x) = r*J.x
proof
let x be VECTOR of graphNSP(T), r be Real;
P60: x = [J.x,T.(J.x)] by P4;
P61: r*x = [J.(r*x),T.(J.(r*x)) ] by P4;
x in graph(T); then
reconsider x1=x as Point of [:X,Y:];
r*x1=r*x by X1, RLSUB_1:14; then
r*x = [r*(J.x),r*(T.(J.x))] by PRVECT_3:18,P60;
hence J.(r*x) = r*(J.x) by P61,XTUPLE_0:1;
end;
for x,y being VECTOR of graphNSP(T) holds J.(x+y) = J.x + J.y
proof
let x,y be VECTOR of graphNSP(T);
P60: x = [J.x,T.(J.x)] by P4;
R60: y = [J.y,T.(J.y)] by P4;
P61: x+y = [J.(x+y),T.(J.(x+y)) ] by P4;
x in graph(T) & y in graph(T); then
reconsider x1=x,y1=y as Point of [:X,Y:];
x1+y1=x+y by X1, RLSUB_1:13;
then x+y = [(J.x)+(J.y),(T.(J.x)) + (T.(J.y)) ] by PRVECT_3:18,P60,R60;
hence J.(x+y) = (J.x) + (J.y) by P61,XTUPLE_0:1;
end;
then reconsider
J as LinearOperator of graphNSP(T),X by P6, LOPBAN_1:def 5, VECTSP_1:def 20;
J is Lipschitzian
proof
PAS01: now
let x be Point of graphNSP(T);
x in graph(T); then
reconsider x1=x as Point of [:X,Y:];
P62: x1= [J.x,T.(J.x)] by P4;
||.J.x.|| <= ||.x1.|| by P62,Lm400X;
hence ||.J.x.|| <= 1 * ||.x.|| by FUNCT_1:49;
end;
take 1;
thus thesis by PAS01;
end;
then reconsider J as Lipschitzian LinearOperator of graphNSP(T),X;
now let x,y be set;
assume AS1: 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 P4;
hence x=y by P4,AS1;
end; then
PA200: J is one-to-one by FUNCT_2:19;
for y be element holds y in rng J iff y in the carrier of X
proof
let y be element;
now assume A2: y in the carrier of X;
then reconsider y1=y as Point of X;
y1 in dom T by A2,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 P4;
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 FUNCT_2:def 3, TARSKI:2;
then reconsider L=J" as
Lipschitzian LinearOperator of X,graphNSP(T) by PA200,Lm100,P5;
consider K being Real such that
G1: 0 <= K &
for x being 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;
P60: x = [J.x,T.(J.x)] by P4;
R72: ||. L.y .|| <= K * ||. y .|| by G1;
x in the carrier of graphNSP(T); then
XX1: x in dom J by FUNCT_2:def 1;
R73: L.y = L.(J.x) by XTUPLE_0:1,P60
.= x by FUNCT_1:34,PA200,XX1;
reconsider x1=x as Point of [:X,Y:];
||.x1.|| = ||.x.|| by FUNCT_1:49;
then ||.T.y.|| <= ||. L.y .|| by R73, Lm400X;
hence ||.T.y.|| <= K * ||. y .|| by R72,XXREAL_0:2;
end;
hence T is Lipschitzian by LOPBAN_1:def 8,G1;
end;
end;
~~