:: 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{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), P₁[ object , object , object , object ] } :

ex f being sequence of F₁() st
( f . 0 = F₂() & f . 1 = F₃() & ( 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 F₁() ex z being Element of F₁() st P₁[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
:: 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;