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