let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V

for v being VECTOR of V st L is convex & L . v <= 0 holds

not v in Carrier L

let L be Linear_Combination of V; :: thesis: for v being VECTOR of V st L is convex & L . v <= 0 holds

not v in Carrier L

let v be VECTOR of V; :: thesis: ( L is convex & L . v <= 0 implies not v in Carrier L )

assume that

A1: L is convex and

A2: L . v <= 0 ; :: thesis: not v in Carrier L

for v being VECTOR of V st L is convex & L . v <= 0 holds

not v in Carrier L

let L be Linear_Combination of V; :: thesis: for v being VECTOR of V st L is convex & L . v <= 0 holds

not v in Carrier L

let v be VECTOR of V; :: thesis: ( L is convex & L . v <= 0 implies not v in Carrier L )

assume that

A1: L is convex and

A2: L . v <= 0 ; :: thesis: not v in Carrier L

per cases
( L . v = 0 or L . v < 0 )
by A2;

end;

suppose A3:
L . v < 0
; :: thesis: not v in Carrier L

end;

now :: thesis: not v in Carrier L

hence
not v in Carrier L
; :: thesis: verumconsider F being FinSequence of the carrier of V such that

F is one-to-one and

A4: rng F = Carrier L and

A5: 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

A6: n in dom F and

A7: F . n = v by A4, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A6;

consider f being FinSequence of REAL such that

A8: len f = len F and

Sum f = 1 and

A9: for n being Nat st n in dom f holds

( f . n = L . (F . n) & f . n >= 0 ) by A5;

n in Seg (len F) by A6, FINSEQ_1:def 3;

then A10: n in dom f by A8, FINSEQ_1:def 3;

then L . v = f . n by A9, A7;

hence contradiction by A3, A9, A10; :: thesis: verum

end;F is one-to-one and

A4: rng F = Carrier L and

A5: 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

A6: n in dom F and

A7: F . n = v by A4, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A6;

consider f being FinSequence of REAL such that

A8: len f = len F and

Sum f = 1 and

A9: for n being Nat st n in dom f holds

( f . n = L . (F . n) & f . n >= 0 ) by A5;

n in Seg (len F) by A6, FINSEQ_1:def 3;

then A10: n in dom f by A8, FINSEQ_1:def 3;

then L . v = f . n by A9, A7;

hence contradiction by A3, A9, A10; :: thesis: verum