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 :
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem Th20:
theorem Th21:
:: deftheorem Def2 defines (*) RLAFFIN1:def 2 :
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem Th26:
theorem Th27:
theorem Th28:
begin
:: deftheorem Def3 defines sum RLAFFIN1:def 3 :
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 :
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 :
theorem
theorem
begin
:: deftheorem defines Affin RLAFFIN1:def 6 :
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 :
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem
theorem Th75:
theorem
theorem Th77:
theorem Th78:
theorem Th79:
theorem
theorem
theorem
theorem
theorem