:: Some Special Matrices of Real Elements and Their Properties
:: by Xiquan Liang , Fuguo Ge and Xiaopeng Yue
::
:: Received October 19, 2006
:: Copyright (c) 2006-2016 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, SUBSET_1, NAT_1, MATRIX_1, RELAT_1, XXREAL_0, CARD_1,
ARYTM_3, LATTICE3, FUNCT_4, FINSEQ_1, TREES_1, COMPLEX1, ARYTM_1,
FUNCOP_1, QC_LANG1, VECTSP_1, REAL_1, MATRIXR1, ZFMISC_1, MATRIX10,
FUNCT_7;
notations COMPLEX1, TARSKI, ZFMISC_1, SUBSET_1, FINSEQ_1, MATRIX_0, ORDINAL1,
FUNCT_7, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, MATRIXR1,
RLVECT_1, VECTSP_1, STRUCT_0, MATRIX_3, GROUP_1, MATRIX_1;
constructors XXREAL_0, REAL_1, BINOP_2, MEMBERED, COMPLEX1, MATRIX_3,
MATRIX_4, MATRIXR1, RELSET_1, FUNCT_7, NUMBERS;
registrations RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, VECTSP_1, ORDINAL1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
begin
reserve a,b for Real,
i,j,n for Nat,
M,M1,M2,M3,M4 for Matrix of n, REAL;
definition
let M be Matrix of REAL;
attr M is Positive means
:: MATRIX10:def 1
for i,j st [i,j] in Indices M holds M*(i,j) > 0;
attr M is Negative means
:: MATRIX10:def 2
for i,j st [i,j] in Indices M holds M*(i,j) < 0;
attr M is Nonpositive means
:: MATRIX10:def 3
for i,j st [i,j] in Indices M holds M*(i, j) <= 0;
attr M is Nonnegative means
:: MATRIX10:def 4
for i,j st [i,j] in Indices M holds M*(i, j) >= 0;
end;
definition
let M1,M2 be Matrix of REAL;
pred M1 is_less_than M2 means
:: MATRIX10:def 5
for i,j st [i,j] in Indices M1 holds M1 *(i,j) < M2*(i,j);
pred M1 is_less_or_equal_with M2 means
:: MATRIX10:def 6
for i,j st [i,j] in Indices M1 holds M1*(i,j) <= M2*(i,j);
end;
definition
let M be Matrix of REAL;
func |:M:| -> Matrix of REAL means
:: MATRIX10:def 7
len it = len M & width it = width
M & for i,j holds [i,j] in Indices M implies it*(i,j) = |.M*(i,j).|;
end;
definition
let n;
let M;
redefine func -M -> Matrix of n,REAL;
end;
definition
let n;
let M;
redefine func |:M:| -> Matrix of n,REAL;
end;
definition
let n;
let M1,M2;
redefine func M1+M2 -> Matrix of n,REAL;
end;
definition
let n;
let M1,M2;
redefine func M1-M2 -> Matrix of n,REAL;
end;
definition
let n;
let a be Real;
let M;
redefine func a*M -> Matrix of n,REAL;
end;
registration
let n;
cluster (n,n) --> 1 -> Positive for Matrix of n,REAL;
cluster ((n,n) --> -1) -> Negative for Matrix of n,REAL;
cluster ((n,n) --> -1) -> Nonpositive for Matrix of n,REAL;
cluster ((n,n) --> 1) -> Nonnegative for Matrix of n,REAL;
end;
registration
let n;
cluster Positive Nonnegative for Matrix of n,REAL;
cluster Negative Nonpositive for Matrix of n,REAL;
end;
registration
cluster Positive Nonnegative for Matrix of REAL;
cluster Negative Nonpositive for Matrix of REAL;
end;
registration
let M be Positive Matrix of REAL;
cluster M@ -> Positive;
end;
registration
let M be Negative Matrix of REAL;
cluster M@ -> Negative;
end;
registration
let M be Nonpositive Matrix of REAL;
cluster M@ -> Nonpositive;
end;
registration
let M be Nonnegative Matrix of REAL;
cluster M@ -> Nonnegative;
end;
theorem :: MATRIX10:1
for x1 be Element of F_Real for x2 be Real st x1 = x2 holds -x1=-x2;
theorem :: MATRIX10:2
for M being Matrix of REAL st [i,j] in Indices M holds (-M)*(i,j) =-(M*(i,j))
;
theorem :: MATRIX10:3
for M1,M2 be Matrix of REAL st len M1=len M2 & width M1=width M2
& [i,j] in Indices M1 holds (M1-M2)*(i,j)=(M1*(i,j)) - (M2*(i,j));
theorem :: MATRIX10:4
for M being Matrix of REAL st [i,j] in Indices M holds (a*M)*(i,j
)=a*(M*(i,j));
theorem :: MATRIX10:5
Indices M = Indices |:M:|;
theorem :: MATRIX10:6
|:a*M:|=|.a.|*|:M:|;
theorem :: MATRIX10:7
M is Negative implies -M is Positive;
theorem :: MATRIX10:8
M1 is Positive & M2 is Positive implies M1+M2 is Positive;
theorem :: MATRIX10:9
-M2 is_less_than M1 implies M1+M2 is Positive;
theorem :: MATRIX10:10
M1 is Nonnegative & M2 is Positive implies M1+M2 is Positive;
theorem :: MATRIX10:11
M1 is Positive & M2 is Negative & |:M2:| is_less_than |:M1:| implies
M1+M2 is Positive;
theorem :: MATRIX10:12
M1 is Positive & M2 is Negative implies M1-M2 is Positive;
theorem :: MATRIX10:13
M2 is_less_than M1 implies M1-M2 is Positive;
theorem :: MATRIX10:14
a>0 & M is Positive implies a*M is Positive;
theorem :: MATRIX10:15
a<0 & M is Negative implies a*M is Positive;
theorem :: MATRIX10:16
M is Positive implies (-M) is Negative;
theorem :: MATRIX10:17
M1 is Negative & M2 is Negative implies M1+M2 is Negative;
theorem :: MATRIX10:18
M1 is_less_than -M2 implies M1+M2 is Negative;
theorem :: MATRIX10:19
M1 is Positive & M2 is Negative & |:M1:| is_less_than |:M2:| implies
M1+M2 is Negative;
theorem :: MATRIX10:20
M1 is_less_than M2 implies M1-M2 is Negative;
theorem :: MATRIX10:21
M1 is Positive & M2 is Negative implies M2-M1 is Negative;
theorem :: MATRIX10:22
a<0 & M is Positive implies a*M is Negative;
theorem :: MATRIX10:23
a>0 & M is Negative implies a*M is Negative;
theorem :: MATRIX10:24
M is Nonnegative implies -M is Nonpositive;
theorem :: MATRIX10:25
M is Negative implies M is Nonpositive;
theorem :: MATRIX10:26
M1 is Nonpositive & M2 is Nonpositive implies M1+M2 is Nonpositive;
theorem :: MATRIX10:27
M1 is_less_or_equal_with -M2 implies M1+M2 is Nonpositive;
theorem :: MATRIX10:28
M1 is_less_or_equal_with M2 implies M1-M2 is Nonpositive;
theorem :: MATRIX10:29
a<=0 & M is Positive implies a*M is Nonpositive;
theorem :: MATRIX10:30
a>=0 & M is Negative implies a*M is Nonpositive;
theorem :: MATRIX10:31
a>=0 & M is Nonpositive implies a*M is Nonpositive;
theorem :: MATRIX10:32
a<=0 & M is Nonnegative implies a*M is Nonpositive;
theorem :: MATRIX10:33
|:M:| is Nonnegative;
theorem :: MATRIX10:34
M1 is Positive implies M1 is Nonnegative;
theorem :: MATRIX10:35
M is Nonpositive implies (-M) is Nonnegative;
theorem :: MATRIX10:36
M1 is Nonnegative & M2 is Nonnegative implies M1+M2 is Nonnegative;
theorem :: MATRIX10:37
-M1 is_less_or_equal_with M2 implies M1+M2 is Nonnegative;
theorem :: MATRIX10:38
M2 is_less_or_equal_with M1 implies M1-M2 is Nonnegative;
theorem :: MATRIX10:39
a>=0 & M is Positive implies a*M is Nonnegative;
theorem :: MATRIX10:40
a<=0 & M is Negative implies a*M is Nonnegative;
theorem :: MATRIX10:41
a<=0 & M is Nonpositive implies a*M is Nonnegative;
theorem :: MATRIX10:42
a>=0 & M is Nonnegative implies a*M is Nonnegative;
theorem :: MATRIX10:43
a>=0 & b>=0 & M1 is Nonnegative & M2 is Nonnegative implies a*M1+b*M2
is Nonnegative;
begin
theorem :: MATRIX10:44
M1 is_less_than M2 implies M1 is_less_or_equal_with M2;
theorem :: MATRIX10:45
M1 is_less_than M2 & M2 is_less_than M3 implies M1 is_less_than M3;
theorem :: MATRIX10:46
M1 is_less_than M2 & M3 is_less_than M4 implies (M1+M3) is_less_than ( M2+M4)
;
theorem :: MATRIX10:47
M1 is_less_than M2 implies M1+M3 is_less_than M2+M3;
theorem :: MATRIX10:48
M1 is_less_than M2 implies M3-M2 is_less_than M3-M1;
theorem :: MATRIX10:49
|:M1+M2:| is_less_or_equal_with |:M1:|+|:M2:|;
theorem :: MATRIX10:50
M1 is_less_or_equal_with M2 implies (M1-M3) is_less_or_equal_with (M2- M3);
theorem :: MATRIX10:51
(M1-M3) is_less_or_equal_with (M2-M3) implies M1 is_less_or_equal_with M2;
theorem :: MATRIX10:52
M1 is_less_or_equal_with M2-M3 implies M3 is_less_or_equal_with M2-M1;
theorem :: MATRIX10:53
M1-M2 is_less_or_equal_with M3 implies M1-M3 is_less_or_equal_with M2;
theorem :: MATRIX10:54
M1 is_less_than M2 & M3 is_less_or_equal_with M4 implies M1-M4
is_less_than M2-M3;
theorem :: MATRIX10:55
M1 is_less_or_equal_with M2 & M3 is_less_than M4 implies M1-M4
is_less_than M2-M3;
theorem :: MATRIX10:56
M1-M2 is_less_or_equal_with M3-M4 implies M1-M3 is_less_or_equal_with M2-M4;
theorem :: MATRIX10:57
M1-M2 is_less_or_equal_with M3-M4 implies M4-M2 is_less_or_equal_with M3-M1;
theorem :: MATRIX10:58
M1-M2 is_less_or_equal_with M3-M4 implies M4-M3 is_less_or_equal_with M2-M1;
theorem :: MATRIX10:59
M1+M2 is_less_or_equal_with M3 implies M1 is_less_or_equal_with M3-M2;
theorem :: MATRIX10:60
M1+M2 is_less_or_equal_with M3+M4 implies M1-M3 is_less_or_equal_with M4-M2;
theorem :: MATRIX10:61
M1+M2 is_less_or_equal_with M3-M4 implies M1+M4 is_less_or_equal_with M3-M2;
theorem :: MATRIX10:62
M1-M2 is_less_or_equal_with M3+M4 implies M1-M4 is_less_or_equal_with M3+M2;
theorem :: MATRIX10:63
M1 is_less_or_equal_with M2 implies -M2 is_less_or_equal_with -M1;
theorem :: MATRIX10:64
M1 is_less_or_equal_with -M2 implies M2 is_less_or_equal_with -M1;
theorem :: MATRIX10:65
-M2 is_less_or_equal_with M1 implies -M1 is_less_or_equal_with M2;
theorem :: MATRIX10:66
M1 is Positive implies M2 is_less_than M2+M1;
theorem :: MATRIX10:67
M1 is Negative implies M1+M2 is_less_than M2;
theorem :: MATRIX10:68
M1 is Nonnegative implies M2 is_less_or_equal_with M1+M2;
theorem :: MATRIX10:69
M1 is Nonpositive implies M1+M2 is_less_or_equal_with M2;
theorem :: MATRIX10:70
M1 is Nonpositive & M3 is_less_or_equal_with M2 implies M3+M1
is_less_or_equal_with M2;
theorem :: MATRIX10:71
M1 is Nonpositive & M3 is_less_than M2 implies M3+M1 is_less_than M2;
theorem :: MATRIX10:72
M1 is Negative & M3 is_less_or_equal_with M2 implies M3+M1 is_less_than M2;
theorem :: MATRIX10:73
M1 is Nonnegative & M2 is_less_or_equal_with M3 implies M2
is_less_or_equal_with M1+M3;
theorem :: MATRIX10:74
M1 is Positive & M2 is_less_or_equal_with M3 implies M2 is_less_than M1+M3;
theorem :: MATRIX10:75
M1 is Nonnegative & M2 is_less_than M3 implies M2 is_less_than M1+M3;
theorem :: MATRIX10:76
M1 is Nonnegative implies M2-M1 is_less_or_equal_with M2;
theorem :: MATRIX10:77
M1 is Positive implies M2-M1 is_less_than M2;
theorem :: MATRIX10:78
M1 is Nonpositive implies M2 is_less_or_equal_with M2-M1;
theorem :: MATRIX10:79
M1 is Negative implies M2 is_less_than M2-M1;
theorem :: MATRIX10:80
M1 is_less_or_equal_with M2 implies M2-M1 is Nonnegative;
theorem :: MATRIX10:81
M1 is Nonnegative & M2 is_less_than M3 implies M2-M1 is_less_than M3;
theorem :: MATRIX10:82
M1 is Nonpositive & M2 is_less_or_equal_with M3 implies M2
is_less_or_equal_with M3-M1;
theorem :: MATRIX10:83
M1 is Nonpositive & M2 is_less_than M3 implies M2 is_less_than M3-M1;
theorem :: MATRIX10:84
M1 is Negative & M2 is_less_or_equal_with M3 implies M2 is_less_than M3-M1;
theorem :: MATRIX10:85
M1 is_less_than M2 & a>0 implies a*M1 is_less_than a*M2;
theorem :: MATRIX10:86
M1 is_less_than M2 & a>=0 implies a*M1 is_less_or_equal_with a*M2;
theorem :: MATRIX10:87
M1 is_less_than M2 & a<0 implies a*M2 is_less_than a*M1;
theorem :: MATRIX10:88
M1 is_less_than M2 & a<=0 implies a*M2 is_less_or_equal_with a*M1;
theorem :: MATRIX10:89
M1 is_less_or_equal_with M2 & a>=0 implies a*M1 is_less_or_equal_with a*M2;
theorem :: MATRIX10:90
M1 is_less_or_equal_with M2 & a<=0 implies a*M2 is_less_or_equal_with a*M1;
theorem :: MATRIX10:91
a>=0 & a<=b & M1 is Nonnegative & M1 is_less_or_equal_with M2 implies
a*M1 is_less_or_equal_with b*M2;
theorem :: MATRIX10:92
a<=0 & b<=a & M1 is Nonpositive & M2 is_less_or_equal_with M1 implies
a*M1 is_less_or_equal_with b*M2;
theorem :: MATRIX10:93
a<0 & b<=a & M1 is Negative & M2 is_less_than M1 implies a*M1
is_less_than b*M2;
theorem :: MATRIX10:94
a>=0 & a**=0 & a****0 & a<=b & M1 is Positive & M1 is_less_than M2 implies a*M1
is_less_than b*M2;
**