begin
:: deftheorem defines @ MATRTOP1:def 1 :
for rf being real-valued FinSequence holds @ rf = rf;
:: deftheorem defines @ MATRTOP1:def 2 :
for p being FinSequence of F_Real holds @ p = p;
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem
theorem Th9:
theorem
theorem Th11:
theorem Th12:
theorem
theorem
theorem Th15:
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
theorem Th16:
theorem
Lm2:
for n being Nat
for f being b1 -element real-valued FinSequence holds f is Point of (TOP-REAL n)
begin
definition
let n,
m be
Nat;
let M be
Matrix of
n,
m,
F_Real;
func Mx2Tran M -> Function of
(TOP-REAL n),
(TOP-REAL m) means :
Def3:
for
f being
n -element real-valued FinSequence holds
it . f = Line (
((LineVec2Mx (@ f)) * M),1)
if n <> 0 otherwise for
f being
n -element real-valued FinSequence holds
it . f = 0. (TOP-REAL m);
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;
:: deftheorem Def3 defines Mx2Tran MATRTOP1:def 3 :
for n, m being Nat
for M being Matrix of n,m,F_Real
for b4 being Function of (TOP-REAL n),(TOP-REAL m) holds
( ( n <> 0 implies ( b4 = Mx2Tran M iff for f being b1 -element real-valued FinSequence holds b4 . f = Line (((LineVec2Mx (@ f)) * M),1) ) ) & ( not n <> 0 implies ( b4 = Mx2Tran M iff for f being b1 -element real-valued FinSequence holds b4 . f = 0. (TOP-REAL m) ) ) );
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem
theorem
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem
theorem
begin
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
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))).| ) )
theorem Th44:
theorem Th45:
theorem
theorem Th47: