environ
vocabularies HIDDEN, NUMBERS, CARD_1, XXREAL_0, ARYTM_3, RELAT_1, ARYTM_1, XBOOLE_0, SUBSET_1, FUNCT_1, ZFMISC_1, NORMSP_1, RLSUB_1, RSSPACE, COHSP_1, PRE_TOPC, METRIC_1, SUPINF_2, TARSKI, REAL_1, COMPLEX1, LOPBAN_1, STRUCT_0, NORMSP_2, RCOMP_1, NAT_1, CARD_3, ORDINAL2, SEQ_2, RSSPACE3, FUNCT_2, UNIALG_1, PARTFUN1, FCONT_1, CFCONT_1, RLVECT_1, TMAP_1, MSSUBFAM, RELAT_2, RLTOPSP1, REWRITE1, FINSEQ_1, NORMSP_0, ALGSTR_0, LOPBAN_7, REALSET1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, REALSET1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1, FUNCT_3, FINSEQ_1, FINSEQ_2, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, RLSUB_1, VECTSP_1, NORMSP_0, NORMSP_1, T_0TOPSP, TMAP_1, RLTOPSP1, RSSPACE, EUCLID, RSSPACE3, LOPBAN_1, NFCONT_1, NORMSP_2, PDIFF_1, PRVECT_3;
definitions TARSKI, FUNCT_2, NORMSP_0, NORMSP_1, LOPBAN_1, VECTSP_1, RLSUB_1;
theorems TARSKI, XBOOLE_1, RLVECT_1, RELAT_1, RLSUB_1, ZFMISC_1, FUNCT_2, XREAL_1, XCMPLX_1, NORMSP_1, NFCONT_1, XXREAL_0, FUNCT_1, ORDINAL1, PARTFUN1, VECTSP_1, RSSPACE, NORMSP_2, FUNCT_3, ABSVALUE, PDIFF_8, PDIFF_1, FINSEQ_1, XTUPLE_0, LOPBAN_1, NORMSP_0, LOPBAN_6, T_0TOPSP, TOPS_2, TMAP_1, PRVECT_3, RSSPACE3;
schemes FUNCT_2;
registrations XREAL_0, XXREAL_0, ORDINAL1, RELSET_1, STRUCT_0, NAT_1, NORMSP_1, NORMSP_2, FUNCT_1, FUNCT_2, LOPBAN_1, NORMSP_0, RELAT_1, RLTOPSP1, PRVECT_3, NUMBERS, XBOOLE_0, VALUED_0;
constructors HIDDEN, REAL_1, PCOMPS_1, RUSUB_4, NFCONT_1, FUNCT_3, NEWTON, NORMSP_2, RSSPACE3, T_0TOPSP, RELSET_1, TMAP_1, PRVECT_3, PDIFF_1, REALSET1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities STRUCT_0, RLVECT_1, PCOMPS_1, NORMSP_0, NORMSP_2, PRVECT_3;
expansions TARSKI, FUNCT_2, NORMSP_0, NORMSP_1, LOPBAN_1;
definition
let X,
Y be
RealNormSpace;
let T be
LinearOperator of
X,
Y;
func graphNSP T -> non
empty NORMSTR equals
NORMSTR(#
(graph T),
(Zero_ ((graph T),[:X,Y:])),
(Add_ ((graph T),[:X,Y:])),
(Mult_ ((graph T),[:X,Y:])),
(graphNrm T) #);
correctness
coherence
NORMSTR(# (graph T),(Zero_ ((graph T),[:X,Y:])),(Add_ ((graph T),[:X,Y:])),(Mult_ ((graph T),[:X,Y:])),(graphNrm T) #) is non empty NORMSTR ;
;
end;
::
deftheorem defines
graphNSP LOPBAN_7:def 4 :
for X, Y being RealNormSpace
for T being LinearOperator of X,Y holds graphNSP T = NORMSTR(# (graph T),(Zero_ ((graph T),[:X,Y:])),(Add_ ((graph T),[:X,Y:])),(Mult_ ((graph T),[:X,Y:])),(graphNrm T) #);
Lm1:
for X, Y being RealNormSpace
for T being LinearOperator of X,Y
for x, y being Point of (graphNSP T)
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (graphNSP T) ) & ( x = 0. (graphNSP T) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )