begin
Lm1:
for r being Real
for V being RealLinearSpace
for u, w, v being VECTOR of V st r <> 1 & (r * u) + ((1 - r) * w) = v holds
w = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u)
theorem Th1:
theorem
theorem Th3:
theorem
begin
:: deftheorem Def1 defines Int RLAFFIN2:def 1 :
Lm2:
for V being non empty RLSStruct
for A being Subset of V holds Int A c= conv A
theorem
theorem
theorem
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem
begin
:: deftheorem Def2 defines center_of_mass RLAFFIN2:def 2 :
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem
theorem Th24:
Lm3:
for r, s being Real
for V being RealLinearSpace
for v being VECTOR of V
for L1, L2 being Linear_Combination of V st L1 . v <> L2 . v holds
( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) )
theorem Th25:
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem