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


theorem Th1: :: LOPBAN_6:1
for x, y being Real st 0 <= x & x < y holds
ex s0 being Real st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y )
proof end;

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

theorem Th2: :: LOPBAN_6:2
for X being RealNormSpace
for y1 being Point of X
for r being Real holds Ball (y1,r) = y1 + (Ball ((0. X),r))
proof end;

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

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)
proof end;

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)
proof end;

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)
proof end;

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 & W = W1 holds
V + W = V1 + W1
proof end;

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 & x = x1 holds
x + V = x1 + V1
proof end;

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
proof end;

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
proof end;

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

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

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

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

:: 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
for BX1 being Subset of (LinearTopSpaceNorm X)
for TBX1, BYr being 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 end;

:: 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 & T1 is onto holds
T1 is open
proof end;