environ
vocabularies HIDDEN, ALGSTR_0, ARYTM_1, ARYTM_3, BINOP_2, CARD_1, CARD_3, CLASSES1, COMPLEX1, CONNSP_2, EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1, FINSOP_1, FUNCT_1, FUNCT_2, FVSUM_1, INCSP_1, LMOD_7, MATRIX_1, MATRIX_3, MATRIX_6, MATRIX13, MATRIX15, MATRIXR1, MATRLIN, MATRLIN2, MESFUNC1, METRIC_1, NAT_1, NUMBERS, ORDINAL2, ORDINAL4, PARTFUN1, PARTFUN3, PRE_POLY, PRE_TOPC, PRVECT_1, QC_LANG1, RANKNULL, REAL_1, RELAT_1, RLSUB_1, RLVECT_3, RLVECT_5, RVSUM_1, SQUARE_1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI, TOPS_1, TOPS_2, TREES_1, VALUED_0, VALUED_1, VECTSP_1, VECTSP10, XBOOLE_0, XXREAL_0, ZFMISC_1, FUNCOP_1, FUNCT_7, MOD_3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, FINSET_1, TOPS_1, TOPS_2, FUNCT_1, PARTFUN1, VALUED_0, VALUED_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, BINOP_1, STRUCT_0, VECTSP_1, MATRIX_0, MATRIX_1, MATRIX_3, VECTSP_4, VECTSP_7, VECTSP_9, MATRIX13, XREAL_0, RVSUM_1, ALGSTR_0, FVSUM_1, RANKNULL, MATRIX11, COMPLEX1, BINOP_2, FUNCOP_1, SQUARE_1, PRE_TOPC, PARTFUN3, MATRIX_6, MATRLIN, MATRLIN2, NAT_D, MATRIX15, CONNSP_2, METRIC_1, EUCLID, FINSOP_1, PNPROC_1, RUSUB_4, PRVECT_1;
definitions BORSUK_1, PARTFUN3, TARSKI, XBOOLE_0;
theorems ABSVALUE, BINOP_2, CARD_1, CARD_2, CONNSP_2, EUCLID, EUCLID_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQOP, FINSOP_1, FUNCOP_1, FUNCT_1, FUNCT_2, FVSUM_1, GOBOARD6, LAPLACE, MATRIX_0, MATRIX_3, MATRIX_4, MATRIX_6, MATRIX11, MATRIX13, MATRIX14, MATRIX15, MATRIXR1, MATRLIN, MATRLIN2, MATRPROB, METRIC_1, NAT_1, ORDINAL1, PARTFUN3, RANKNULL, RELAT_1, RLVECT_1, RUSUB_4, RVSUM_1, SPPOL_1, SQUARE_1, STIRL2_1, TARSKI, TOPREAL3, TOPS_2, VALUED_0, VALUED_1, VECTSP_4, VECTSP_7, VECTSP_9, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_0, XREAL_1, XXREAL_0, ZFMISC_1;
schemes FINSEQ_1, FUNCT_2, NAT_1;
registrations BINOP_2, CARD_1, EUCLID, EUCLID_9, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_1, FUNCT_2, GRCAT_1, MATRIX13, MATRLIN2, MEMBERED, MOD_2, MONOID_0, NAT_1, NUMBERS, PARTFUN3, PRVECT_1, RELAT_1, RELSET_1, RVSUM_1, STRUCT_0, VALUED_0, VALUED_1, VECTSP_1, VECTSP_9, XREAL_0, XXREAL_0, MATRIX_6, ORDINAL1;
constructors HIDDEN, BINARITH, CONNSP_2, FINSOP_1, FVSUM_1, LAPLACE, MATRIX_6, MATRIX11, MATRIX13, MATRIX15, MATRLIN2, MONOID_0, PARTFUN3, PNPROC_1, RANKNULL, RELSET_1, RUSUB_5, SETWISEO, SQUARE_1, TOPS_1, TOPS_2, VECTSP_9, VECTSP10, WELLORD2, EUCLID, MATRIX_1, REAL_1, BINOP_2, VALUED_2;
requirements HIDDEN, ARITHM, NUMERALS, REAL, BOOLE, SUBSET;
equalities EUCLID, FINSEQ_1, MATRIX13, RANKNULL, SQUARE_1, STRUCT_0, VECTSP_1, VECTSP_4, XBOOLE_0, FVSUM_1, RLVECT_1;
expansions FINSEQ_1, PARTFUN3, STRUCT_0, TARSKI, XBOOLE_0;
Lm1:
for n, m being Nat
for K being Field
for A being Matrix of n,m,K st ( n = 0 implies m = 0 ) & the_rank_of A = n holds
ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m
Lm2:
for n being Nat
for f being b1 -element real-valued FinSequence holds f is Point of (TOP-REAL n)
definition
let n,
m be
Nat;
let M be
Matrix of
n,
m,
F_Real;
existence
( ( n <> 0 implies ex b1 being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds b1 . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( not n <> 0 implies ex b1 being Function of (TOP-REAL n),(TOP-REAL m) st
for f being n -element real-valued FinSequence holds b1 . f = 0. (TOP-REAL m) ) )
uniqueness
for b1, b2 being Function of (TOP-REAL n),(TOP-REAL m) holds
( ( n <> 0 & ( for f being n -element real-valued FinSequence holds b1 . f = Line (((LineVec2Mx (@ f)) * M),1) ) & ( for f being n -element real-valued FinSequence holds b2 . f = Line (((LineVec2Mx (@ f)) * M),1) ) implies b1 = b2 ) & ( not n <> 0 & ( for f being n -element real-valued FinSequence holds b1 . f = 0. (TOP-REAL m) ) & ( for f being n -element real-valued FinSequence holds b2 . f = 0. (TOP-REAL m) ) implies b1 = b2 ) )
correctness
consistency
for b1 being Function of (TOP-REAL n),(TOP-REAL m) holds verum;
;
end;
reconsider zz = 0 as Real ;
Lm4:
for n, m being Nat
for M being Matrix of n,m,F_Real
for f being b1 -element real-valued FinSequence ex L being b2 -element FinSequence of REAL st
( |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| & ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) )
reconsider jj = 1 as Real ;