I want to prove a property of linear space. Property description as follows:
If exist unique β, and β = p1α1+p2α2+…+pnαn , then α1,α2, … , αn linearly
independent.
Where β, α1,α2, … , αn are the elements of linearly space, and p1,p2, … , pn
are complex.
Derivation：
β = p1α1+p2α2+…+pnαn (1)
0 = k1α1+k2α2+…+knαn (2)
(1)+ (2) ==> β = p1α1+p2α2+…+pnαn = (k1+p1)α1+(k2+p2)α2+…+(kn+pn)αn
==> k1=0, k2=0,…, kn=0 ==> α1,α2, … , αn linearly independent
Now, I have proved a goal, and save it as a theorem.
g `!k:complex x:'a. (k LM x = ls0) /\ (x <> ls0) ==> (k = 0)`
Where “LM” is multiplication sign of linear space, “ls0” is zero of linear
space.
My question is how to prove the goal as follows?
g `!l1:complex list l2:'a list. (LENGTH l1 = LENGTH l2) /\ (LMP(l1,l2) =
ls0) /\ (EVERY P l2) ==> (EVERY Q l1)`;
Where“LN” is plus of linear space.
val ls_mult_add = Define
`(LMP ([],l2:'a list) = ls0) /\
(LMP ((h1::t1):complex list,l2:'a list) = if (l2 = []) then ls0
else (h1 LM HD l2) LP
(LMP (t1,TL l2)))`;
if l1=(p1,p2,…,pn), l2=(α1,α2,…,αn) , then LMP(l1,l2) = p1α1+p2α2+…+pnαn
val Q_def = Define `!x:complex. Q x = (x = 0c)`;
val P_def = Define `!x:'a. P x = (x <> ls0)`;
I am looking forward your advice.
Thanks.
Peng.
------------------------------------------------------------------------------
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_d2d_mar
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
