:: Affine Independence in Vector Spaces
:: by Karol P\c{a}k
::
:: Received December 18, 2009
:: Copyright (c) 2009-2021 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 ALGSTR_0, ARYTM_1, ARYTM_3, XBOOLE_0, CARD_1, CONVEX1, CONVEX2,
CONVEX3, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1, FUNCT_1, FUNCT_2,
MONOID_0, ORDERS_1, RELAT_1, RLSUB_1, RLVECT_1, RLVECT_2, RLVECT_3,
RUSUB_4, SEMI_AF1, SETFAM_1, SUBSET_1, TARSKI, CLASSES1, SUPINF_2,
RLVECT_5, REAL_1, NUMBERS, NAT_1, CARD_3, XXREAL_0, STRUCT_0, ZFMISC_1,
RLAFFIN1, ORDINAL1, ORDINAL4, PARTFUN1, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDERS_1, CARD_1, NUMBERS,
XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, FINSET_1, SETFAM_1, DOMAIN_1,
ALGSTR_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, STRUCT_0,
FINSEQ_2, FINSEQ_3, FINSEQOP, CLASSES1, RVSUM_1, RLVECT_1, RLVECT_2,
RLVECT_3, RLVECT_5, RLSUB_1, RLSUB_2, RUSUB_4, CONVEX1, CONVEX2, CONVEX3;
constructors BINOP_1, BINOP_2, CLASSES1, CONVEX1, CONVEX3, FINSEQOP, FINSOP_1,
MATRLIN, ORDERS_1, REALSET1, REAL_1, RLVECT_3, RLVECT_5, RVSUM_1,
RLSUB_2, RUSUB_5, SETWISEO, RELSET_1;
registrations BINOP_2, CARD_1, CONVEX1, FINSET_1, FINSEQ_2, FUNCT_1, FUNCT_2,
NAT_1, NUMBERS, RELAT_1, RLVECT_1, RLVECT_3, RUSUB_4, STRUCT_0, SUBSET_1,
VALUED_0, XCMPLX_0, XREAL_0, XXREAL_0, RLVECT_5, RELSET_1, RLVECT_2,
ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
reserve x,y for set,
r,s for Real,
S for non empty addLoopStr,
LS,LS1,LS2 for Linear_Combination of S,
G for Abelian add-associative right_zeroed right_complementable
non empty addLoopStr,
LG,LG1,LG2 for Linear_Combination of G,
g,h for Element of G,
RLS for non empty RLSStruct,
R for vector-distributive scalar-distributive scalar-associative
scalar-unitalnon empty RLSStruct,
AR for Subset of R,
LR,LR1,LR2 for Linear_Combination of R,
V for RealLinearSpace,
v,v1,v2,w,p for VECTOR of V,
A,B for Subset of V,
F1,F2 for Subset-Family of V,
L,L1,L2 for Linear_Combination of V;
registration
let RLS;
let A be empty Subset of RLS;
cluster conv A -> empty;
end;
registration let RLS;
let A be non empty Subset of RLS;
cluster conv A -> non empty;
end;
theorem :: RLAFFIN1:1
for v be Element of R holds conv {v} = {v};
theorem :: RLAFFIN1:2
for A be Subset of RLS holds A c= conv A;
theorem :: RLAFFIN1:3
for A,B be Subset of RLS st A c= B holds conv A c= conv B;
theorem :: RLAFFIN1:4
for S,A be Subset of RLS st A c= conv S holds conv S = conv(S\/A);
theorem :: RLAFFIN1:5
for V be add-associative non empty addLoopStr
for A be Subset of V for v,w be Element of V
holds (v+w)+A = v+(w+A);
theorem :: RLAFFIN1:6
for V be Abelian right_zeroed non empty addLoopStr for A be Subset of V
holds 0.V + A = A;
theorem :: RLAFFIN1:7
for A be Subset of G holds card A = card (g+A);
theorem :: RLAFFIN1:8
for v be Element of S holds v + {}S = {}S;
theorem :: RLAFFIN1:9
for A,B be Subset of RLS st A c= B holds r*A c= r*B;
theorem :: RLAFFIN1:10
(r*s)* AR = r * (s*AR);
theorem :: RLAFFIN1:11
1 * AR = AR;
theorem :: RLAFFIN1:12
0 * A c= {0.V};
theorem :: RLAFFIN1:13
for F be FinSequence of S holds (LS1+LS2) * F = (LS1*F) + (LS2*F);
theorem :: RLAFFIN1:14
for F be FinSequence of V holds (r*L) * F = r * (L*F);
theorem :: RLAFFIN1:15
A is linearly-independent & A c= B & Lin B = V implies
ex I be linearly-independent Subset of V st A c= I & I c= B & Lin I = V;
begin :: Two Transformations of Linear Combinations
definition
let G,LG,g;
func g + LG -> Linear_Combination of G means
:: RLAFFIN1:def 1
it.h = LG.(h-g);
end;
theorem :: RLAFFIN1:16
Carrier (g+LG) = g + Carrier LG;
theorem :: RLAFFIN1:17
g + (LG1+LG2) = (g+LG1) + (g+LG2);
theorem :: RLAFFIN1:18
v + (r*L) = r * (v+L);
theorem :: RLAFFIN1:19
g + (h+LG) = (g+h) + LG;
theorem :: RLAFFIN1:20
g + ZeroLC G = ZeroLC G;
theorem :: RLAFFIN1:21
0.G + LG = LG;
definition
let R,LR; let r be Real;
func r (*) LR -> Linear_Combination of R means
:: RLAFFIN1:def 2
for v be Element of R holds it.v = LR.(r"*v) if r<>0 otherwise
it = ZeroLC R;
end;
theorem :: RLAFFIN1:22
Carrier (r(*)LR) c= r*Carrier LR;
theorem :: RLAFFIN1:23
r <> 0 implies Carrier (r(*)LR) = r * Carrier LR;
theorem :: RLAFFIN1:24
r (*) (LR1+LR2) = (r(*)LR1) + (r(*)LR2);
theorem :: RLAFFIN1:25
r * (s(*)L) = s (*) (r*L);
theorem :: RLAFFIN1:26
r (*) ZeroLC(R) = ZeroLC R;
theorem :: RLAFFIN1:27
r(*)(s(*)LR)=(r*s)(*)LR;
theorem :: RLAFFIN1:28
1 (*) LR = LR;
begin :: The Sum of Coefficients of a Linear Combination
definition
let S,LS;
func sum LS -> Real means
:: RLAFFIN1:def 3
ex F be FinSequence of S st
F is one-to-one & rng F = Carrier LS & it = Sum (LS*F);
end;
theorem :: RLAFFIN1:29
for F be FinSequence of S st Carrier LS misses rng F holds Sum (LS*F) = 0;
theorem :: RLAFFIN1:30
for F be FinSequence of S st F is one-to-one & Carrier LS c= rng F
holds sum LS = Sum (LS*F);
theorem :: RLAFFIN1:31
sum ZeroLC S = 0;
theorem :: RLAFFIN1:32
for v be Element of S st Carrier LS c= {v} holds sum LS = LS.v;
theorem :: RLAFFIN1:33
for v1,v2 be Element of S st
Carrier LS c= {v1,v2} & v1 <> v2 holds sum LS = LS.v1 + LS.v2;
theorem :: RLAFFIN1:34
sum (LS1+LS2) = sum LS1 + sum LS2;
theorem :: RLAFFIN1:35
sum (r * L) = r * sum L;
theorem :: RLAFFIN1:36
sum (L1-L2) =sum L1 - sum L2;
theorem :: RLAFFIN1:37
sum LG = sum (g+LG);
theorem :: RLAFFIN1:38
r <> 0 implies sum LR = sum (r(*)LR);
theorem :: RLAFFIN1:39
Sum (v + L) = (sum L)*v + Sum L;
theorem :: RLAFFIN1:40
Sum (r(*)L) = r * Sum L;
begin :: Affine Independence of Vectors
definition
let V,A;
attr A is affinely-independent means
:: RLAFFIN1:def 4
A is empty or ex v st v in A & -v + A\{0.V} is linearly-independent;
end;
registration
let V;
cluster empty -> affinely-independent for Subset of V;
let v;
cluster {v} -> affinely-independent for Subset of V;
let w;
cluster {v,w} -> affinely-independent for Subset of V;
end;
registration
let V;
cluster 1-element affinely-independent for Subset of V;
end;
theorem :: RLAFFIN1:41
A is affinely-independent iff for v st v in A holds
-v + A\{0.V} is linearly-independent;
theorem :: RLAFFIN1:42
A is affinely-independent iff
for L be Linear_Combination of A st Sum L = 0.V & sum L = 0
holds Carrier L = {};
theorem :: RLAFFIN1:43
A is affinely-independent & B c= A implies B is affinely-independent;
registration
let V;
cluster linearly-independent -> affinely-independent for Subset of V;
end;
reserve I for affinely-independent Subset of V;
registration
let V,I,v;
cluster v + I -> affinely-independent;
end;
theorem :: RLAFFIN1:44
v+A is affinely-independent implies A is affinely-independent;
registration
let V,I,r;
cluster r*I -> affinely-independent;
end;
theorem :: RLAFFIN1:45
r * A is affinely-independent & r <> 0 implies A is affinely-independent;
theorem :: RLAFFIN1:46
0.V in A implies
(A is affinely-independent iff A \ {0.V} is linearly-independent);
definition
let V;
let F be Subset-Family of V;
attr F is affinely-independent means
:: RLAFFIN1:def 5
A in F implies A is affinely-independent;
end;
registration
let V;
cluster empty -> affinely-independent for Subset-Family of V;
let I;
cluster {I} -> affinely-independent for Subset-Family of V;
end;
registration
let V;
cluster empty affinely-independent for Subset-Family of V;
cluster non empty affinely-independent for Subset-Family of V;
end;
theorem :: RLAFFIN1:47
F1 is affinely-independent & F2 is affinely-independent implies
F1 \/ F2 is affinely-independent;
theorem :: RLAFFIN1:48
F1 c= F2 & F2 is affinely-independent implies F1 is affinely-independent;
begin :: Affine Hull
definition
let RLS;
let A be Subset of RLS;
func Affin A -> Subset of RLS equals
:: RLAFFIN1:def 6
meet {B where B is Affine Subset of RLS : A c= B};
end;
registration
let RLS;
let A be Subset of RLS;
cluster Affin A -> Affine;
end;
registration
let RLS;
let A be empty Subset of RLS;
cluster Affin A -> empty;
end;
registration
let RLS;
let A be non empty Subset of RLS;
cluster Affin A -> non empty;
end;
theorem :: RLAFFIN1:49
for A be Subset of RLS holds A c= Affin A;
theorem :: RLAFFIN1:50
for A be Affine Subset of RLS holds A = Affin A;
theorem :: RLAFFIN1:51
for A,B be Subset of RLS st A c= B & B is Affine holds Affin A c= B;
theorem :: RLAFFIN1:52
for A,B be Subset of RLS st A c= B holds Affin A c= Affin B;
theorem :: RLAFFIN1:53
Affin (v+A) = v + Affin A;
theorem :: RLAFFIN1:54
AR is Affine implies r * AR is Affine;
theorem :: RLAFFIN1:55
r <> 0 implies Affin (r*AR) = r * Affin AR;
theorem :: RLAFFIN1:56
Affin (r*A) = r * Affin A;
theorem :: RLAFFIN1:57
v in Affin A implies Affin A = v + Up Lin (-v+A);
theorem :: RLAFFIN1:58
A is affinely-independent iff for B st B c= A & Affin A = Affin B holds A = B
;
theorem :: RLAFFIN1:59
Affin A = {Sum L where L is Linear_Combination of A : sum L=1};
theorem :: RLAFFIN1:60
I c=A implies ex Ia be affinely-independent Subset of V st
I c= Ia & Ia c= A & Affin Ia = Affin A;
theorem :: RLAFFIN1:61
for A,B be finite Subset of V st
A is affinely-independent & Affin A = Affin B & card B <= card A
holds B is affinely-independent;
theorem :: RLAFFIN1:62
L is convex iff sum L = 1 & for v holds 0 <= L.v;
theorem :: RLAFFIN1:63
L is convex implies L.x <= 1;
theorem :: RLAFFIN1:64
L is convex & L.x = 1 implies Carrier L = {x};
theorem :: RLAFFIN1:65
conv A c= Affin A;
theorem :: RLAFFIN1:66
x in conv A & (conv A)\{x} is convex implies x in A;
theorem :: RLAFFIN1:67
Affin conv A = Affin A;
theorem :: RLAFFIN1:68
conv A c= conv B implies Affin A c= Affin B;
theorem :: RLAFFIN1:69
for A,B be Subset of RLS st A c= Affin B holds Affin (A\/B) = Affin B;
begin :: Barycentric Coordinates
definition
let V;
let A such that
A is affinely-independent;
let x be object such that
x in Affin A;
func x |-- A -> Linear_Combination of A means
:: RLAFFIN1:def 7
Sum it = x & sum it = 1;
end;
theorem :: RLAFFIN1:70
v1 in Affin I & v2 in Affin I implies
((1-r)*v1+r*v2) |-- I = (1-r) * (v1|--I) + r * (v2|--I);
theorem :: RLAFFIN1:71
x in conv I implies x|--I is convex & 0 <= (x|--I).v & (x|--I).v <= 1;
theorem :: RLAFFIN1:72
x in conv I implies ((x|--I).y = 1 iff x = y & x in I);
theorem :: RLAFFIN1:73
for I st x in Affin I & for v st v in I holds 0 <= (x|--I).v
holds x in conv I;
theorem :: RLAFFIN1:74
x in I implies (conv I)\{x} is convex;
theorem :: RLAFFIN1:75
for B st x in Affin I & for y st y in B holds (x|--I).y = 0
holds x in Affin(I\B) & x |-- I = x |-- (I\B);
theorem :: RLAFFIN1:76
for B st x in conv I & for y st y in B holds (x|--I).y = 0
holds x in conv (I\B);
theorem :: RLAFFIN1:77
B c= I & x in Affin B implies x |-- B = x |-- I;
theorem :: RLAFFIN1:78
v1 in Affin A & v2 in Affin A & r+s = 1 implies r*v1 + s*v2 in Affin A;
theorem :: RLAFFIN1:79
for A,B be finite Subset of V st
A is affinely-independent & Affin A c= Affin B
holds card A <= card B;
theorem :: RLAFFIN1:80
for A,B be finite Subset of V st
A is affinely-independent & Affin A c= Affin B & card A = card B
holds B is affinely-independent;
theorem :: RLAFFIN1:81
L1.v <> L2.v implies ((r*L1+(1-r)*L2).v = s iff r = (L2.v-s)/(L2.v-L1.v));
theorem :: RLAFFIN1:82
A\/{v} is affinely-independent iff
A is affinely-independent & (v in A or not v in Affin A);
theorem :: RLAFFIN1:83
not w in Affin A & v1 in A & v2 in A & r<>1 & r*w + (1-r)*v1 = s*w + (1-s)*v2
implies r = s & v1 = v2;
theorem :: RLAFFIN1:84
v in I & w in Affin I & p in Affin(I\{v}) & w = r*v + (1-r)*p
implies r = (w|--I).v;