:: Open Mapping Theorem :: by Hideki Sakurai , Hisayoshi Kunimune and Yasunari Shidama :: :: Received September 23, 2008 :: Copyright (c) 2008-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies 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 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; constructors 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; 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; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin theorem :: LOPBAN_6:1 for x,y be Real st 0<=x & x non empty set, A() -> Element of D(), B() -> Element of D(), P[object,object,object,object]}: ex f being sequence of D() st f.0 = A() & f.1 = B() & for n being Nat holds P[n,f.n,f.(n+1),f.(n+2)] provided for n being Nat for x,y being Element of D() ex z being Element of D() st P[n,x,y,z]; reserve X, Y for RealNormSpace; theorem :: LOPBAN_6:2 for y1 be Point of X, r be Real holds Ball(y1,r) = y1 + Ball(0.X,r); theorem :: LOPBAN_6:3 for r,a be Real st 0 < a holds Ball(0.X,a*r) = a * Ball(0.X,r); theorem :: LOPBAN_6:4 for T be LinearOperator of X,Y, B0,B1 be Subset of X holds T.:(B0+B1) = T.:B0+T.:B1; theorem :: LOPBAN_6:5 for T be LinearOperator of X,Y, B0 be Subset of X, a be Real holds T.:(a*B0) = a*T.:B0; theorem :: LOPBAN_6:6 for T be LinearOperator of X,Y, B0 be Subset of X, x1 be Point of X holds T.:(x1+ B0) = T.x1 + T.:B0; theorem :: LOPBAN_6:7 for V,W be Subset of X, V1,W1 be Subset of LinearTopSpaceNorm X st V= V1 & W=W1 holds V+W=V1+W1; theorem :: LOPBAN_6:8 for V be Subset of X,x be Point of X, V1 be Subset of LinearTopSpaceNorm X, x1 be Point of LinearTopSpaceNorm X st V=V1 & x=x1 holds x+V=x1+V1; theorem :: LOPBAN_6:9 for V be Subset of X,a be Real, V1 be Subset of LinearTopSpaceNorm X st V=V1 holds a*V=a*V1; theorem :: LOPBAN_6:10 for V be Subset of TopSpaceNorm X, V1 be Subset of LinearTopSpaceNorm X st V=V1 holds Cl(V)=Cl(V1); theorem :: LOPBAN_6:11 for x be Point of X, r be Real holds Ball(0.X,r)=(-1)* Ball(0.X,r); theorem :: LOPBAN_6:12 for x be Point of X,r be Real, V be Subset of LinearTopSpaceNorm X st V = Ball(x,r) holds V is convex; theorem :: LOPBAN_6:13 for x be Point of X,r be Real, T be LinearOperator of X,Y , V be Subset of LinearTopSpaceNorm Y st V = T.: Ball(x,r) holds V is convex; theorem :: LOPBAN_6:14 for x be Point of X, r, s be Real st r <= s holds Ball(x, r) c= Ball(x,s); :: Open Mapping lemma theorem :: LOPBAN_6:15 for X be RealBanachSpace, Y be RealNormSpace, T be Lipschitzian LinearOperator of X,Y, r be Real, BX1 be Subset of LinearTopSpaceNorm X, TBX1,BYr be 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; :: Open Mapping Theorem ::$N Open Mapping Theorem theorem :: LOPBAN_6:16 for X, Y be RealBanachSpace, T be Lipschitzian LinearOperator of X,Y, T1 be Function of LinearTopSpaceNorm X,LinearTopSpaceNorm Y st T1=T & T1 is onto holds T1 is open;