let n be Nat; for K being Field
for M being Matrix of n,K holds
( M is lower_triangular Matrix of n,K iff M @ is upper_triangular Matrix of n,K )
let K be Field; for M being Matrix of n,K holds
( M is lower_triangular Matrix of n,K iff M @ is upper_triangular Matrix of n,K )
let M be Matrix of n,K; ( M is lower_triangular Matrix of n,K iff M @ is upper_triangular Matrix of n,K )
thus
( M is lower_triangular Matrix of n,K implies M @ is upper_triangular Matrix of n,K )
( M @ is upper_triangular Matrix of n,K implies M is lower_triangular Matrix of n,K )proof
assume A1:
M is
lower_triangular Matrix of
n,
K
;
M @ is upper_triangular Matrix of n,K
now for i, j being Nat st [i,j] in Indices (M @) & i > j holds
(M @) * (i,j) = 0. Klet i,
j be
Nat;
( [i,j] in Indices (M @) & i > j implies (M @) * (i,j) = 0. K )assume that A2:
[i,j] in Indices (M @)
and A3:
i > j
;
(M @) * (i,j) = 0. KA4:
[j,i] in Indices M
by A2, MATRIX_0:def 6;
then
M * (
j,
i)
= 0. K
by A1, A3, MATRIX_1:def 9;
hence
(M @) * (
i,
j)
= 0. K
by A4, MATRIX_0:def 6;
verum end;
hence
M @ is
upper_triangular Matrix of
n,
K
by MATRIX_1:def 8;
verum
end;
assume A5:
M @ is upper_triangular Matrix of n,K
; M is lower_triangular Matrix of n,K
now for i, j being Nat st [i,j] in Indices M & i < j holds
M * (i,j) = 0. Klet i,
j be
Nat;
( [i,j] in Indices M & i < j implies M * (i,j) = 0. K )assume that A6:
[i,j] in Indices M
and A7:
i < j
;
M * (i,j) = 0. K
[j,i] in Indices (M @)
by A6, MATRIX_0:def 6;
then
(M @) * (
j,
i)
= 0. K
by A5, A7, MATRIX_1:def 8;
hence
M * (
i,
j)
= 0. K
by A6, MATRIX_0:def 6;
verum end;
hence
M is lower_triangular Matrix of n,K
by MATRIX_1:def 9; verum