:: Open Mapping Theorem
:: by Hideki Sakurai , Hisayoshi Kunimune and Yasunari Shidama
::
:: Received September 23, 2008
:: Copyright (c) 2008-2026 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<y ex s0 be Real st 0<s0
& x < y/(1+s0) & y/(1+s0) < y
proof
let x,y be Real;
assume that
A1: 0<=x and
A2: x<y;
ex s0 be Real st 0<s0 & x < y/(1+s0) & y/(1+s0) < y
proof
consider s be Real such that
A3: x < s and
A4: s < y by A2,XREAL_1:5;
now
per cases by A1;
case
A5: 0=x;
set s0=s;
y < y*(1+s0) by A1,A3,A4,XREAL_1:29,155;
hence 0<s0 & x < y/(1+s0) & y/(1+s0) < y by A3,A4,A5,XREAL_1:83,139;
end;
case
A6: 0<x;
set s0=s /x - 1;
A7: (1+s0)"=1/(1+s0) by XCMPLX_1:215;
then
A8: s*(1+s0)"= (s*1)/(1+s0) by XCMPLX_1:74;
(1+s0)*x=(x/x)*s by XCMPLX_1:75;
then (1+s0)*x=1*s by A6,XCMPLX_1:60;
then
A9: (1+s0)"*(1+s0)*x=s*(1+s0)";
0 < 1+s0 by A3,A6,XREAL_1:187;
then
A10: (1+s0)"*(1+s0)=1 by A7,XCMPLX_1:106;
A11: 1< 1+s0 by A3,A6,XREAL_1:187;
then y < y*(1+s0) by A1,A2,XREAL_1:155;
hence 0<s0 & x < y/(1+s0) & y/(1+s0) < y by A4,A11,A9,A10,A8,XREAL_1:50
,74,83;
end;
end;
hence thesis;
end;
hence thesis;
end;
scheme
RecExD3{D() -> 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.||<r by A7;
then ||.-y1.|| < r by RLVECT_1:14;
then
A8: ||.y1.|| < r by NORMSP_1:2;
||.z1.|| = |.a.|* ||.y1.|| by A6,NORMSP_1:def 1
.= a* ||.y1.|| by A1,ABSVALUE:def 1;
then ||.z1.|| < a*r by A1,A8,XREAL_1:68;
then ||.-z1.|| < a*r by NORMSP_1:2;
then ||.0.X-z1.|| < a*r by RLVECT_1:14;
hence thesis;
end;
theorem
for T be LinearOperator of X,Y, B0,B1 be Subset of X holds T.:(B0+B1)
= T.:B0+T.:B1
proof
let T be LinearOperator of X,Y, B0,B1 be Subset of X;
thus T.:(B0+B1) c= T.:B0+T.:B1
proof
let t be object;
assume t in T.:(B0+B1);
then consider z1 be object such that
z1 in the carrier of X and
A1: z1 in B0+B1 and
A2: t= T.z1 by FUNCT_2:64;
consider x1,x2 be Element of X such that
A3: z1=x1+x2 and
A4: x1 in B0 & x2 in B1 by A1;
A5: T.x1 in T.:B0 & T.x2 in T.:B1 by A4,FUNCT_2:35;
t=T.x1+T.x2 by A2,A3,VECTSP_1:def 20;
hence thesis by A5;
end;
let t be object;
assume t in T.:B0 + T.:B1;
then consider tz0,tz1 be Point of Y such that
A6: t=tz0+tz1 and
A7: tz0 in T.:B0 and
A8: tz1 in T.:B1;
consider z1 be Element of X such that
A9: z1 in B1 and
A10: tz1=T.z1 by A8,FUNCT_2:65;
consider z0 be Element of X such that
A11: z0 in B0 and
A12: tz0=T.z0 by A7,FUNCT_2:65;
reconsider z1 as Point of X;
reconsider z0 as Point of X;
A13: z0+z1 in B0+B1 by A11,A9;
t=T.(z0+z1) by A6,A12,A10,VECTSP_1:def 20;
hence thesis by A13,FUNCT_2:35;
end;
theorem Th5:
for T be LinearOperator of X,Y, B0 be Subset of X, a be Real
holds T.:(a*B0) = a*T.:B0
proof
let T be LinearOperator of X,Y, B0 be Subset of X, a be Real;
thus T.:(a*B0) c= a*T.:B0
proof
let t be object;
assume t in T.:(a*B0);
then consider z1 be object such that
z1 in the carrier of X and
A1: z1 in a*B0 and
A2: t= T.z1 by FUNCT_2:64;
consider x1 be Element of X such that
A3: z1=a*x1 and
A4: x1 in B0 by A1;
A5: T.x1 in T.:B0 by A4,FUNCT_2:35;
t=a* T.x1 by A2,A3,LOPBAN_1:def 5;
hence thesis by A5;
end;
let t be object;
assume t in a*T.:B0;
then consider tz0 be Point of Y such that
A6: t=a*tz0 and
A7: tz0 in T.:B0;
consider z0 be Element of X such that
A8: z0 in B0 and
A9: tz0=T.z0 by A7,FUNCT_2:65;
reconsider z0 as Point of X;
set z1=a*z0;
A10: z1 in a*B0 by A8;
t=T. z1 by A6,A9,LOPBAN_1:def 5;
hence thesis by A10,FUNCT_2:35;
end;
theorem Th6:
for T be LinearOperator of X,Y, B0 be Subset of X, x1 be Point of
X holds T.:(x1+ B0) = T.x1 + T.:B0
proof
let T be LinearOperator of X,Y, B0 be Subset of X, x1 be Point of X;
thus T.:(x1+ B0) c= T.x1 + T.:B0
proof
let t be object;
assume t in T.:(x1+ B0);
then consider z1 be object such that
A1: z1 in the carrier of X and
A2: z1 in x1+ B0 and
A3: t= T.z1 by FUNCT_2:64;
reconsider z1 as Point of X by A1;
consider z0 be Element of X such that
A4: z1=x1+ z0 and
A5: z0 in B0 by A2;
A6: T.z0 in T.:B0 by A5,FUNCT_2:35;
t=T.x1 + T.z0 by A3,A4,VECTSP_1:def 20;
hence thesis by A6;
end;
let t be object;
assume t in T.x1 + T.:B0;
then consider tz0 be Point of Y such that
A7: t=T.x1+tz0 and
A8: tz0 in T.:B0;
consider z0 be Element of X such that
A9: z0 in B0 and
A10: tz0=T.z0 by A8,FUNCT_2:65;
A11: x1+z0 in x1+B0 by A9;
t=T.(x1+z0) by A7,A10,VECTSP_1:def 20;
hence thesis by A11,FUNCT_2:35;
end;
theorem
for V,W be Subset of X, V1,W1 be Subset of LinearTopSpaceNorm X st V=
V1 & W=W1 holds V+W=V1+W1
proof
let V,W be Subset of X, V1,W1 be Subset of LinearTopSpaceNorm X such that
A1: V=V1 and
A2: W=W1;
thus V+W c= V1+W1
proof
let x be object;
assume x in V+W;
then consider u,v be Point of X such that
A3: x=u+v and
A4: u in V and
A5: v in W;
reconsider v1=v as Point of LinearTopSpaceNorm X by A2,A5;
reconsider u1=u as Point of LinearTopSpaceNorm X by A1,A4;
u+v=u1+v1 by NORMSP_2:def 4;
hence thesis by A1,A2,A3,A4,A5;
end;
let x be object;
assume x in V1+W1;
then consider u,v be Point of LinearTopSpaceNorm X such that
A6: x=u+v and
A7: u in V1 and
A8: v in W1;
reconsider v1=v as Point of X by A2,A8;
reconsider u1=u as Point of X by A1,A7;
u+v=u1+v1 by NORMSP_2:def 4;
hence thesis by A1,A2,A6,A7,A8;
end;
theorem Th8:
for V be Subset of X,x be Point of X, V1 be Subset of
LinearTopSpaceNorm X, x1 be Point of LinearTopSpaceNorm X st V=V1 & x=x1 holds
x+V=x1+V1
proof
let V be Subset of X,x be Point of X, V1 be Subset of LinearTopSpaceNorm X,
x1 be Point of LinearTopSpaceNorm X such that
A1: V=V1 and
A2: x=x1;
thus x+V c= x1+V1
proof
let z be object;
assume z in x+V;
then consider u be Point of X such that
A3: z=x+u and
A4: u in V;
reconsider u1=u as Point of LinearTopSpaceNorm X by A1,A4;
x+u=x1+u1 by A2,NORMSP_2:def 4;
hence thesis by A1,A3,A4;
end;
let z be object;
assume z in x1+V1;
then consider u1 be Point of LinearTopSpaceNorm X such that
A5: z=x1+u1 and
A6: u1 in V1;
reconsider u=u1 as Point of X by A1,A6;
x1+u1=x+u by A2,NORMSP_2:def 4;
hence thesis by A1,A5,A6;
end;
theorem Th9:
for V be Subset of X,a be Real, V1 be Subset of
LinearTopSpaceNorm X st V=V1 holds a*V=a*V1
proof
let V be Subset of X,a be Real,
V1 be Subset of LinearTopSpaceNorm X such
that
A1: V=V1;
thus a*V c=a*V1
proof
let z be object;
assume z in a*V;
then consider v be Point of X such that
A2: z=a*v and
A3: v in V;
reconsider v1=v as Point of LinearTopSpaceNorm X by A1,A3;
a*v=a*v1 by NORMSP_2:def 4;
hence thesis by A1,A2,A3;
end;
let z be object;
assume z in a*V1;
then consider v be Point of LinearTopSpaceNorm X such that
A4: z=a*v and
A5: v in V1;
reconsider v1=v as Point of X by A1,A5;
a*v=a*v1 by NORMSP_2:def 4;
hence thesis by A1,A4,A5;
end;
theorem Th10:
for V be Subset of TopSpaceNorm X, V1 be Subset of
LinearTopSpaceNorm X st V=V1 holds Cl(V)=Cl(V1)
proof
let V be Subset of TopSpaceNorm X, V1 be Subset of LinearTopSpaceNorm X such
that
A1: V=V1;
thus Cl(V) c= Cl(V1)
proof
let z be object;
assume
A2: z in Cl(V);
A3: for D1 be Subset of LinearTopSpaceNorm X st D1 is closed holds V1 c=
D1 implies z in D1
proof
let D1 be Subset of LinearTopSpaceNorm X such that
A4: D1 is closed;
reconsider D0=D1 as Subset of X by NORMSP_2:def 4;
reconsider D2=D1 as Subset of TopSpaceNorm X by NORMSP_2:def 4;
D0 is closed by A4,NORMSP_2:32;
then
A5: D2 is closed by NORMSP_2:15;
assume V1 c= D1;
hence thesis by A1,A2,A5,PRE_TOPC:15;
end;
z in the carrier of X by A2;
then z in the carrier of LinearTopSpaceNorm X by NORMSP_2:def 4;
hence thesis by A3,PRE_TOPC:15;
end;
let z be object;
assume
A6: z in Cl(V1);
A7: for D1 be Subset of TopSpaceNorm X st D1 is closed holds V c= D1
implies z in D1
proof
let D1 be Subset of TopSpaceNorm X such that
A8: D1 is closed;
reconsider D0=D1 as Subset of X;
reconsider D2=D1 as Subset of LinearTopSpaceNorm X by NORMSP_2:def 4;
D0 is closed by A8,NORMSP_2:15;
then
A9: D2 is closed by NORMSP_2:32;
assume V c= D1;
hence thesis by A1,A6,A9,PRE_TOPC:15;
end;
z in the carrier of LinearTopSpaceNorm X by A6;
then z in the carrier of TopSpaceNorm X by NORMSP_2:def 4;
hence thesis by A7,PRE_TOPC:15;
end;
theorem Th11:
for x be Point of X, r be Real holds Ball(0.X,r)=(-1)* Ball(0.X,r)
proof
let x be Point of X, r be Real;
thus Ball(0.X,r) c= (-1)*Ball(0.X,r)
proof
let z be object;
assume
A1: z in Ball(0.X,r);
then reconsider z1=z as Point of X;
ex zz1 be Point of X st z1=zz1 & ||.0.X-zz1.|| < r by A1;
then ||.-z1.|| < r by RLVECT_1:14;
then ||.-(-z1).|| < r by NORMSP_1:2;
then ||.0.X-(-z1).|| < r by RLVECT_1:14;
then
A2: -z1 in Ball(0.X,r);
(-1)*(-z1) =1*z1 by RLVECT_1:26
.=z1 by RLVECT_1:def 8;
hence thesis by A2;
end;
let z be object;
assume
A3: z in (-1)*Ball(0.X,r);
then reconsider z1=z as Point of X;
consider y1 be Point of X such that
A4: z1=(-1)* y1 and
A5: y1 in Ball(0.X,r) by A3;
ex zz1 be Point of X st y1 =zz1 & ||.0.X-zz1.||<r by A5;
then ||.-y1.|| < r by RLVECT_1:14;
then ||.-(-y1).|| < r by NORMSP_1:2;
then
A6: ||.0.X-(-y1).|| < r by RLVECT_1:14;
-y1 =z1 by A4,RLVECT_1:16;
hence thesis by A6;
end;
theorem Th12:
for x be Point of X,r be Real, V be Subset of
LinearTopSpaceNorm X st V = Ball(x,r) holds V is convex
proof
let x be Point of X,r be Real, V be Subset of LinearTopSpaceNorm X;
reconsider V1 = Ball(x,r) as Subset of X;
A1: for u,v being Point of X, s being Real
st 0 < s & s <1 & u in V1 & v in
V1 holds s*u + (1-s)*v in V1
proof
let u,v be Point of X, s be Real;
assume that
A2: 0 < s and
A3: s < 1 and
A4: u in V1 and
A5: v in V1;
A6: ex v1 be Point of X st v =v1 & ||.x-v1.||<r by A5;
0 < |.s.| & ex u1 be Point of X st u =u1 & ||.x-u1.||<r by A2,A4,
ABSVALUE:def 1;
then
A7: |.s.|*||.x-u.|| < |.s.|*r by XREAL_1:68;
s+0<1 by A3;
then
A8: 1-s >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<a by A18,XREAL_1:139;
then e.1=a|^1 & 0<a|^1 by PREPOWER:def 1;
then 0< e.1*r by A1,XREAL_1:129;
then ||.y-y.|| < e.1*r by NORMSP_1:6;
then B0 is open & y in B0 by NORMSP_2:23;
then Ball(y,e.1*r) meets TBX1 by A2,A4,A17,PRE_TOPC:def 7;
then consider s be object such that
A24: s in Ball(y,e.1*r) and
A25: s in T.: Ball(0.X,1) by A3,XBOOLE_0:3;
consider xn1 be object such that
A26: xn1 in the carrier of X and
A27: xn1 in Ball(0.X,1) and
A28: s = T.xn1 by A25,FUNCT_2:64;
reconsider xn1 as Point of X by A26;
A29: for n being Nat for v,w be Point of X ex z being Point
of X st P[n,v,w,z]
proof
let n being Nat;
let v,w be Point of X;
now
reconsider B0 = Ball(y,e.(n+2)*r) as Subset of LinearTopSpaceNorm Y
by NORMSP_2:def 4;
reconsider BYsr = Ball(T.w,e.(n+1)*r) as Subset of
LinearTopSpaceNorm Y by NORMSP_2:def 4;
reconsider TB1 = T.: Ball(w,e.(n+1)) as Subset of LinearTopSpaceNorm
Y by NORMSP_2:def 4;
assume that
w in Ball(v,e.n) and
A30: ||.T.w-y.|| < e.(n+1)*r;
e.(n+1)=a|^(n+1) by PREPOWER:def 1;
then
A31: BYsr c= Cl (TB1) by A5,A23,NEWTON:83;
e.(n+2)=a|^(n+2) & 0<a|^(n+2) by A23,NEWTON:83,PREPOWER:def 1;
then 0< e.(n+2)*r by A1,XREAL_1:129;
then ||.y-y.|| < e.(n+2)*r by NORMSP_1:6;
then
A32: B0 is open & y in B0 by NORMSP_2:23;
y in BYsr by A30;
then Ball(y,e.(n+2)*r) meets TB1 by A31,A32,PRE_TOPC:def 7;
then consider s be object such that
A33: s in Ball(y,e.(n+2)*r) and
A34: s in T.: Ball(w,e.(n+1)) by XBOOLE_0:3;
consider z be object such that
A35: z in the carrier of X and
A36: z in Ball(w,e.(n+1)) and
A37: s = T.z by A34,FUNCT_2:64;
reconsider z as Point of X by A35;
reconsider sb=T.z as Point of Y;
ex ss1 be Point of Y st sb=ss1 & ||.y-ss1.|| < e.(n+2)*r by A33,A37;
then ||.T.z-y.|| < e.(n+2)*r by NORMSP_1:7;
hence
ex z be Point of X st z in Ball(w,e.(n+1)) & ||.T.z-y.|| < e.(n
+2)*r by A36;
end;
hence thesis;
end;
consider xn be sequence of X such that
A38: xn.0 = 0.X & xn.1 = xn1 & for n being Nat holds P[n,
xn.n,xn.(n+1),xn.(n+2)] from RecExD3(A29);
reconsider sb=T.xn1 as Point of Y;
A39: ex ss1 be Point of Y st sb=ss1 & ||.y-ss1.|| < e.1*r by A24,A28;
A40: for n be Nat holds xn.(n+1) in Ball(xn.n,e.n) & ||.T.(xn
.(n+1))-y.|| < e.(n+1)*r
proof
defpred PN[Nat] means xn.($1+1) in Ball(xn.$1,e.$1) & ||.T.
(xn.($1+1))-y.|| < e.($1+1)*r;
A41: now
let n be Nat;
assume
A42: PN[n];
P[n,xn.n,xn.(n+1),xn.(n+2)] by A38;
hence PN[n+1] by A42;
end;
A43: PN[0] by A27,A39,A38,NORMSP_1:7,PREPOWER:3;
thus for n be Nat holds PN[n] from NAT_1:sch 2(A43, A41);
end;
A44: e.0 = 1 by PREPOWER:3;
A45: for m, k be Nat holds ||.xn.(m+k) - xn.m.|| <= e.m*((1-e
.k)/(1-e.1))
proof
let m be Nat;
defpred PN[Nat] means ||.xn.(m+$1) - xn.m.|| <= e.m*((1-e.
$1)/(1-e.1));
A46: now
let k be Nat;
A47: (a|^k-a|^(k+1))/(1-a|^1)+ (1-a|^k)/(1-a|^1) =(a|^k-a|^(k+1)+(1-a
|^k))/(1-a|^1) by XCMPLX_1:62
.=(1-a|^(k+1))/(1-a|^1);
assume PN[k];
then ||.xn.((m+k)+1) - xn.m.|| <= ||.xn.((m+k)+1) - xn.(m+k).|| +
||.xn.(m+k) - xn .m.|| & ||.xn.((m+k)+1) - xn.(m+k).|| + ||.xn.(m+k) - xn.m.||
<= ||.xn.((m+k)+ 1) - xn.(m+k).|| + e.m*((1-e.k)/(1-e.1)) by NORMSP_1:10
,XREAL_1:6;
then
A48: ||.xn.(m+(k+1)) - xn.m.|| <= ||.xn.((m+k)+1) - xn.(m+k).|| + e.
m*((1-e.k)/(1-e.1)) by XXREAL_0:2;
xn.(m+k+1) in Ball(xn.(m+k),e.(m+k)) by A40;
then
ex xn2 be Point of X st xn.((m+k)+1)=xn2 & ||.xn.(m+k) - xn2.||
< e.(m+k);
then ||.xn.((m+k)+1) - xn.(m+k).|| < e.(m+k) by NORMSP_1:7;
then
A49: ||.xn.((m+k)+1) - xn.(m+k).|| + e.m*((1-e.k)/(1-e.1)) <= e.(m+k
) + e.m*((1-e.k)/(1-e.1)) by XREAL_1:6;
a|^1<1 by A20;
then 0< 1-a|^1 by XREAL_1:50;
then
A50: a|^k=((a|^k)*(1-a|^1))/(1-a|^1) by XCMPLX_1:89
.=(a|^k-a|^k*a|^1)/(1-a|^1)
.=(a|^k-a|^(k+1))/(1-a|^1) by NEWTON:8;
e.(m+k)+e.m*((1-e.k)/(1-e.1)) = a|^(m+k)+e.m*((1-e.k)/(1-e.1))
by PREPOWER:def 1
.= a|^(m+k)+(a|^m)*((1-e.k)/(1-e.1)) by PREPOWER:def 1
.= a|^(m+k)+(a|^m)*((1-a|^k)/(1-e.1)) by PREPOWER:def 1
.= a|^(m+k)+(a|^m)*((1-a|^k)/(1-a|^1)) by PREPOWER:def 1
.=a|^m*a|^k + (a|^m)*((1-a|^k)/(1-a|^1)) by NEWTON:8
.=a|^m*((1-a|^(k+1))/(1-a|^1)) by A50,A47
.=e.m*((1-a|^(k+1))/(1-a|^1)) by PREPOWER:def 1
.=e.m*((1-e.(k+1))/(1-a|^1)) by PREPOWER:def 1
.=e.m*((1-e.(k+1))/(1-e.1)) by PREPOWER:def 1;
hence PN[k+1] by A48,A49,XXREAL_0:2;
end;
||.xn.(m+0) - xn.m.|| = ||.0.X.|| by RLVECT_1:5;
then
A51: PN[ 0] by A44;
for k be Nat holds PN[ k] from NAT_1:sch 2(A51,A46);
hence thesis;
end;
A52: for k be Nat st 0 <= k holds ||.xn.||.k <= 1/(1-a)
proof
let k be Nat;
assume 0 <= k;
A53: e.k = a|^k & e.1 = a|^1 by PREPOWER:def 1;
a|^1 < 1 by A20;
then
A54: 0< 1-a|^1 by XREAL_1:50;
1-a|^k <1 by A23,NEWTON:83,XREAL_1:44;
then (1-e.k)/(1-e.1) <= 1/(1-a|^1) by A53,A54,XREAL_1:74;
then
A55: (1-e.k)/(1-e.1) <= 1/(1-a );
||. xn.(0+k) - xn.0 .|| <= e.0*((1-e.k)/(1-e.1)) by A45;
then ||.xn.k .|| <= (1-e.k)/(1-e.1) by A44,A38,RLVECT_1:13;
then ||.xn.k .|| <= 1/(1-a ) by A55,XXREAL_0:2;
hence thesis by NORMSP_0:def 4;
end;
A56: Sum(e) = 1/(1-a) by A21,SERIES_1:24;
1/(1-a)=1/((1*(1+s1)-s1)/(1+s1)) by A18,XCMPLX_1:127
.=1+s1 by XCMPLX_1:100;
then
A57: Sum(e) < 1+s0 by A19,A56,XREAL_1:6;
set xx= lim xn;
A58: now
let m be Nat;
hereby
let k be Nat;
A59: 0 < a|^m by A23,NEWTON:83;
||.xn.(m+k)-xn.m.|| <= e.m*((1-e.k)/(1-e.1)) by A45;
then ||.xn.(m+k)-xn.m.|| <= a|^m*((1-e.k)/(1-e.1)) by PREPOWER:def 1;
then ||.xn.(m+k)-xn.m.|| <= a|^m*((1-a|^k)/(1-e.1)) by PREPOWER:def 1
;
then
A60: ||.xn.(m+k)-xn.m.|| <= a|^m*((1-a|^k)/(1-a|^1)) by PREPOWER:def 1;
a|^1 < 1 by A20;
then
A61: 0< 1-a|^1 by XREAL_1:50;
1-a|^k < 1 by A23,NEWTON:83,XREAL_1:44;
then (1-a|^k)/(1-a|^1)< 1/(1-a|^1) by A61,XREAL_1:74;
then a|^m*((1-a|^k)/(1-a|^1)) < a|^m*(1/(1-a|^1)) by A59,XREAL_1:68;
hence ||.xn.(m+k)-xn.m.|| < a|^m*(1/(1-a|^1)) by A60,XXREAL_0:2;
end;
end;
now
let r1 be Real;
A62: e is convergent & lim e =0 by A22,SERIES_1:4;
a|^1 < 1 by A20;
then
A63: 0< 1-a|^1 by XREAL_1:50;
assume 0 < r1;
then 0< r1*(1-a|^1) by A63,XREAL_1:129;
then consider p1 be Nat such that
A64: for m be Nat st p1<=m holds |.e.m-0 .|< r1*(1-a|^
1) by A62,SEQ_2:def 7;
reconsider p1 as Nat;
take m=p1;
|.e.p1-0 .|< r1*(1-a|^1) by A64;
then e.p1 < 0+r1*(1-a|^1) by RINFSUP1:1;
then e.p1/(1-a|^1) <r1*(1-a|^1)/(1-a|^1) by A63,XREAL_1:74;
then e.p1/(1-a|^1) < r1 by A63,XCMPLX_1:89;
then a|^p1/(1-a|^1) < r1 by PREPOWER:def 1;
then
A65: a|^p1*(1/(1-a|^1)) < r1 by XCMPLX_1:99;
hereby
let n be Nat;
assume m <= n;
then consider k1 be Nat such that
A66: n = m + k1 by NAT_1:10;
reconsider k1 as Nat;
n = m + k1 by A66;
hence ||.xn.n-xn.m.|| < r1 by A58,A65,XXREAL_0:2;
end;
end;
then xn is Cauchy_sequence_by_Norm by LOPBAN_3:5;
then
A67: xn is convergent by LOPBAN_1:def 15;
then lim ||.xn.|| = ||.lim xn.|| by LOPBAN_1:41;
then ||.xx .|| <= Sum(e) by A56,A67,A52,LOPBAN_1:41,RSSPACE2:5;
then ||.xx.|| < 1+s0 by A57,XXREAL_0:2;
then ||.-xx.|| < 1+s0 by NORMSP_1:2;
then ||.0.X-xx.|| < 1+s0 by RLVECT_1:14;
then
A68: xx in Ball(0.X,1+s0);
rng xn c= the carrier of X;
then
A69: rng xn c= dom T by FUNCT_2:def 1;
A70: now
let n be Nat;
A71: n in NAT by ORDINAL1:def 12;
thus (T/*xn).n=T/.(xn.n) by A69,FUNCT_2:109,A71
.=T.(xn.n);
end;
A72: now
let s be Real;
assume 0 < s;
then
A73: 0< s/r by A1,XREAL_1:139;
e is convergent & lim e =0 by A22,SERIES_1:4;
then consider m0 be Nat such that
A74: for n be Nat st m0<=n holds |.e.n-0 .|< s/r by A73,
SEQ_2:def 7;
reconsider m=m0+1 as Nat;
take m;
a|^1 < 1 & 0 < a|^m0 by A23,A20,NEWTON:83;
then a|^m0*a|^1 <= a|^m0 by XREAL_1:153;
then a|^(m0+1) <= a|^m0 by NEWTON:8;
then e.(m0+1) <= a|^m0 by PREPOWER:def 1;
then
A75: e.(m0+1) <= e.m0 by PREPOWER:def 1;
|.e.m0-0 .|< s/r by A74;
then e.m0 < 0+s/r by RINFSUP1:1;
then e.(m0+1)< s/r by A75,XXREAL_0:2;
then e.(m0+1)*r < s/r*r by A1,XREAL_1:68;
then
A76: e.(m0+1)*r < s by A1,XCMPLX_1:87;
now
let n be Nat;
assume
A77: m <= n;
1 <= m0+1 by NAT_1:11;
then reconsider n0= n-1 as Nat by A77,NAT_1:21,XXREAL_0:2;
consider m1 be Nat such that
A78: n0+1 = m0+1 + m1 by A77,NAT_1:10;
A79: a |^(n0+1) = a |^(m0+1) * a |^ m1 by A78,NEWTON:8;
0< a |^(m0+1) & a|^m1 <= 1|^m1 by A23,A20,NEWTON:83,PREPOWER:9;
then a |^(n0+1) <= a |^(m0+1) by A79,XREAL_1:153;
then e.(n0+1) <= a |^(m0+1) by PREPOWER:def 1;
then e.(n0+1) <= e.(m0+1) by PREPOWER:def 1;
then e.(n0+1)*r <= e.(m0+1)*r by A1,XREAL_1:64;
then ||.T.(xn.n)-y.|| <= e.(m0+1)*r by A40,XXREAL_0:2;
then ||.T.(xn.n)-y.|| < s by A76,XXREAL_0:2;
hence ||.(T/*xn).n-y.|| < s by A70;
end;
hence for n be Nat st m <= n holds ||.(T/*xn).n-y.|| < s;
end;
T is_continuous_in xx by LOPBAN_5:4;
then T/*xn is convergent & T/.xx = lim (T/*xn) by A67,A69,NFCONT_1:def 5;
then y=T.xx by A72,NORMSP_1:def 7;
hence z in T.:Ball(0.X,1+s0) by A68,FUNCT_2:35;
end;
hence thesis;
end;
now
reconsider TB01 = T.: Ball(0.X,1) as Subset of Y;
let z be object;
assume
A80: z in Ball(0.Y,r);
then reconsider y=z as Point of Y;
ex yy1 be Point of Y st y=yy1 & ||.0.Y-yy1.|| < r by A80;
then ||.-y.|| < r by RLVECT_1:14;
then
A81: ||.y.|| < r by NORMSP_1:2;
consider s0 be Real such that
A82: 0<s0 and
A83: ||.y.||< r/(1+s0) and
r/(1+s0) < r by A81,Th1;
set y1=(1+s0)*y;
(1+s0)*||.y.|| < r/(1+s0)*(1+s0) by A82,A83,XREAL_1:68;
then (1+s0)*||.y.|| < r by A82,XCMPLX_1:87;
then |.1+s0.|*||.y.|| < r by A82,ABSVALUE:def 1;
then ||.(1+s0)*y.|| < r by NORMSP_1:def 1;
then ||.-y1.|| < r by NORMSP_1:2;
then ||.0.Y-y1.|| < r by RLVECT_1:14;
then
A84: (1+s0)*y in Ball(0.Y,r);
Ball(0.Y,r) c= T.: Ball(0.X,1+s0) by A15,A82;
then
A85: (1+s0)*y in T.: Ball(0.X,1+s0) by A84;
reconsider s1=1+s0 as non zero Real by A82;
s1*Ball(0.X,1)= Ball(0.X,s1*1) by A82,Th3;
then s1*y in s1*TB01 by A85,Th5;
then s1"*(s1*y) in s1"*(s1*TB01);
then (s1"*s1)*y in s1"*(s1*TB01) by RLVECT_1:def 7;
then
A86: (s1"*s1)*y in (s1"*s1)*TB01 by CONVEX1:37;
s1"*s1=(1/s1)*s1 by XCMPLX_1:215
.=1 by XCMPLX_1:106;
then y in 1*TB01 by A86,RLVECT_1:def 8;
hence z in T.: Ball(0.X,1) by CONVEX1:32;
end;
hence thesis by A2,A3;
end;
:: Open Mapping Theorem
::$N Open Mapping Theorem
theorem
for X, Y be RealBanachSpace, T be Lipschitzian LinearOperator of X,Y, T1 be
Function of LinearTopSpaceNorm X,LinearTopSpaceNorm Y st T1=T & T1 is onto
holds T1 is open
proof
let X, Y be RealBanachSpace, T be Lipschitzian LinearOperator of X,Y, T1 be
Function of LinearTopSpaceNorm X,LinearTopSpaceNorm Y;
assume that
A1: T1=T and
A2: T1 is onto;
thus for G be Subset of LinearTopSpaceNorm X st G is open holds T1.:G is open
proof
reconsider TB1 = T.: Ball(0.X,1) as Subset of LinearTopSpaceNorm Y by
NORMSP_2:def 4;
defpred P[Nat, set] means ex TBn be Subset of TopSpaceNorm Y st
TBn=T.: Ball(0.X,$1) & $2=Cl(TBn);
let G be Subset of LinearTopSpaceNorm X;
A3: for n being Element of NAT ex y being Element of bool the carrier of Y
st P[n,y]
proof
let n being Element of NAT;
reconsider TBn = T.: Ball(0.X,n) as Subset of TopSpaceNorm Y;
Cl(TBn) c= the carrier of Y;
hence thesis;
end;
consider f be sequence of bool (the carrier of Y) such that
A4: for x being Element of NAT holds P[x,f.x] from FUNCT_2:sch 3(A3);
reconsider f as SetSequence of Y;
A5: for n be Nat holds f.n is closed
proof
let n be Nat;
n in NAT by ORDINAL1:def 12;
then
ex TBn be Subset of TopSpaceNorm Y st TBn=T.: Ball(0.X,n) & f.n=Cl(
TBn) by A4;
hence thesis by NORMSP_2:15;
end;
A6: the carrier of Y c= union rng f
proof
let z be object;
assume z in the carrier of Y;
then reconsider z1=z as Point of Y;
rng T = the carrier of (LinearTopSpaceNorm Y ) by A1,A2,FUNCT_2:def 3;
then rng T = the carrier of Y by NORMSP_2:def 4;
then consider x1 be object such that
A7: x1 in the carrier of X and
A8: z1=T.x1 by FUNCT_2:11;
reconsider x1 as Point of X by A7;
consider m be Element of NAT such that
A9: ||.x1.|| <= m by MESFUNC1:8;
set n=m+1;
||.x1.|| +0< m+1 by A9,XREAL_1:8;
then ||.-x1.|| < n by NORMSP_1:2;
then ||.0.X-x1.|| < n by RLVECT_1:14;
then x1 in Ball(0.X,n);
then
A10: T.x1 in T.:Ball(0.X,n) by FUNCT_2:35;
NAT=dom f by FUNCT_2:def 1;
then
A11: f.n in rng f by FUNCT_1:3;
consider TBn be Subset of TopSpaceNorm Y such that
A12: TBn=T.: Ball(0.X,n) and
A13: f.n =Cl(TBn) by A4;
TBn c= f.n by A13,PRE_TOPC:18;
hence thesis by A8,A10,A12,A11,TARSKI:def 4;
end;
union rng f is Subset of Y by PROB_1:11;
then union rng f = the carrier of Y by A6;
then consider n0 be Nat, r be Real,
y0 be Point of Y such that
A14: 0 < r and
A15: Ball (y0,r) c= f.n0 by A5,LOPBAN_5:3;
n0 in NAT by ORDINAL1:def 12;
then consider TBn0 be Subset of TopSpaceNorm Y such that
A16: TBn0=T.: Ball(0.X,n0) and
A17: f.n0=Cl(TBn0) by A4;
consider TBn01 be Subset of TopSpaceNorm Y such that
A18: TBn01=T.: Ball(0.X,n0+1) and
A19: f.(n0+1)=Cl(TBn01) by A4;
Ball(0.X,n0) c= Ball(0.X,n0+1) by Th14,NAT_1:11;
then TBn0 c= TBn01 by A16,A18,RELAT_1:123;
then f.n0 c= f.(n0+1) by A17,A19,PRE_TOPC:19;
then
A20: Ball (y0,r) c= Cl(TBn01) by A15,A19;
reconsider LTBn01=TBn01 as Subset of LinearTopSpaceNorm(Y) by
NORMSP_2:def 4;
(-1) is non zero Real;
then
A21: Cl((-1)*LTBn01) =(-1)*Cl(LTBn01) by RLTOPSP1:52;
reconsider yy0 = y0 as Point of LinearTopSpaceNorm Y by NORMSP_2:def 4;
A22: Ball (0.Y,r/(2*n0+2)) is Subset of LinearTopSpaceNorm Y by NORMSP_2:def 4;
||.y0-y0.|| < r by A14,NORMSP_1:6;
then y0 in Ball (y0,r);
then y0 in Cl(TBn01) by A20;
then yy0 in Cl(LTBn01) by Th10;
then
A23: (-1)*yy0 in (-1)*Cl(LTBn01);
reconsider nb1 =1/(2*n0+2) as non zero Real by XREAL_1:139;
reconsider TBX1 = T.: Ball(0.X,1) as Subset of Y;
reconsider my0 = {-yy0} as Subset of LinearTopSpaceNorm Y;
reconsider TBnx01 = T.: Ball(0.X,n0+1) as Subset of LinearTopSpaceNorm Y
by NORMSP_2:def 4;
reconsider BYyr = Ball(y0,r) as Subset of LinearTopSpaceNorm Y by
NORMSP_2:def 4;
reconsider BYr = Ball(0.Y,r) as Subset of LinearTopSpaceNorm Y by
NORMSP_2:def 4;
reconsider XTB01 = T.: Ball(0.X,n0+1) as Subset of Y;
A24: -yy0=(-1)*yy0 by RLVECT_1:16
.=(-1)*y0 by NORMSP_2:def 4
.=-y0 by RLVECT_1:16;
(-1)*LTBn01 = (-1)* (XTB01) by A18,Th9
.= T.:((-1)*Ball(0.X,n0+1)) by Th5
.= LTBn01 by A18,Th11;
then -yy0 in Cl(LTBn01) by A21,A23,RLVECT_1:16;
then -yy0 in Cl(TBn01) by Th10;
then {-yy0} c= Cl(TBn01) by ZFMISC_1:31;
then
A25: my0 c= Cl(TBnx01) by A18,Th10;
BYyr c= Cl(TBnx01) by A18,A20,Th10;
then my0 + BYyr c= Cl(TBnx01) + Cl(TBnx01) by A25,RLTOPSP1:11;
then -yy0 + BYyr c= Cl(TBnx01) + Cl(TBnx01) by RUSUB_4:33;
then
A26: -y0 + Ball (y0,r) c= Cl(TBnx01) + Cl(TBnx01) by A24,Th8;
A27: Cl(TBnx01) + Cl(TBnx01) c= Cl(TBnx01+TBnx01) by RLTOPSP1:62;
Ball (y0,r) = y0 + Ball (0.Y,r) by Th2;
then BYyr = yy0+ BYr by Th8;
then (-yy0)+BYyr =(-yy0 + yy0)+ BYr by RLTOPSP1:6;
then (-yy0)+BYyr =0.(LinearTopSpaceNorm Y)+ BYr by RLVECT_1:5;
then (-yy0)+BYyr ={0.(LinearTopSpaceNorm Y)}+ BYr by RUSUB_4:33;
then (-yy0)+BYyr = BYr by CONVEX1:35;
then Ball (0.Y,r) = -y0 + Ball (y0,r) by A24,Th8;
then
A28: Ball (0.Y,r) c= Cl(TBnx01+TBnx01) by A26,A27;
TBnx01= 1* TBnx01 by CONVEX1:32;
then
A29: TBnx01+TBnx01 =(1+1)* TBnx01 by Th13,CONVEX1:13
.= 2 * TBnx01;
Ball(0.X,(n0+1)*1) = (n0+1) * Ball(0.X,1) by Th3;
then (n0+1)*TBX1 = T.: Ball(0.X,n0+1) by Th5;
then TBnx01+TBnx01 = 2* ((n0+1)*TB1) by A29,Th9
.= (2*(n0+1))*TB1 by CONVEX1:37
.=(2*n0+2)*TB1;
then
A30: Cl(TBnx01+TBnx01) = (2*n0+2)* Cl(TB1) by RLTOPSP1:52;
A31: 0 < r/(2*n0+2) by A14,XREAL_1:139;
Ball (0.Y, r/(2*n0+2)) = Ball (0.Y, r*1/(2*n0+2))
.=Ball (0.Y, r*(1/(2*n0+2))) by XCMPLX_1:74
.=nb1 * Ball(0.Y,r) by Th3
.= nb1 * BYr by Th9;
then
A32: Ball (0.Y, r/(2*n0+2)) c= 1/(2*n0+2) *((2*n0+2)* Cl(TB1)) by A28,A30,
CONVEX1:39;
1/(2*n0+2) *((2*n0+2)* Cl(TB1)) =(1/(2*n0+2)*(2*n0+2))* Cl(TB1) by
CONVEX1:37
.= 1* Cl(TB1) by XCMPLX_1:106
.= Cl(TB1) by CONVEX1:32;
then
A33: Ball (0.Y,r/(2*n0+2)) c= T.: Ball(0.X,1) by A14,A32,A22,Th15,XREAL_1:139;
A34: for p be Real st p > 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;