:: Open Mapping Theorem
:: by Hideki Sakurai , Hisayoshi Kunimune and Yasunari Shidama
::
:: Received September 23, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

theorem Th1: :: LOPBAN_6:1
for x, y being real number st 0 <= x &amp; x < y holds
ex s0 being real number st
( 0 < s0 &amp; x < y / (1 + s0) &amp; y / (1 + s0) < y )
proofend;

scheme :: LOPBAN_6:sch 1
RecExD3{ F1() ->  non empty set , F2() ->  Element of F1(), F3() ->  Element of F1(), P1[ set , set , set , set ] } :
 ex f being Function of NAT,F1() st
( f . 0 = F2() &amp; f . 1 = F3() &amp; ( for n being Element of NAT holds P1[n,f . n,f . (n + 1),f . (n + 2)] ) )
provided
A1: for n being Element of NAT
for x, y being Element of F1() ex z being Element of F1() st P1[n,x,y,z]
proofend;

theorem Th2: :: LOPBAN_6:2
for X being RealNormSpace
for y1 being Point of X
for r being real number holds Ball (y1,r) = y1 + (Ball ((0. X),r))
proofend;

theorem Th3: :: LOPBAN_6:3
for X being RealNormSpace
for r being real number
for a being Real st 0 < a holds
Ball ((0. X),(a * r)) = a * (Ball ((0. X),r))
proofend;

theorem :: LOPBAN_6:4
for X, Y being RealNormSpace
for T being LinearOperator of X,Y
for B0, B1 being Subset of X holds T .: (B0 + B1) = (T .: B0) + (T .: B1)
proofend;

theorem Th5: :: LOPBAN_6:5
for X, Y being RealNormSpace
for T being LinearOperator of X,Y
for B0 being Subset of X
for a being Real holds T .: (a * B0) = a * (T .: B0)
proofend;

theorem Th6: :: LOPBAN_6:6
for X, Y being RealNormSpace
for T being LinearOperator of X,Y
for B0 being Subset of X
for x1 being Point of X holds T .: (x1 + B0) = (T . x1) + (T .: B0)
proofend;

theorem :: LOPBAN_6:7
for X being RealNormSpace
for V, W being Subset of X
for V1, W1 being Subset of (LinearTopSpaceNorm X) st V = V1 &amp; W = W1 holds
V + W = V1 + W1
proofend;

theorem Th8: :: LOPBAN_6:8
for X being RealNormSpace
for V being Subset of X
for x being Point of X
for V1 being Subset of (LinearTopSpaceNorm X)
for x1 being Point of (LinearTopSpaceNorm X) st V = V1 &amp; x = x1 holds
x + V = x1 + V1
proofend;

theorem Th9: :: LOPBAN_6:9
for X being RealNormSpace
for V being Subset of X
for a being Real
for V1 being Subset of (LinearTopSpaceNorm X) st V = V1 holds
a * V = a * V1
proofend;

theorem Th10: :: LOPBAN_6:10
for X being RealNormSpace
for V being Subset of (TopSpaceNorm X)
for V1 being Subset of (LinearTopSpaceNorm X) st V = V1 holds
Cl V = Cl V1
proofend;

theorem Th11: :: LOPBAN_6:11
for X being RealNormSpace
for x being Point of X
for r being real number holds Ball ((0. X),r) = (- 1) * (Ball ((0. X),r))
proofend;

theorem Th12: :: LOPBAN_6:12
for X being RealNormSpace
for x being Point of X
for r being real number
for V being Subset of (LinearTopSpaceNorm X) st V = Ball (x,r) holds
V is convex
proofend;

theorem Th13: :: LOPBAN_6:13
for X, Y being RealNormSpace
for x being Point of X
for r being real number
for T being LinearOperator of X,Y
for V being Subset of (LinearTopSpaceNorm Y) st V = T .: (Ball (x,r)) holds
V is convex
proofend;

theorem Th14: :: LOPBAN_6:14
for X being RealNormSpace
for x being Point of X
for r, s being real number st r <= s holds
Ball (x,r) c= Ball (x,s)
proofend;

:: Open Mapping lemma
theorem Th15: :: LOPBAN_6:15
for X being RealBanachSpace
for Y being RealNormSpace
for T being Lipschitzian LinearOperator of X,Y
for r being real number
for BX1 being Subset of (LinearTopSpaceNorm X)
for TBX1, BYr being Subset of (LinearTopSpaceNorm Y) st r > 0 &amp; BYr = Ball ((0. Y),r) &amp; TBX1 = T .: (Ball ((0. X),1)) &amp; BYr c= Cl TBX1 holds
BYr c= TBX1
proofend;

:: Open Mapping Theorem
:: [WP: ] Open_Mapping_Theorem
theorem :: LOPBAN_6:16
for X, Y being RealBanachSpace
for T being Lipschitzian LinearOperator of X,Y
for T1 being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y) st T1 = T &amp; T1 is onto holds
T1 is open
proofend;