:: Open Mapping Theorem
:: by Hideki Sakurai , Hisayoshi Kunimune and Yasunari Shidama
::
:: Received September 23, 2008
:: Copyright (c) 2008-2021 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, MCART_1, ZFMISC_1, NORMSP_1, PRE_TOPC, METRIC_1,
SUPINF_2, TARSKI, REAL_1, COMPLEX1, LOPBAN_1, STRUCT_0, NORMSP_2,
RCOMP_1, CONVEX1, XCMPLX_0, PREPOWER, SERIES_1, NEWTON, NAT_1, CARD_3,
ORDINAL2, SEQ_2, RSSPACE3, FUNCT_2, PARTFUN1, FCONT_1, PROB_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, FUNCT_1, RELSET_1, FUNCT_2,
XTUPLE_0, MCART_1, PRE_TOPC, DOMAIN_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, COMPLEX1, REAL_1, NAT_1, STRUCT_0, XXREAL_0, SEQ_2, NEWTON,
PREPOWER, SERIES_1, RLVECT_1, CONVEX1, RUSUB_4, NORMSP_0, NORMSP_1,
NORMSP_2, RSSPACE3, LOPBAN_1, NFCONT_1, LOPBAN_5, KURATO_2, T_0TOPSP;
constructors REAL_1, DOMAIN_1, SEQ_2, PCOMPS_1, RUSUB_4, CONVEX1, NFCONT_1,
NEWTON, PREPOWER, SERIES_1, NORMSP_2, RSSPACE3, LOPBAN_5, T_0TOPSP,
RELSET_1, COMSEQ_2, XTUPLE_0, BINOP_1;
registrations XREAL_0, XXREAL_0, ORDINAL1, RELSET_1, STRUCT_0, TOPS_1,
SUBSET_1, NAT_1, NORMSP_1, NORMSP_2, FUNCT_2, LOPBAN_1, NORMSP_0, NEWTON,
XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, T_0TOPSP, XBOOLE_0;
equalities RLVECT_1, PCOMPS_1, CONVEX1, RUSUB_4, ALGSTR_0, NORMSP_2, XBOOLE_0,
LOPBAN_5;
expansions TARSKI, CONVEX1, XBOOLE_0;
theorems TARSKI, SEQ_2, RLVECT_1, RELAT_1, RUSUB_4, RLTOPSP1, SERIES_1,
PREPOWER, ZFMISC_1, FUNCT_2, XBOOLE_0, XREAL_1, XCMPLX_1, NORMSP_1,
PRE_TOPC, NFCONT_1, XXREAL_0, FUNCT_1, NEWTON, MESFUNC1, NORMSP_2,
RINFSUP1, ABSVALUE, XCMPLX_0, LOPBAN_3, ORDINAL1, RSSPACE2, LOPBAN_1,
NAT_1, PROB_1, LOPBAN_5, CONVEX1, VECTSP_1, NORMSP_0;
schemes FUNCT_2, RECDEF_1, NAT_1;
begin
theorem Th1:
for x,y be Real st 0<=x & x non empty set, A() -> Element of D(), B() -> Element of D(),
P[object,object,object,object]}:
ex f being sequence of D() st f.0 = A() & f.1 = B() &
for n being Nat holds P[n,f.n,f.(n+1),f.(n+2)]
provided
A1: for n being Nat for x,y being Element of D() ex z being
Element of D() st P[n,x,y,z]
proof
defpred Q[set,set,set] means P[$1, $2`1,$2`2, $3`2] & $2`2 = $3`1;
A2: for n being Nat for x being Element of [:D(),D() :] ex y
being Element of [:D(),D() :] st Q[n,x,y]
proof
let n be Nat;
let x be Element of [:D(),D() :];
set z=x`1;
set w=x`2;
reconsider z,w as Element of D();
consider s being Element of D() such that
A3: P[n,z,w,s] by A1;
set y = [w,s];
reconsider y as Element of [:D(),D() :];
take y;
thus thesis by A3;
end;
consider g being sequence of [:D(),D() :] such that
A4: g.0 = [A(),B()] & for n being Nat holds Q[n,g.n,g.(n+1)]
from RECDEF_1:sch 2(A2);
deffunc F(Nat)=(g.$1)`1;
A5: for x being Element of NAT holds F(x) in D();
consider f being sequence of D() such that
A6: for x being Element of NAT holds f.x = F(x) from FUNCT_2:sch 8(A5);
A7: now
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
A8: f.n = (g.nn)`1 by A6;
Q[n+1,g.(n+1),g.((n+1)+1)] by A4;
then
A9: f.(n+2) =(g.(n+1))`2 by A6;
f.(n+1) = (g.(n+1))`1 by A6
.=(g.nn)`2 by A4;
hence P[n, f.n,f.(n+1), f.(n+2)] by A4,A8,A9;
end;
take f;
A10: Q[0,g.0,g.(0+1)] by A4;
A11: f.0 = (g.0)`1 by A6
.= A() by A4;
f.1 = (g.1)`1 by A6
.= B() by A4,A10;
hence thesis by A11,A7;
end;
reserve X, Y for RealNormSpace;
theorem Th2:
for y1 be Point of X, r be Real holds Ball(y1,r) = y1 + Ball(0.X,r)
proof
let y1 be Point of X, r be Real;
thus Ball(y1,r) c=y1 + Ball(0.X,r)
proof
let t be object;
assume
A1: t in Ball(y1,r);
then reconsider z1=t as Point of X;
set z0=z1-y1;
ex zz1 be Point of X st z1=zz1 & ||.y1-zz1.|| < r by A1;
then ||.-z0.|| < r by RLVECT_1:33;
then ||.0.X-z0.||< r by RLVECT_1:14;
then
A2: z0 in Ball(0.X,r);
z0+y1=z1+((-y1)+y1) by RLVECT_1:def 3;
then z0+y1=z1+0.X by RLVECT_1:5;
then z1=z0+y1 by RLVECT_1:4;
hence thesis by A2;
end;
let t be object;
assume t in y1 + Ball(0.X,r);
then consider z0 be Point of X such that
A3: t=y1+z0 and
A4: z0 in Ball(0.X,r);
set z1=z0+y1;
ex zz0 be Point of X st z0=zz0 & ||.0.X-zz0.|| < r by A4;
then ||.-z0.|| < r by RLVECT_1:14;
then ||.z0.|| < r by NORMSP_1:2;
then ||.z0+ 0.X.|| < r by RLVECT_1:4;
then ||.z0+ (y1+-y1).|| < r by RLVECT_1:5;
then ||.z1-y1.|| < r by RLVECT_1:def 3;
then ||.y1-z1.|| < r by NORMSP_1:7;
hence thesis by A3;
end;
theorem Th3:
for r,a be Real st 0 < a holds Ball(0.X,a*r) = a
* Ball(0.X,r)
proof
let r,a be Real;
assume
A1: 0 < a;
thus Ball(0.X,a*r) c= a * Ball(0.X,r)
proof
let z be object;
assume
A2: z in Ball(0.X,a*r);
then reconsider z1=z as Point of X;
ex zz1 be Point of X st z1=zz1 & ||.0.X-zz1.|| < a*r by A2;
then ||.-z1.|| < a*r by RLVECT_1:14;
then ||.z1.|| < a*r by NORMSP_1:2;
then a"* ||.z1.|| < a"* (a*r) by A1,XREAL_1:68;
then a"* ||.z1.|| < (a*a")*r;
then
A3: a"* ||.z1.|| < 1*r by A1,XCMPLX_0:def 7;
set y1=a"*z1;
||.y1.|| = |.a".|* ||.z1.|| by NORMSP_1:def 1
.= a"* ||.z1.|| by A1,ABSVALUE:def 1;
then ||.-y1.|| < r by A3,NORMSP_1:2;
then ||.0.X-y1.|| < r by RLVECT_1:14;
then
A4: y1 in Ball(0.X,r);
a*y1=a*a"*z1 by RLVECT_1:def 7
.= 1*z1 by A1,XCMPLX_0:def 7
.= z1 by RLVECT_1:def 8;
hence thesis by A4;
end;
let z be object;
assume
A5: z in a*Ball(0.X,r);
then reconsider z1 = z as Point of X;
consider y1 be Point of X such that
A6: z1=a * y1 and
A7: y1 in Ball(0.X,r) by A5;
ex yy1 be Point of X st y1=yy1 & ||.0.X-yy1.||0 by XREAL_1:20;
then 0 < |.1-s.| by ABSVALUE:def 1;
then |.1-s.|*||.x-v.|| < |.1-s.|*r by A6,XREAL_1:68;
then
|.s.|*||.x-u.|| + |.1-s.|*||.x-v.|| < |.s.|*r + |.1-s.|*r by A7,
XREAL_1:8;
then |.s.|*||.x-u.|| + |.1-s.|*||.x-v.|| < s*r + |.1-s.|*r by A2,
ABSVALUE:def 1;
then |.s.|*||.x-u.|| + |.1-s.|*||.x-v.|| < s*r + (1-s)*r by A8,
ABSVALUE:def 1;
then ||.s*(x-u).|| + |.1-s.|*||.x-v.|| < 1* r by NORMSP_1:def 1;
then
A9: ||.s*(x-u).|| + ||.(1-s)*(x-v).|| < r by NORMSP_1:def 1;
||.s*x +(1-s)*x -(s*u + (1-s)*v).|| = ||.s*x +(-(s*u + (1-s)*v))+(1-s)
*x.|| by RLVECT_1:def 3
.= ||.s*x +(-1)*(s*u + (1-s)*v) +(1-s)*x.|| by RLVECT_1:16
.= ||.s*x + ((-1)*(s*u) +(-1)*((1-s)*v)) +(1-s)*x.|| by RLVECT_1:def 5
.= ||.s*x + (-s*u +(-1)*((1-s)*v)) +(1-s)*x.|| by RLVECT_1:16
.= ||.s*x + (-s*u +-(1-s)*v) + (1-s)*x.|| by RLVECT_1:16
.= ||.(s*x + -s*u) +-(1-s)*v + (1-s)*x.|| by RLVECT_1:def 3
.= ||.s*x - s*u + ((1-s)*x -(1-s)*v).|| by RLVECT_1:def 3
.= ||.s* (x - u) + ((1-s)*x -(1-s)*v).|| by RLVECT_1:34
.= ||.s* (x - u) + (1-s)*(x -v).|| by RLVECT_1:34;
then
||.s*x +(1-s)*x -(s*u + (1-s)*v).|| <= ||.s*(x-u).|| + ||.(1-s)*(x-v)
.|| by NORMSP_1:def 1;
then ||.s*x +(1-s)*x -(s*u + (1-s)*v).|| < r by A9,XXREAL_0:2;
then ||.(s+(1-s))*x -(s*u + (1-s)*v).|| < r by RLVECT_1:def 6;
then ||.x -(s*u + (1-s)*v).|| < r by RLVECT_1:def 8;
hence thesis;
end;
assume
A10: V = Ball(x,r);
for u,v being Point of LinearTopSpaceNorm X,
s being Real st 0 < s & s
< 1 & u in V & v in V holds s*u + (1-s)*v in V
proof
let u,v being Point of LinearTopSpaceNorm X;
let s being Real;
reconsider u1=u as Point of X by NORMSP_2:def 4;
reconsider v1=v as Point of X by NORMSP_2:def 4;
s*u1 = s*u & (1-s)*v1 =(1-s)*v by NORMSP_2:def 4;
then
A11: s*u1 + (1-s)*v1 = s*u + (1-s)*v by NORMSP_2:def 4;
assume 0 < s & s < 1 & u in V & v in V;
hence thesis by A10,A1,A11;
end;
hence thesis;
end;
theorem Th13:
for x be Point of X,r be Real, T be LinearOperator of X,Y
, V be Subset of LinearTopSpaceNorm Y st V = T.: Ball(x,r) holds V is convex
proof
let x be Point of X,r be Real, T be LinearOperator of X,Y, V be
Subset of LinearTopSpaceNorm Y;
reconsider V1 = T.: Ball(x,r) as Subset of Y;
A1: for u,v being Point of Y, s being Real
st 0 < s & s <1 & u in V1 & v in
V1 holds s*u + (1-s)*v in V1
proof
reconsider Bxr =Ball(x,r) as Subset of LinearTopSpaceNorm X by
NORMSP_2:def 4;
let u,v being Point of Y, s being Real;
assume that
A2: 0 < s & s < 1 and
A3: u in V1 and
A4: v in V1;
consider z1 be object such that
A5: z1 in the carrier of X and
A6: z1 in Ball(x,r) and
A7: u= T.z1 by A3,FUNCT_2:64;
reconsider zz1=z1 as Point of X by A5;
reconsider za1=zz1 as Point of LinearTopSpaceNorm X by NORMSP_2:def 4;
consider z2 be object such that
A8: z2 in the carrier of X and
A9: z2 in Ball(x,r) and
A10: v= T.z2 by A4,FUNCT_2:64;
reconsider zz2=z2 as Point of X by A8;
A11: (1-s)*v=T.((1-s)*zz2) by A10,LOPBAN_1:def 5;
reconsider za2=zz2 as Point of LinearTopSpaceNorm X by NORMSP_2:def 4;
s*za1 =s*zz1 & (1-s)*za2 =(1-s)*zz2 by NORMSP_2:def 4;
then
A12: s*za1 + (1-s)*za2=s*zz1 + (1-s)*zz2 by NORMSP_2:def 4;
s*u=T.(s*zz1) by A7,LOPBAN_1:def 5;
then
A13: s*u + (1-s)*v =T.(s*zz1 + (1-s)*zz2) by A11,VECTSP_1:def 20;
Bxr is convex by Th12;
then s*za1 + (1-s)*za2 in Bxr by A2,A6,A9;
hence thesis by A12,A13,FUNCT_2:35;
end;
assume
A14: V = T.: Ball(x,r);
for u,v being Point of LinearTopSpaceNorm Y,
s being Real st 0 < s & s
< 1 & u in V & v in V holds s*u + (1-s)*v in V
proof
let u,v being Point of LinearTopSpaceNorm Y;
let s be Real;
reconsider u1=u as Point of Y by NORMSP_2:def 4;
reconsider v1=v as Point of Y by NORMSP_2:def 4;
s*u1 =s*u & (1-s)*v1 =(1-s)*v by NORMSP_2:def 4;
then
A15: s*u1 + (1-s)*v1 =s*u + (1-s)*v by NORMSP_2:def 4;
assume 0 < s & s < 1 & u in V & v in V;
hence thesis by A14,A1,A15;
end;
hence thesis;
end;
theorem Th14:
for x be Point of X, r, s be Real st r <= s holds Ball(x,
r) c= Ball(x,s)
proof
let x be Point of X, r, s be Real;
assume
A1: r <=s;
for u being Point of X st u in Ball(x,r) holds u in Ball(x,s)
proof
let u be Point of X;
assume u in Ball(x,r);
then ex uu1 be Point of X st u=uu1 & ||.x-uu1.|| < r;
then ||.x-u.|| + r < r + s by A1,XREAL_1:8;
then ||.x-u.|| < r + s - r by XREAL_1:20;
hence thesis;
end;
hence thesis;
end;
:: Open Mapping lemma
theorem Th15:
for X be RealBanachSpace, Y be RealNormSpace, T be Lipschitzian
LinearOperator of X,Y, r be Real, BX1 be Subset of LinearTopSpaceNorm X,
TBX1,BYr be Subset of LinearTopSpaceNorm Y st r>0 & BYr=Ball(0.Y,r ) & TBX1=T.:
Ball(0.X,1) & BYr c= Cl (TBX1) holds BYr c= TBX1
proof
let X be RealBanachSpace, Y be RealNormSpace,
T be Lipschitzian LinearOperator of
X,Y, r be Real, BX1 be Subset of LinearTopSpaceNorm X, TBX1,BYr be
Subset of LinearTopSpaceNorm Y;
assume that
A1: r>0 and
A2: BYr=Ball(0.Y,r ) and
A3: TBX1=T.: Ball(0.X,1) and
A4: BYr c= Cl (TBX1);
A5: for x be Point of X,y be Point of Y, TB1, BYsr be Subset of
LinearTopSpaceNorm Y, s be Real st s >0 & TB1=T.: Ball(x,s) & y=T.x &
BYsr =Ball(y,s*r) holds BYsr c= Cl (TB1)
proof
reconsider TB01 = T.: Ball(0.X,1) as Subset of Y;
let x be Point of X, y be Point of Y, TB1, BYsr be Subset of
LinearTopSpaceNorm Y, s be Real;
assume that
A6: s >0 and
A7: TB1=T.: Ball(x,s) and
A8: y=T.x and
A9: BYsr =Ball(y,s*r);
reconsider s1 = s as non zero Real by A6;
reconsider y1=y as Point of LinearTopSpaceNorm Y by NORMSP_2:def 4;
A10: Ball(y,s*r) =y + Ball(0.Y,s*r) by Th2;
reconsider TB0xs = T.: Ball(x,s) as Subset of Y;
reconsider TB0s = T.: Ball(0.X,s) as Subset of Y;
Ball(x,s) = x+Ball(0.X,s) by Th2;
then
A11: y+TB0s = TB0xs by A8,Th6;
s1*BYr c= s1*Cl (TBX1) by A4,CONVEX1:39;
then s1*BYr c= Cl (s1*TBX1) by RLTOPSP1:52;
then y1+s1*BYr c= y1+Cl (s1*TBX1) by RLTOPSP1:8;
then
A12: y1+s1*BYr c= Cl (y1+s1*TBX1) by RLTOPSP1:38;
Ball(0.Y,s*r)=s1*Ball(0.Y,r) by A6,Th3;
then Ball(0.Y,s*r) = s1*BYr by A2,Th9;
then
A13: y1+s1*BYr=BYsr by A9,A10,Th8;
A14: s1*Ball(0.X,1)= Ball(0.X,s1*1) by A6,Th3;
s1*TB01 =s1* TBX1 by A3,Th9;
hence thesis by A7,A12,A13,A11,A14,Th5,Th8;
end;
A15: for s0 be Real st s0 >0 holds Ball(0.Y,r ) c= T.: Ball(0.X,1+s0)
proof
let s0 be Real;
assume
A16: s0 >0;
now
let z be object;
assume
A17: z in Ball(0.Y,r);
then reconsider y =z as Point of Y;
consider s1 be Real such that
A18: 0 < s1 and
A19: s1 < s0 by A16,XREAL_1:5;
set a=s1/(1+s1);
set e= a GeoSeq;
A20: a<1 by A18,XREAL_1:29,191;
then
A21: |.a.| < 1 by A18,ABSVALUE:def 1;
then
A22: e is summable by SERIES_1:24;
defpred P[Nat,Point of X,Point of X, Point of X] means $3 in
Ball($2,e.$1) & ||.T.$3-y.|| < e.($1+1)*r implies $4 in Ball($3,e.($1+1)) & ||.
T.$4-y.|| < e.($1+2)*r;
reconsider B0 =Ball(y,e.1*r) as Subset of LinearTopSpaceNorm Y by
NORMSP_2:def 4;
A23: 0 0
ex q be Real st 0 < q & Ball (0.Y,q) c=T.:
Ball(0.X,p)
proof
reconsider TB1 =T.: Ball(0.X,1) as Subset of Y;
let p be Real;
assume
A35: p > 0;
then
A36: p*Ball(0.X,1)= Ball(0.X,p*1) by Th3;
take r/(2*n0+2)*p;
p* Ball (0.Y,r/(2*n0+2)) c= p*TB1 by A33,CONVEX1:39;
then Ball (0.Y,r/(2*n0+2)*p) c= p*TB1 by A35,Th3;
hence thesis by A31,A35,A36,Th5,XREAL_1:129;
end;
assume
A37: G is open;
now
let y be Point of Y;
assume y in T1.:G;
then consider x be Point of X such that
A38: x in G and
A39: y=T.x by A1,FUNCT_2:65;
consider p be Real such that
A40: p>0 and
A41: {z where z is Point of X: ||.x-z.|| < p} c= G by A37,A38,NORMSP_2:22;
reconsider TBp =T.: Ball(0.X,p) as Subset of Y;
consider q be Real such that
A42: 0 < q and
A43: Ball (0.Y,q) c=TBp by A34,A40;
Ball(x,p) c= G by A41;
then
A44: x+Ball(0.X,p) c= G by Th2;
now
let t be object;
assume t in y + TBp;
then consider tz0 be Point of Y such that
A45: t=y+tz0 and
A46: tz0 in TBp;
consider z0 be Element of X such that
A47: z0 in Ball(0.X,p) and
A48: tz0=T.z0 by A46,FUNCT_2:65;
reconsider z0 as Point of X;
A49: x+ z0 in x+Ball(0.X,p) by A47;
t=T.(x+z0) by A39,A45,A48,VECTSP_1:def 20;
hence t in T1.:G by A1,A44,A49,FUNCT_2:35;
end;
then
A50: y + TBp c= T.: G by A1;
take q;
now
let t be object;
assume t in y + Ball(0.Y,q);
then ex z0 be Point of Y st t= y + z0 & z0 in Ball(0.Y,q);
hence t in y + TBp by A43;
end;
then y + Ball (0.Y,q) c= y+ TBp;
then Ball (y,q) c= y+ TBp by Th2;
hence 0 < q & {w where w is Point of Y: ||.y-w.|| < q } c= T1.:G by A1
,A50,A42;
end;
hence thesis by NORMSP_2:22;
end;
end;