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

environ

vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, T_0TOPSP, 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;
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;
constructors HIDDEN, 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;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities RLVECT_1, PCOMPS_1, CONVEX1, RUSUB_4, ALGSTR_0, NORMSP_2, XBOOLE_0, LOPBAN_5;
expansions TARSKI, CONVEX1, XBOOLE_0;


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;