:: Open Mapping Theorem
:: by Hideki Sakurai , Hisayoshi Kunimune and Yasunari Shidama
::
:: Received September 23, 2008
:: Copyright (c) 2008 Association of Mizar Users
environ
vocabularies TARSKI, BOOLE, RLVECT_1, FUNCT_1, PRE_TOPC, ARYTM, ABSVALUE,
ARYTM_1, FCONT_1, FINSEQ_4, ARYTM_3, RELAT_1, SEQ_2, LATTICES, OPPCAT_1,
ORDINAL2, NORMSP_1, PREPOWER, METRIC_1, NORMSP_2, PROB_1, RSSPACE3,
LOPBAN_1, SUPINF_2, JORDAN1, MCART_1, GROUP_1, XREAL_0, SGRAPH1;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, FUNCT_1, RELSET_1,
FUNCT_2, PARTFUN1, MCART_1, FUNCOP_1, PRE_TOPC, DOMAIN_1, BINOP_1,
ORDINAL1, ORDINAL2, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1,
STRUCT_0, XXREAL_0, SEQ_1, SEQ_2, INT_1, NEWTON, PREPOWER, SERIES_1,
RLVECT_1, FRAENKEL, CONVEX1, METRIC_1, RUSUB_4, NORMSP_1, NORMSP_2,
RSSPACE3, RLTOPSP1, LOPBAN_1, NFCONT_1, LOPBAN_5, KURATO_2, T_0TOPSP;
constructors XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL2, TOPS_1, REAL_1, DOMAIN_1,
SEQ_1, SEQ_2, PCOMPS_1, RUSUB_4, CONVEX1, RLTOPSP1, NFCONT_1, NAT_1,
FUNCT_1, FUNCT_2, PSCOMP_1, PARTFUN1, NEWTON, PREPOWER, SERIES_1,
NORMSP_2, RSSPACE3, LOPBAN_1, LOPBAN_5, T_0TOPSP;
registrations REAL_1, NUMBERS, ORDINAL2, XREAL_0, ZFMISC_1, XBOOLE_0,
METRIC_1, SERIES_1, XXREAL_0, ORDINAL1, RELSET_1, STRUCT_0, MEMBERED,
RLTOPSP1, TOPS_1, KURATO_2, SUBSET_1, NAT_1, RLVECT_1, NORMSP_1,
NORMSP_2, FUNCT_1, FUNCT_2, FUNCOP_1, RSSPACE3, SEQM_3, PARTFUN1,
MONOID_0, PROB_1, LOPBAN_1, LOPBAN_5, T_0TOPSP;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, RLVECT_1, METRIC_1, PCOMPS_1, CONVEX1, RUSUB_4, T_0TOPSP,
XREAL_0, RLSUB_1, ALGSTR_0, ZFMISC_1, RLTOPSP1, NORMSP_2, XBOOLE_0,
RSSPACE3, ORDINAL1, BHSP_1, SEQ_2, SERIES_1, PREPOWER, SUBSET_1,
FRAENKEL, LOPBAN_1, LOPBAN_5, NFCONT_1, MEMBERED, FUNCT_1, FUNCT_2;
theorems TARSKI, XBOOLE_1, SEQ_2, RLVECT_1, XREAL_0, 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,
SUBSET_1, RSSPACE2, LOPBAN_1, NAT_1, REAL_2, PROB_1, LOPBAN_5, CONVEX1,
MCART_1;
schemes FUNCT_2, RECDEF_1, NAT_1;
begin
theorem Lm00:
for x,y be real number st 0<=x & x non empty set, A() -> Element of D(),
B() -> Element of D(), P[set,set,set,set]}:
ex f being Function of NAT,D() st
f.0 = A() & f.1 = B() &
for n being Element of NAT holds P[n,f.n,f.(n+1),f.(n+2)]
provided
P0: for n being Element of 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;
P1: for n being Element of NAT for x being Element of [:D(),D() :]
ex y being Element of [:D(),D() :]
st Q[n,x,y]
proof
let n be Element of 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
P2: P[n,z,w,s] by P0;
set y = [w,s];
reconsider y as Element of [:D(),D() :];
take y;
thus Q[n,x,y] by P2,MCART_1:7;
end;
consider g being Function of NAT,[:D(),D() :] such that
P2: g.0 = [A(),B()] &
for n being Element of NAT holds Q[n,g.n,g.(n+1)]
from RECDEF_1:sch 2(P1);
deffunc F(Element of NAT)=(g.$1)`1;
P3: for x being Element of NAT holds F(x) in D();
consider f being Function of NAT,D() such that
P4: for x being Element of NAT holds f.x = F(x)
from FUNCT_2:sch 8(P3);
take f;
P5:Q[0,g.0,g.(0+1)] by P2;
EA1: f.0 = (g.0)`1 by P4
.= A() by MCART_1:7,P2;
EA2: f.1 = (g.1)`1 by P4
.= B() by MCART_1:7,P2,P5;
now let n be Element of NAT;
P6:Q[n+1,g.(n+1),g.((n+1)+1)] by P2;
E1: f.n = (g.n)`1 by P4;
E2: f.(n+1) = (g.(n+1))`1 by P4
.=(g.n)`2 by P2;
f.(n+2) =(g.(n+1))`2 by P6,P4;
hence P[n, f.n,f.(n+1), f.(n+2)] by P2,E1,E2;
end;
hence thesis by EA1,EA2;
end;
reserve X, Y for RealNormSpace;
theorem Lm01:
for y1 be Point of X, r be real number
holds Ball(y1,r) = y1 + Ball(0.X,r)
proof
let y1 be Point of X, r be real number;
thus Ball(y1,r) c=y1 + Ball(0.X,r)
proof
let t be set;
assume A1: t in Ball(y1,r);
reconsider z1=t as Point of X by A1;
set z0=z1-y1;
ex zz1 be Point of X st z1=zz1 & ||.y1-zz1.|| < r by A1;
then ||.-z0.|| < r by RLVECT_1:47;
then ||.0.X-z0.||< r by RLVECT_1:27;
then
A2: z0 in Ball(0.X,r);
z0+y1=z1+((-y1)+y1) by RLVECT_1:def 6;
then z0+y1=z1+0.X by RLVECT_1:16;
then z1=z0+y1 by RLVECT_1:10;
hence t in y1 + Ball(0.X,r) by A2;
end;
let t be set;
assume t in y1 + Ball(0.X,r);
then consider z0 be Point of X such that
B1: t=y1+z0 & z0 in Ball(0.X,r);
set z1=z0+y1;
ex zz0 be Point of X st
z0=zz0 & ||.0.X-zz0.|| < r by B1;
then ||.-z0.|| < r by RLVECT_1:27;
then ||.z0.|| < r by NORMSP_1:6;
then ||.z0+ 0.X.|| < r by RLVECT_1:10;
then ||.z0+ (y1+-y1).|| < r by RLVECT_1:16;
then ||.z1-y1.|| < r by RLVECT_1:def 6;
then ||.y1-z1.|| < r by NORMSP_1:11;
hence t in Ball(y1,r) by B1;
end;
theorem Lm02:
for r be real number, a be Real st 0 < a
holds Ball(0.X,a*r) = a * Ball(0.X,r)
proof
let r be real number, a be Real;
assume AS: 0 < a;
thus Ball(0.X,a*r) c= a * Ball(0.X,r)
proof
let z be set;
assume
R1: 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 R1;
then ||.-z1.|| < a*r by RLVECT_1:27;
then
R2: ||.z1.|| < a*r by NORMSP_1:6;
set y1=a"*z1;
R4: ||.y1.|| = abs(a")* ||.z1.|| by NORMSP_1:def 2
.= a"* ||.z1.|| by AS, ABSVALUE:def 1;
a"* ||.z1.|| < a"* (a*r) by R2,AS,XREAL_1:70;
then a"* ||.z1.|| < (a*a")*r;
then a"* ||.z1.|| < 1*r by XCMPLX_0:def 7,AS;
then ||.-y1.|| < r by NORMSP_1:6,R4;
then ||.0.X-y1.|| < r by RLVECT_1:27;
then
RA1: y1 in Ball(0.X,r);
a*y1=a*a"*z1 by RLVECT_1:def 9
.= 1*z1 by XCMPLX_0:def 7,AS
.= z1 by RLVECT_1:def 9;
hence z in a * Ball(0.X,r) by RA1;
end;
let z be set;
assume
L1: z in a*Ball(0.X,r);
reconsider z1 = z as Point of X by L1;
consider y1 be Point of X such that
B1: z1=a * y1 & y1 in Ball(0.X,r) by L1;
ex yy1 be Point of X st
y1=yy1 & ||.0.X-yy1.||0 by XREAL_1:22;
A4: ||.s*x +(1-s)*x -(s*u + (1-s)*v).||
= ||.s*x +(-(s*u + (1-s)*v))+(1-s)*x.|| by RLVECT_1:def 6
.= ||.s*x +(-1)*(s*u + (1-s)*v) +(1-s)*x.|| by RLVECT_1:29
.= ||.s*x + ((-1)*(s*u) +(-1)*((1-s)*v)) +(1-s)*x.|| by RLVECT_1:def 9
.= ||.s*x + (-s*u +(-1)*((1-s)*v)) +(1-s)*x.|| by RLVECT_1:29
.= ||.s*x + (-s*u +-(1-s)*v) + (1-s)*x.|| by RLVECT_1:29
.= ||.(s*x + -s*u) +-(1-s)*v + (1-s)*x.|| by RLVECT_1:def 6
.= ||.s*x - s*u + ((1-s)*x -(1-s)*v).|| by RLVECT_1:def 6
.= ||.s* (x - u) + ((1-s)*x -(1-s)*v).|| by RLVECT_1:48
.= ||.s* (x - u) + (1-s)*(x -v).|| by RLVECT_1:48;
A7: 0 < abs(s) by ABSVALUE:def 1,A2;
A8: 0 < abs(1-s) by ABSVALUE:def 1,AX1;
AZ1: ex u1 be Point of X st
u =u1 & ||.x-u1.||0 & BX1=Ball(0.X,1) & 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 bounded LinearOperator of X,Y,
r be real number,
BX1 be Subset of LinearTopSpaceNorm X,
TBX1,BYr be Subset of LinearTopSpaceNorm Y;
assume
AS0: r>0 & BX1=Ball(0.X,1) & BYr=Ball(0.Y,r )
& TBX1=T.: Ball(0.X,1) & BYr c= Cl (TBX1);
A1: for x be Point of X,y be Point of Y,
TB1, BYsr be Subset of LinearTopSpaceNorm Y,
s be real number
st s >0 & TB1=T.: Ball(x,s) & y=T.x
& BYsr =Ball(y,s*r)
holds BYsr c= Cl (TB1)
proof
let x be Point of X, y be Point of Y,
TB1, BYsr be Subset of LinearTopSpaceNorm Y,
s be real number;
assume
A2: s >0 & TB1=T.: Ball(x,s) & y=T.x & BYsr =Ball(y,s*r);
reconsider TB0 = T.:Ball(0.X,s)
as Subset of LinearTopSpaceNorm Y by NORMSP_2:def 4;
reconsider x1=x as Point of LinearTopSpaceNorm X by NORMSP_2:def 4;
reconsider y1=y as Point of LinearTopSpaceNorm Y by NORMSP_2:def 4;
reconsider s1 = s as non zero Real by A2,XREAL_0:def 1;
s1*BYr c= s1*Cl (TBX1) by AS0,CONVEX1:39;
then s1*BYr c= Cl (s1*TBX1) by RLTOPSP1:53;
then y1+s1*BYr c= y1+Cl (s1*TBX1) by RLTOPSP1:8;
then
P1: y1+s1*BYr c= Cl (y1+s1*TBX1) by RLTOPSP1:39;
Q1: Ball(y,s*r) =y + Ball(0.Y,s*r) by Lm01;
Ball(0.Y,s*r)=s1*Ball(0.Y,r) by A2,Lm02; then
Ball(0.Y,s*r) = s1*BYr by Lm06,AS0; then
P2: y1+s1*BYr=BYsr by A2,Q1,Lm05;
reconsider TB0s = T.: Ball(0.X,s) as Subset of Y;
reconsider TB01 = T.: Ball(0.X,1) as Subset of Y;
reconsider TB0xs = T.: Ball(x,s) as Subset of Y;
Ball(x,s) = x+Ball(0.X,s) by Lm01; then
Q3: y+TB0s = TB0xs by A2,Lm03;
Q4:s1*TB01 =s1* TBX1 by AS0,Lm06;
s1*Ball(0.X,1)= Ball(0.X,s1*1) by A2,Lm02;
hence thesis by P1,P2,Q3,A2,Lm05,Q4,Lm032;
end;
B1: for s0 be real number st s0 >0 holds
Ball(0.Y,r ) c= T.: Ball(0.X,1+s0)
proof
let s0 be real number;
assume C1:s0 >0;
now let z be set;
assume
C2: z in Ball(0.Y,r); then
reconsider y =z as Point of Y;
consider s1 be real number such that
C21: 0 < s1 & s1 < s0 by C1,XREAL_1:7;
set a=s1/(1+s1);
set e= a GeoSeq;
C23:0 0 ex q be Real st
0 < q & Ball (0.Y,q) c=T.: Ball(0.X,p)
proof
let p be Real;
assume P61: p > 0;
reconsider TB1 =T.: Ball(0.X,1) as Subset of Y;
P610:p*Ball(0.X,1)= Ball(0.X,p*1) by P61,Lm02;
p* Ball (0.Y,r/(2*n0+2)) c= p*TB1 by P5,CONVEX1:39; then
P612: Ball (0.Y,r/(2*n0+2)*p) c= p*TB1 by P61,Lm02;
take q=r/(2*n0+2)*p;
thus thesis by P61,P610,P612,Lm032,Q5,XREAL_1:131;
end;
now let y be Point of Y;
assume P7: y in T1.:G;
consider x be Point of X such that
P8: x in G & y=T.x by P7,AS0,FUNCT_2:116;
consider p be Real such that
P9: p>0 & {z where z is Point of X: ||.x-z.|| < p} c= G
by NORMSP_2:22,P8,AA1;
Ball(x,p) c= G by P9; then
P11: x+Ball(0.X,p) c= G by Lm01;
reconsider TBp =T.: Ball(0.X,p) as Subset of Y;
now let t be set;
assume t in y + TBp; then
consider tz0 be Point of Y such that
AB0: t=y+tz0 & tz0 in TBp;
consider z0 be Element of the carrier of X such that
AB1: z0 in Ball(0.X,p) & tz0=T.z0 by AB0,FUNCT_2:116;
reconsider z0 as Point of X;
A2: x+ z0 in x+Ball(0.X,p) by AB1;
t=T.(x+z0) by AB0,AB1,P8,LOPBAN_1:def 5;
hence t in T1.:G by A2,P11,AS0,FUNCT_2:43;
end; then
Q11: y + TBp c= T.: G by AS0,TARSKI:def 3;
consider q be Real such that
P12: 0 < q & Ball (0.Y,q) c=TBp by P6,P9;
take q;
now let t be set;
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 P12;
end;
then y + Ball (0.Y,q) c= y+ TBp by TARSKI:def 3;
then Ball (y,q) c= y+ TBp by Lm01;
hence 0 < q & {w where w is Point of Y: ||.y-w.|| < q } c= T1.:G
by AS0,Q11,XBOOLE_1:1,P12;
end;
hence T1.:G is open by NORMSP_2:22;
end;
end;