let V be ComplexLinearSpace; :: thesis: for L being C_Linear_Combination of V
for v being VECTOR of V st L is convex & ex r being Real st
( r = L . v & r <= 0 ) holds
not v in Carrier L
let L be C_Linear_Combination of V; :: thesis: for v being VECTOR of V st L is convex & ex r being Real st
( r = L . v & r <= 0 ) holds
not v in Carrier L
let v be VECTOR of V; :: thesis: ( L is convex & ex r being Real st
( r = L . v & r <= 0 ) implies not v in Carrier L )
assume that
A1: L is convex and
A2: ex r being Real st
( r = L . v & r <= 0 ) ; :: thesis: not v in Carrier L
consider r being Real such that
A3: r = L . v and
A4: r <= 0 by A2;
per cases ( r = 0 or r < 0 ) by A4;
suppose r = 0 ; :: thesis: not v in Carrier L
hence not v in Carrier L by A3, Th1; :: thesis: verum
end;
suppose A5: r < 0 ; :: thesis: not v in Carrier L
now :: thesis: not v in Carrier L
consider F being FinSequence of the carrier of V such that
F is one-to-one and
A6: rng F = Carrier L and
A7: 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 ) ) ) by A1;
assume v in Carrier L ; :: thesis: contradiction
then consider n being object such that
A8: n in dom F and
A9: F . n = v by A6, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A8;
consider f being FinSequence of REAL such that
A10: len f = len F and
Sum f = 1 and
A11: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) by A7;
n in Seg (len F) by A8, FINSEQ_1:def 3;
then A12: n in dom f by A10, FINSEQ_1:def 3;
then L . v = f . n by A11, A9;
hence contradiction by A3, A5, A11, A12; :: thesis: verum
end;
hence not v in Carrier L ; :: thesis: verum
end;
end;