:: 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 )

ex s0 being Real st

( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y )

proof end;

scheme :: LOPBAN_6:sch 1

RecExD3{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}() -> Element of F_{1}(), P_{1}[ object , object , object , object ] } :

RecExD3{ F

ex f being sequence of F_{1}() st

( f . 0 = F_{2}() & f . 1 = F_{3}() & ( for n being Nat holds P_{1}[n,f . n,f . (n + 1),f . (n + 2)] ) )

provided( f . 0 = F

A1:
for n being Nat

for x, y being Element of F_{1}() ex z being Element of F_{1}() st P_{1}[n,x,y,z]

for x, y being Element of F

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))

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))

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)

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)

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)

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

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

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

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

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))

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

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

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)

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

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;

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

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;