:: Some Special Matrices of Real Elements and Their Properties
:: by Xiquan Liang , Fuguo Ge and Xiaopeng Yue
::
:: Received October 19, 2006
:: Copyright (c) 2006 Association of Mizar Users
definition
let M be
Matrix of
REAL ;
attr M is
Positive means :
Def1:
:: MATRIX10:def 1
for
i,
j being
Nat st
[i,j] in Indices M holds
M * i,
j > 0 ;
attr M is
Negative means :
Def2:
:: MATRIX10:def 2
for
i,
j being
Nat st
[i,j] in Indices M holds
M * i,
j < 0 ;
attr M is
Nonpositive means :
Def3:
:: MATRIX10:def 3
for
i,
j being
Nat st
[i,j] in Indices M holds
M * i,
j <= 0 ;
attr M is
Nonnegative means :
Def4:
:: MATRIX10:def 4
for
i,
j being
Nat st
[i,j] in Indices M holds
M * i,
j >= 0 ;
end;
:: deftheorem Def1 defines Positive MATRIX10:def 1 :
:: deftheorem Def2 defines Negative MATRIX10:def 2 :
:: deftheorem Def3 defines Nonpositive MATRIX10:def 3 :
:: deftheorem Def4 defines Nonnegative MATRIX10:def 4 :
:: deftheorem Def5 defines is_less_than MATRIX10:def 5 :
:: deftheorem Def6 defines is_less_or_equal_with MATRIX10:def 6 :
definition
let M be
Matrix of
REAL ;
func |:M:| -> Matrix of
REAL means :
Def7:
:: MATRIX10:def 7
(
len it = len M &
width it = width M & ( for
i,
j being
Nat st
[i,j] in Indices M holds
it * i,
j = abs (M * i,j) ) );
existence
ex b1 being Matrix of REAL st
( len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * i,j = abs (M * i,j) ) )
uniqueness
for b1, b2 being Matrix of REAL st len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b1 * i,j = abs (M * i,j) ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds
b2 * i,j = abs (M * i,j) ) holds
b1 = b2
end;
:: deftheorem Def7 defines |: MATRIX10:def 7 :
registration
let n be
Nat;
cluster n,
n --> 1
-> Positive Matrix of
n,
REAL ;
coherence
n,n --> 1 is Positive Matrix of n, REAL
cluster n,
n --> (- 1) -> Negative Matrix of
n,
REAL ;
coherence
n,n --> (- 1) is Negative Matrix of n, REAL
cluster n,
n --> (- 1) -> Nonpositive Matrix of
n,
REAL ;
coherence
n,n --> (- 1) is Nonpositive Matrix of n, REAL
cluster n,
n --> 1
-> Nonnegative Matrix of
n,
REAL ;
coherence
n,n --> 1 is Nonnegative Matrix of n, REAL
end;
Lm1:
for n being Nat
for M1, M2 being Matrix of n, REAL holds
( len M1 = len M2 & width M1 = width M2 )
theorem :: MATRIX10:1
theorem Th2: :: MATRIX10:2
theorem Th3: :: MATRIX10:3
theorem Th4: :: MATRIX10:4
theorem Th5: :: MATRIX10:5
theorem :: MATRIX10:6
theorem :: MATRIX10:7
theorem :: MATRIX10:8
theorem :: MATRIX10:9
theorem :: MATRIX10:10
theorem :: MATRIX10:11
theorem :: MATRIX10:12
theorem :: MATRIX10:13
theorem :: MATRIX10:14
theorem :: MATRIX10:15
theorem :: MATRIX10:16
theorem :: MATRIX10:17
theorem :: MATRIX10:18
theorem :: MATRIX10:19
theorem :: MATRIX10:20
theorem :: MATRIX10:21
theorem :: MATRIX10:22
theorem :: MATRIX10:23
theorem :: MATRIX10:24
theorem :: MATRIX10:25
theorem :: MATRIX10:26
theorem :: MATRIX10:27
theorem :: MATRIX10:28
theorem :: MATRIX10:29
theorem :: MATRIX10:30
theorem :: MATRIX10:31
theorem :: MATRIX10:32
theorem :: MATRIX10:33
theorem :: MATRIX10:34
theorem :: MATRIX10:35
theorem Th36: :: MATRIX10:36
theorem :: MATRIX10:37
theorem :: MATRIX10:38
theorem :: MATRIX10:39
theorem :: MATRIX10:40
theorem :: MATRIX10:41
theorem Th42: :: MATRIX10:42
theorem :: MATRIX10:43
theorem :: MATRIX10:44
theorem :: MATRIX10:45
theorem :: MATRIX10:46
theorem :: MATRIX10:47
theorem :: MATRIX10:48
theorem :: MATRIX10:49
theorem :: MATRIX10:50
theorem :: MATRIX10:51
theorem :: MATRIX10:52
theorem :: MATRIX10:53
theorem :: MATRIX10:54
theorem :: MATRIX10:55
theorem :: MATRIX10:56
theorem :: MATRIX10:57
theorem :: MATRIX10:58
theorem :: MATRIX10:59
theorem :: MATRIX10:60
theorem :: MATRIX10:61
theorem :: MATRIX10:62
theorem :: MATRIX10:63
theorem :: MATRIX10:64
theorem :: MATRIX10:65
theorem :: MATRIX10:66
theorem :: MATRIX10:67
theorem :: MATRIX10:68
theorem :: MATRIX10:69
theorem :: MATRIX10:70
theorem :: MATRIX10:71
theorem :: MATRIX10:72
theorem :: MATRIX10:73
theorem :: MATRIX10:74
theorem :: MATRIX10:75
theorem :: MATRIX10:76
theorem :: MATRIX10:77
theorem :: MATRIX10:78
theorem :: MATRIX10:79
theorem :: MATRIX10:80
theorem :: MATRIX10:81
theorem :: MATRIX10:82
theorem :: MATRIX10:83
theorem :: MATRIX10:84
theorem :: MATRIX10:85
theorem :: MATRIX10:86
theorem :: MATRIX10:87
theorem :: MATRIX10:88
theorem :: MATRIX10:89
theorem :: MATRIX10:90
theorem :: MATRIX10:91
theorem :: MATRIX10:92
theorem :: MATRIX10:93
theorem :: MATRIX10:94
theorem :: MATRIX10:95
theorem :: MATRIX10:96