FORMALIZED MATHEMATICS
Volume5,Number3,1996
Warsaw University-Bia l ystok
Associated Matrix of Linear Map
Robert Milewski
Warsaw University
Bia l ystok
799什么意思MML Identifier:MATRLIN.
The notation and terminology ud in this paper are introduced in the following articles:[13],[2],[11],[17],[18],[33],[21],[32],[3],[34],[8],[9],[4],[14],[15], [35],[36],[23],[31],[16],[30],[26],[24],[12],[29],[19],[27],[1],[7],[25],[6],[10], [5],[22],[28],and[20].
1.Preliminaries
zhetFor simplicity we follow the rules:k,t,i,j,m,n are natural numbers,x is arbitrary,A is a t,and D is a non empty t.
escape的用法We now state two propositions:
(1)For everyfinite quence p of elements of D and for every i holds p i is
afinite quence of elements of D.
(2)For every i and for everyfinite quence p holds rng(p i)⊆rng p.
Let D be a non empty t.A matrix over D is a tabularfinite quence of elements of D∗.
Let K be afield.A matrix over K is a matrix over the carrier of K.
Let D be a non empty t,let us consider k,and let M be a matrix over D. Then M k is a matrix over D.
Next we state four propositions:
(3)For everyfinite quence M of elements of D such that len M=n+1
holds len(M n+1)=n.
(4)Let M be a matrix over D of dimension n+1×m and let M1be a
matrix over D.Then if n>0,then width M=width(M n+1)and if M1= M(n+1) ,then width M=width M1.
(5)For every matrix M over D of dimension n+1×m holds M n+1is a
matrix over D of dimension n×m.
339c 1996Warsaw University-Bia l ystok
ISSN1426–2630
340
robert milewski (6)For every finite quence M of elements of D such that len M =n +1
holds M =(M len M ) M (len M ) .
Let us consider D and let P be a finite quence of elements of D .Then P is a matrix over D of dimension 1×len P.
2.More on Finite Sequence
One can prove the following propositions:
(7)For every t A and for every finite quence F holds (Sgm(F −1A ))
Sgm(F −1(rng F \A ))is a permutation of dom F.
(8)Let F be a finite quence and let A be a subt of rng F.Suppo
F is one-to-one.Then there exists a permutation p of dom F such that (F −A c )(F −A )=F ·p.
A function is finite quence yielding if:
(Def.1)For every x such that x ∈dom it holds it(x )is a finite quence.
Let us obrve that there exists a function which is finite quence yielding.Let F ,G be finite quence yielding functions.The functor F ⌢G yields a finite quence yielding function and is defined by the conditions (Def.2).(Def.2)(i)dom(F ⌢G )=dom F ∩dom G,and
(ii)for arbitrary i such that i ∈dom(F ⌢G )and for all finite quences f ,g such that f =F (i )and g =G (i )
holds (F ⌢G )(i )=f g.
3.Matrices and Finite Sequences in Vector Space
For simplicity we adopt the following convention:K denotes a field,V de-notes a vector space over K ,a denotes an element of the carrier of K ,W denotes an element of the carrier of V ,K 1,K 2,K 3denote linear combinations of V ,and X denotes a subt of the carrier of V .
Next we state four propositions:
(9)If X is linearly independent and support K 1⊆X and support K 2⊆X and K 1= K 2,then K 1=K 2.
(10)If X is linearly independent and support K 1⊆X and support K 2⊆X and support K 3⊆X and K 1= K 2+ K 3,then K 1=K 2+K 3.
(11)If X is linearly independent and support K 1⊆X and support K 2⊆X and a =0K and K 1=a · K 2,then K 1=a ·K 2.
(12)For every basis b 2of V there exists a linear combination K 4of V such that W = K 4and support K 4⊆b 2.
1849年Let K be a field and let V be a vector space over K .We say that V is finite dimensional if and only if:
(Def.3)There exists finite subt of the carrier of V which is a basis of V .
associated matrix of linear map 341
Let K be a field.Note that there exists a vector space over K which is strict and finite dimensional.
uglyLet K be a field and let V be a finite dimensional vector space over K .A finite quence of elements of the carrier of V is called an ordered basis of V if:(Def.4)It is one-to-one and rng it is a basis of V .
For simplicity we adopt the following convention:p will denote a finite -quence,M 1will denote a matrix over D of dimension n ×m ,M 2will denote a matrix over D of dimension k ×m ,V 1,V 2,V 3will denote finite dimensional vector spaces over K ,f ,f 1,f 2will denote maps from V 1into V 2,g will denote a map from V 2into V 3,b 1will denote an ordered basis of V 1,b 2will denote an ordered basis of V 2,b 3will denote an ordered basis of V 3,b will denote a basis of V 1,v 1,v 2will denote vectors of V 2,v will denote an element of the carrier of V 1,p 2,F will denote finite quences of elements of the carrier of V 1,p 1,d will denote finite quences of elements of the carrier of K ,and K 4will denote a linear combination of V 1.
Let us consider K ,let us consider V 1,V 2,and let us consider f 1,f 2.The functor f 1+f 2yielding a map from V 1into V 2is defined as follows:(Def.5)For every element v of the carrier of V 1holds (f 1+f 2)(v )=f 1(v )+f 2(v ).
Let us consider K ,let us consider V 1,V 2,let us consider f ,and let a be an element of the carrier of K .The functor a ·f yielding a map from V 1into V 2is defined as follows:
(Def.6)For every element v of the carrier of V 1holds (a ·f )(v )=a ·f (v ).
The following propositions are true:
(13)Let a be an element of the carrier of V 1,and let F be a finite quence
of elements of the carrier of V 1,and let G be a finite quence of elements of the carrier of K .Suppo len F =len G and for every k and for every element v of the carrier of K such that k ∈dom F and v =G (k )holds F (k )=v ·a.Then F = G ·a.
(14)Let a be an element of the carrier of V 1,and let F be a finite quence
of elements of the carrier of K ,and let G be a finite quence of elements of the carrier of V 1.If len F
=len G and for every k such that k ∈dom F holds G (k )=πk F ·a,then G = F ·a.(15)If for every k such that k ∈dom F holds πk F =0(V 1),then F =0(V 1).Let us consider K ,let us consider V 1,and let us consider p 1,p 2.The functor lmlt(p 1,p 2)yielding a finite quence of elements of the carrier of V 1is defined as follows:
(Def.7)lmlt(p 1,p 2)=(the left multiplication of V 1)◦(p 1,p 2).
Next we state the proposition
(16)If dom p 1=dom p 2,then dom lmlt(p 1,p 2)=dom p 1and
dom lmlt(p 1,p 2)=dom p 2.
Let us consider K ,let us consider V 1,and let M be a matrix over the carrier of V 1.The functor M yields a finite quence of elements of the carrier of V 1and is defined as follows:
342
robert milewski (Def.8)len M =len M and for every k such that k ∈dom M holds
πk M = Line(M,k ).
The following propositions are true:
(17)For every matrix M over the carrier of V 1such that len M =0holds M =0(V 1).
(18)For every matrix M over the carrier of V 1of dimension m +1×0holds M =0(V 1).
(19)
For every element x of the carrier of V 1holds x = x T .(20)
For every finite quence p of elements of the carrier of V 1such that f is linear holds f ( p )= (f ·p ).(21)Let a be a finite quence of elements of the carrier of K and let p be
a finite quence of elements of the carrier of V 1.If len p =len a,then if f is linear,then f ·lmlt(a,p )=lmlt(a,f ·p ).
少儿英语培训机构排名
(22)Let a be a finite quence of elements of the carrier of K .If len a =len b 2,then if g is linear,then g ( lmlt(a,b 2))= lmlt(a,g ·b 2).
(23)Let F ,F 1be finite quences of elements of the carrier of V 1,and let K 4be a linear combination
of V 1,and let p be a permutation of dom F.If F 1=F ·p,then K 4F 1=(K 4F )·p.(24)If F is one-to-one and support K 4⊆rng F,then (K 4F )= K 4.(25)Let A be a t and let p be a finite quence of elements of the carrier of V 1.Suppo rng p ⊆A.Suppo f 1is linear and f 2is linear and for every v such that v ∈A holds f 1(v )=f 2(v ).Then f 1( p )=f 2( p ).(26)
If f 1is linear and f 2is linear,then for every ordered basis b 1of V 1such that len b 1>0holds if f 1·b 1=f 2·b 1,then f 1=f 2.Let D be a non empty t.Obrve that every matrix over D is finite quence yielding.
Let D be a non empty t and let F ,G be matrices over D .Then F ⌢G is a matrix over D .
Let D be a non empty t,let us consider n ,m ,k ,let M 1be a matrix over D of dimension n ×k ,and let M 2be a matrix over D of dimension m ×k .Then M 1M 2is a matrix over D of dimension n +m ×k .
One can prove the following propositions:
(27)Given i ,and let M 1be a matrix over D of dimension n ×k ,and
let M 2be a matrix over D of dimension m ×k .If i ∈dom M 1,then Line(M 1M 2,i )=Line(M 1,i ).
(28)Let M 1be a matrix over D of dimension n ×k and let M 2be a matrix
over D of dimension m ×k .If width M 1=width M 2,then width(M 1M 2)=width M 1and width(M 1M 2)=width M 2.
(29)Given i ,n ,and let M 1be a matrix over D of dimension t ×k ,and
let M 2be a matrix over D of dimension m ×k .If n ∈dom M 2and i =len M 1+n,then Line(M 1M 2,i )=Line(M 2,n ).
associated matrix of linear map
343(30)Let M 1be a matrix over D of dimension n ×k and let M 2be a matrix
over D of dimension m ×k .If width M 1=width M 2,then for every i such that i ∈Seg width M 1holds (M 1M 2),i =((M 1),i )((M 2),i ).小学生学习
(31)Let M 1be a matrix over the carrier of V 1of dimension n ×k and
let M 2be a matrix over the carrier of V 1of dimension m ×k .Then (M 1M 2)=( M 1) M 2.
(32)Let M 1be a matrix over D of dimension n ×k and let M 2be a matrix
over D of dimension m ×k .If width M 1=width M 2,then (M 1M 2)T =(M 1T )⌢M 2T .
(33)For all matrices M 1,M 2over the carrier of V 1holds (the addition of V 1)◦( M 1, M 2)= (M 1⌢M 2).
Let D be a non empty t,let F be a binary operation on D ,and let P 1,P 2be finite quences of elements of D .Then F ◦(P 1,P 2)is a finite quence of elements of D .
Next we state veral propositions:
(34)Let P 1,P 2be finite quences of elements of the carrier of V 1.If len P 1=
len P 2,then ((the addition of V 1)◦(P 1,P 2))= P 1+ P 2.
(35)For all matrices M 1,M 2over the carrier of V 1such that len M 1=len M 2holds M 1+ M 2= (M 1⌢M 2).
(36)For every finite quence P of elements of the carrier of V 1holds P = ( P T ).
(37)For every n and for every matrix M over the carrier of V 1such that len M =n holds M = (M T ).
(38)Let M be a matrix over the carrier of K of dimension n ×m .Suppo许多人
n >0and m >0.Let p ,d be finite quences of elements of the carrier of K .Suppo len p =n and len d =m and for every j such that j ∈dom d holds πj d = (p •M ,j ).Let b ,c be finite quences of elements of the carrier of V 1.Suppo len b =m and len c =n and for every i such that i ∈dom c holds πi c = lmlt(Line(M,i ),b ).Then lmlt(p,c )= lmlt(d,b ).
4.Decomposition of a Vector in Basis
Let K be a field,let V be a finite dimensional vector space over K ,let b 1be an ordered basis of V ,and let W be an element of the carrier of V .The functor W →b 1yielding a finite quence of elements of the carrier of K is defined by the conditions (Def.9).
(Def.9)(i)len(W →b 1)=len b 1,and (ii)there exists a linear combination K 4of V such that W = K 4and
support K 4⊆rng b 1and for every k such that 1≤k and k ≤len(W →b 1)holds πk (W →b 1)=K 4(πk b 1).
344robert milewski
The following four propositions are true:
(39)If v 1→b 2=v 2→b 2,then v 1=v 2.(40)v = lmlt(v →b 1,b 1).(41)If len d =len b 1,then d = lmlt(d,b 1)→b 1.
(42)Let a be a finite quence of elements of the carrier of K .Suppo
len a =len b 2.Let j be a natural number.Suppo j ∈dom b 3.Let d be a finite quence of elements of the carrier of K .Suppo len d =len b 2and for every k such that k ∈dom b 2holds d (k )=πj (g (πk b 2)→b 3).If len b 2>0and len b 3>0,then πj ( lmlt(a,g ·b 2)→b 3)= (a •d ).
5.Associated Matrix of Linear Map
Let K be a field,let V 1,V 2be finite dimensional vector spaces over K ,let f be a function from the carrier of V 1into the carrier of V 2,let b 1be a finite quence of elements of the carrier of V 1,and let b 2be an ordered basis of V 2.The functor AutMt(f,b 1,b 2)yielding a matrix over K is defined as follows:(Def.10)len AutMt(f,b 1,b 2)=len b 1and for every k such that k ∈dom b 1holds
πk AutMt(f,b 1,b 2)=f (πk b 1)→b 2.
One can prove the following propositions:
(43)If len b 1=0,then AutMt(f,b 1,b 2)=ε.
(44)If len b 1>0,then width AutMt(f,b 1,b 2)=len b 2.
(45)If f 1is linear and f 2is linear,then if AutMt(f 1,b 1,b 2)=
AutMt(f 2,b 1,b 2)and len b 1>0,then f 1=f 2.
(46)If f is linear and g is linear and len b 1>0and len b 2>0and len b 3>0,
七年级上册英语教案
then AutMt(g ·f,b 1,b 3)=AutMt(f,b 1,b 2)·AutMt(g,b 2,b 3).
(47)AutMt(f 1+f 2,b 1,b 2)=AutMt(f 1,b 1,b 2)+AutMt(f 2,b 1,b 2).
(48)If a =0K ,then AutMt(a ·f,b 1,b 2)=a ·AutMt(f,b 1,b 2).
References
[1]
Grzegorz Bancerek.Cardinal numbers.Formalized Mathematics ,1(2):377–382,1990.[2]
Grzegorz Bancerek.The fundamental properties of natural numbers.Formalized Math-ematics ,1(1):41–46,1990.[3]
Grzegorz Bancerek and Krzysztof Hryniewiecki.Segments of natural numbers and finite quences.Formalized Mathematics ,1(1):107–114,1990.[4]
Czes l aw Byli´n ski.Basic functions and operations on functions.Formalized Mathematics ,1(1):245–254,1990.[5]
Czes l aw Byli´n ski.Binary operations.Formalized Mathematics ,1(1):175–180,1990.[6]
Czes l aw Byli´n ski.Binary operations applied to finite quences.Formalized Mathemat-ics ,1(4):643–649,1990.[7]
Czes l aw Byli´n ski.Finite quences and tuples of elements of a non-empty ts.Formal-ized Mathematics ,1(3):529–536,1990.[8]Czes l aw Byli´n ski.Functions and their basic properties.Formalized Mathematics ,湘夫人翻译
1(1):55–65,1990.
