environ
vocabularies HIDDEN, RLSUB_1, UNIALG_1, DUALSP01, NORMSP_3, CFCONT_1, MOD_4, RLVECT_1, ARYTM_1, RELAT_1, FUNCT_1, RSSPACE, RSSPACE3, VECTSP_1, REAL_1, TARSKI, MSSUBFAM, STRUCT_0, REALSET1, FUNCOP_1, FCONT_1, NORMSP_0, SEQ_2, LOPBAN_1, ORDINAL2, ARYTM_3, ALGSTR_0, NORMSP_1, FUNCT_2, PRE_TOPC, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, SEQ_4, XBOOLE_0, CARD_1, SUPINF_2, COMPLEX1, XXREAL_0, XXREAL_2, NAT_1, REWRITE1, METRIC_1, RELAT_2, PARTFUN1, RCOMP_1, TOPS_1, SETFAM_1, TOPGEN_1, CARD_3, NORMSP_2, RLVECT_3, VECTSP10, GROUP_6;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, CARD_1, ORDINAL1, SETFAM_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, FUNCOP_1, REALSET1, NUMBERS, CARD_3, XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, COMPLEX1, XXREAL_2, SEQ_4, STRUCT_0, ALGSTR_0, PRE_TOPC, TOPS_1, RLVECT_1, RLVECT_3, RLSUB_1, VECTSP_1, VECTSP_4, NORMSP_0, NORMSP_1, NORMSP_2, HAHNBAN, RSSPACE, RSSPACE3, LOPBAN_1, NFCONT_1, VECTSP10, DUALSP01, TOPGEN_1;
definitions ALGSTR_0, VECTSP_1, TARSKI, LOPBAN_1;
theorems SEQ_4, FUNCT_1, COMPLEX1, TARSKI, RSSPACE3, XREAL_0, XXREAL_0, NORMSP_1, LOPBAN_1, FUNCT_2, XBOOLE_0, XREAL_1, RLVECT_1, FUNCOP_1, VECTSP_1, RLSUB_1, RSSPACE, NORMSP_0, ORDINAL1, VECTSP_4, LOPBAN_7, NDIFF_1, PRE_TOPC, TOPS_1, TOPGEN_1, SUBSET_1, NFCONT_1, XXREAL_2, DUALSP01, RELAT_1, XCMPLX_1, NORMSP_2, LOPBAN_3, RLVECT_3, VECTSP10, CARD_3;
schemes FUNCT_2;
registrations STRUCT_0, XREAL_0, NUMBERS, ORDINAL1, MEMBERED, RELAT_1, XXREAL_0, VECTSP_1, FUNCT_2, SEQ_4, RELSET_1, TOPS_1, XCMPLX_0, NORMSP_0, NAT_1, NORMSP_1, DUALSP01, XBOOLE_0, SUBSET_1, XXREAL_2, NORMSP_2, RLSUB_1, REALSET1, LOPBAN_1;
constructors HIDDEN, REALSET1, RSSPACE3, BINOP_2, LOPBAN_2, NFCONT_1, DUALSP01, RELSET_1, SEQ_4, NORMSP_2, CARD_3, PCOMPS_1, RLVECT_3, SETFAM_1, TOPS_1, VECTSP10, TOPGEN_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities BINOP_1, RLVECT_1, STRUCT_0, REALSET1, ALGSTR_0, NORMSP_0, VECTSP_1, VECTSP_4, RLSUB_1, VECTSP10, PCOMPS_1, DUALSP01, NORMSP_2;
expansions RLSUB_1, TARSKI, XBOOLE_0, FUNCT_2, NORMSP_0, NORMSP_1, VECTSP_1, STRUCT_0, RLVECT_1, TOPS_1, NFCONT_1;
theorem LMINEQ:
for
x,
y,
z being
Real st
0 <= y & ( for
e being
Real st
0 < e holds
x <= z + (y * e) ) holds
x <= z
SUBTH:
for V being RealNormSpace
for V1 being Subset of V
for x, y being Point of V
for x1, y1 being Point of (NLin V1)
for a being Real st x = x1 & y = y1 holds
( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )
XTh7:
for V being RealNormSpace
for V1 being Subset of V
for x, y being Point of (NLin V1)
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (NLin V1) ) & ( x = 0. (NLin V1) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
NISOM06:
for X, Y being RealNormSpace
for L being Lipschitzian LinearOperator of X,Y
for V being Subset of X
for W being Subset of Y st L is isomorphism & W = L .: V & W is closed holds
V is closed
definition
let V,
W be
RealLinearSpace;
let L be
LinearOperator of
V,
W;
existence
ex b1 being LinearOperator of (VectQuot (V,(Ker L))),(Im L) st
( b1 is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
b1 . z = L . v ) )
by LMQ21;
uniqueness
for b1, b2 being LinearOperator of (VectQuot (V,(Ker L))),(Im L) st b1 is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
b1 . z = L . v ) & b2 is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
b2 . z = L . v ) holds
b1 = b2
end;
LMQ231:
for V being RealNormSpace
for W being Subspace of V
for v being VECTOR of V holds NormVSets (V,W,v) is bounded_below
definition
let V be
RealNormSpace;
let W be
Subspace of
V;
existence
ex b1 being Function of (CosetSet (V,W)),REAL st
for A being Element of CosetSet (V,W)
for v being VECTOR of V st A = v + W holds
b1 . A = lower_bound (NormVSets (V,W,v))
uniqueness
for b1, b2 being Function of (CosetSet (V,W)),REAL st ( for A being Element of CosetSet (V,W)
for v being VECTOR of V st A = v + W holds
b1 . A = lower_bound (NormVSets (V,W,v)) ) & ( for A being Element of CosetSet (V,W)
for v being VECTOR of V st A = v + W holds
b2 . A = lower_bound (NormVSets (V,W,v)) ) holds
b1 = b2
end;
definition
let X be
RealNormSpace;
let Y be
Subspace of
X;
assume A1:
ex
CY being
Subset of
X st
(
CY = the
carrier of
Y &
CY is
closed )
;
existence
ex b1 being strict RealNormSpace st
( RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = VectQuot (X,Y) & the normF of b1 = NormCoset (X,Y) )
uniqueness
for b1, b2 being strict RealNormSpace st RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = VectQuot (X,Y) & the normF of b1 = NormCoset (X,Y) & RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = VectQuot (X,Y) & the normF of b2 = NormCoset (X,Y) holds
b1 = b2
;
end;
LMCL1:
for X being RealNormSpace
for Y, Z being Subset of X st Z = the carrier of (Lin Y) holds
not Cl Z is empty
definition
let X be
RealNormSpace;
let Y be
Subset of
X;
correctness
existence
ex b1 being non empty NORMSTR ex Z being Subset of X st
( Z = the carrier of (Lin Y) & b1 = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) );
uniqueness
for b1, b2 being non empty NORMSTR st ex Z being Subset of X st
( Z = the carrier of (Lin Y) & b1 = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) & ex Z being Subset of X st
( Z = the carrier of (Lin Y) & b2 = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) holds
b1 = b2;
end;
SUBTHCL:
for V being RealNormSpace
for V1 being Subset of V
for x, y being Point of V
for x1, y1 being Point of (ClNLin V1)
for a being Real st x = x1 & y = y1 holds
( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )