:: deftheorem defines convex CONVEX1:def 3 :
for V being RealLinearSpace
for L being Linear_Combination of V holds
( L is convex iff ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) ) );