begin
Lm1:
for RLS being non empty RLSStruct
for A being Subset of RLS holds A c= conv A
theorem
theorem
theorem Th3:
theorem
Lm2:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for A, B being Subset of V
for v being Element of V holds (v + A) \ (v + B) = v + (A \ B)
Lm3:
for S being non empty addLoopStr
for v, w being Element of S holds {(v + w)} = v + {w}
theorem Th5:
theorem Th6:
Lm4:
for V being non empty addLoopStr
for A being Subset of V
for v being Element of V holds card (v + A) c= card A
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
begin
:: deftheorem Def1 defines + RLAFFIN1:def 1 :
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for LG being Linear_Combination of G
for g being Element of G
for b4 being Linear_Combination of G holds
( b4 = g + LG iff for h being Element of G holds b4 . h = LG . (h - g) );
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem Th20:
theorem Th21:
:: deftheorem Def2 defines (*) RLAFFIN1:def 2 :
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R
for r being Real
for b4 being Linear_Combination of R holds
( ( r <> 0 implies ( b4 = r (*) LR iff for v being Element of R holds b4 . v = LR . ((r " ) * v) ) ) & ( not r <> 0 implies ( b4 = r (*) LR iff b4 = ZeroLC R ) ) );
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem Th26:
theorem Th27:
theorem Th28:
begin
:: deftheorem Def3 defines sum RLAFFIN1:def 3 :
for S being non empty addLoopStr
for LS being Linear_Combination of S
for b3 being Real holds
( b3 = sum LS iff ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & b3 = Sum (LS * F) ) );
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
begin
:: deftheorem Def4 defines affinely-independent RLAFFIN1:def 4 :
for V being RealLinearSpace
for A being Subset of V holds
( A is affinely-independent iff ( A is empty or ex v being VECTOR of V st
( v in A & ((- v) + A) \ {(0. V)} is linearly-independent ) ) );
Lm5:
for V being RealLinearSpace
for A being Subset of V st A is affinely-independent holds
for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {}
Lm6:
for V being RealLinearSpace
for A being Subset of V st ( for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} ) holds
for p being VECTOR of V st p in A holds
((- p) + A) \ {(0. V)} is linearly-independent
theorem Th41:
theorem Th42:
theorem Th43:
theorem
theorem
theorem Th46:
:: deftheorem Def5 defines affinely-independent RLAFFIN1:def 5 :
for V being RealLinearSpace
for F being Subset-Family of V holds
( F is affinely-independent iff for A being Subset of V st A in F holds
A is affinely-independent );
theorem
theorem
begin
:: deftheorem defines Affin RLAFFIN1:def 6 :
for RLS being non empty RLSStruct
for A being Subset of RLS holds Affin A = meet { B where B is Affine Subset of RLS : A c= B } ;
Lm7:
for V being non empty RLSStruct
for A being Subset of V holds A c= Affin A
Lm8:
for V being non empty RLSStruct
for A being Affine Subset of V holds A = Affin A
theorem
theorem
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem
theorem Th57:
Lm9:
for V being RealLinearSpace
for A being Subset of V holds Lin (A \/ {(0. V)}) = Lin A
theorem Th58:
theorem Th59:
theorem Th60:
theorem
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem
theorem Th67:
theorem
theorem Th69:
begin
:: deftheorem Def7 defines |-- RLAFFIN1:def 7 :
for V being RealLinearSpace
for A being Subset of V st A is affinely-independent holds
for x being set st x in Affin A holds
for b4 being Linear_Combination of A holds
( b4 = x |-- A iff ( Sum b4 = x & sum b4 = 1 ) );
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem
theorem Th75:
theorem
theorem Th77:
theorem Th78:
theorem Th79:
theorem
theorem
theorem
theorem
theorem