let V be RealLinearSpace; :: thesis: for M being Subset of V st ( for N being Subset of V

for L being Linear_Combination of N st L is convex & N c= M holds

Sum L in M ) holds

M is convex

let M be Subset of V; :: thesis: ( ( for N being Subset of V

for L being Linear_Combination of N st L is convex & N c= M holds

Sum L in M ) implies M is convex )

assume A1: for N being Subset of V

for L being Linear_Combination of N st L is convex & N c= M holds

Sum L in M ; :: thesis: M is convex

let u, v be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for b_{1} being object holds

( b_{1} <= 0 or 1 <= b_{1} or not u in M or not v in M or (b_{1} * u) + ((1 - b_{1}) * v) in M )

let rr be Real; :: thesis: ( rr <= 0 or 1 <= rr or not u in M or not v in M or (rr * u) + ((1 - rr) * v) in M )

reconsider r = rr as Real ;

assume that

A2: 0 < rr and

A3: rr < 1 and

A4: ( u in M & v in M ) ; :: thesis: (rr * u) + ((1 - rr) * v) in M

set N = {u,v};

A5: {u,v} c= M by A4, ZFMISC_1:32;

reconsider N = {u,v} as Subset of V ;

for L being Linear_Combination of N st L is convex & N c= M holds

Sum L in M ) holds

M is convex

let M be Subset of V; :: thesis: ( ( for N being Subset of V

for L being Linear_Combination of N st L is convex & N c= M holds

Sum L in M ) implies M is convex )

assume A1: for N being Subset of V

for L being Linear_Combination of N st L is convex & N c= M holds

Sum L in M ; :: thesis: M is convex

let u, v be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for b

( b

let rr be Real; :: thesis: ( rr <= 0 or 1 <= rr or not u in M or not v in M or (rr * u) + ((1 - rr) * v) in M )

reconsider r = rr as Real ;

assume that

A2: 0 < rr and

A3: rr < 1 and

A4: ( u in M & v in M ) ; :: thesis: (rr * u) + ((1 - rr) * v) in M

set N = {u,v};

A5: {u,v} c= M by A4, ZFMISC_1:32;

reconsider N = {u,v} as Subset of V ;

now :: thesis: (rr * u) + ((1 - rr) * v) in Mend;

hence
(rr * u) + ((1 - rr) * v) in M
; :: thesis: verumper cases
( u <> v or u = v )
;

end;

suppose A6:
u <> v
; :: thesis: (rr * u) + ((1 - rr) * v) in M

consider L being Linear_Combination of {u,v} such that

A7: ( L . u = r & L . v = 1 - r ) by A6, RLVECT_4:38;

reconsider L = L as Linear_Combination of N ;

A8: L is convex

hence (rr * u) + ((1 - rr) * v) in M by A1, A5, A8; :: thesis: verum

end;A7: ( L . u = r & L . v = 1 - r ) by A6, RLVECT_4:38;

reconsider L = L as Linear_Combination of N ;

A8: L is convex

proof

Sum L = (r * u) + ((1 - r) * v)
by A6, A7, RLVECT_2:33;
A9:
r - r < 1 - r
by A3, XREAL_1:9;

then v in { w where w is Element of V : L . w <> 0 } by A7;

then A10: v in Carrier L by RLVECT_2:def 4;

A11: for n being Element of NAT st n in dom <*r,(1 - r)*> holds

( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )

then u in Carrier L by RLVECT_2:def 4;

then A15: ( Carrier L c= {u,v} & {u,v} c= Carrier L ) by A10, RLVECT_2:def 6, ZFMISC_1:32;

take F = <*u,v*>; :: according to CONVEX1:def 3 :: thesis: ( F is one-to-one & rng F = Carrier L & ex b_{1} being FinSequence of REAL st

( len b_{1} = len F & Sum b_{1} = 1 & ( for b_{2} being set holds

( not b_{2} in dom b_{1} or ( b_{1} . b_{2} = L . (F . b_{2}) & 0 <= b_{1} . b_{2} ) ) ) ) )

A16: Sum <*r,(1 - r)*> = r + (1 - r) by RVSUM_1:77

.= 1 ;

thus F is one-to-one by A6, FINSEQ_3:94; :: thesis: ( rng F = Carrier L & ex b_{1} being FinSequence of REAL st

( len b_{1} = len F & Sum b_{1} = 1 & ( for b_{2} being set holds

( not b_{2} in dom b_{1} or ( b_{1} . b_{2} = L . (F . b_{2}) & 0 <= b_{1} . b_{2} ) ) ) ) )

thus rng F = (rng <*u*>) \/ (rng <*v*>) by FINSEQ_1:31

.= {u} \/ (rng <*v*>) by FINSEQ_1:38

.= {u} \/ {v} by FINSEQ_1:38

.= {u,v} by ENUMSET1:1

.= Carrier L by A15, XBOOLE_0:def 10 ; :: thesis: ex b_{1} being FinSequence of REAL st

( len b_{1} = len F & Sum b_{1} = 1 & ( for b_{2} being set holds

( not b_{2} in dom b_{1} or ( b_{1} . b_{2} = L . (F . b_{2}) & 0 <= b_{1} . b_{2} ) ) ) )

reconsider r = r as Element of REAL by XREAL_0:def 1;

reconsider jr = 1 - r as Element of REAL by XREAL_0:def 1;

take f = <*r,jr*>; :: thesis: ( len f = len F & Sum f = 1 & ( for b_{1} being set holds

( not b_{1} in dom f or ( f . b_{1} = L . (F . b_{1}) & 0 <= f . b_{1} ) ) ) )

len <*r,(1 - r)*> = 2 by FINSEQ_1:44

.= len <*u,v*> by FINSEQ_1:44 ;

hence ( 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 A16, A11; :: thesis: verum

end;then v in { w where w is Element of V : L . w <> 0 } by A7;

then A10: v in Carrier L by RLVECT_2:def 4;

A11: for n being Element of NAT st n in dom <*r,(1 - r)*> holds

( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )

proof

u in { w where w is Element of V : L . w <> 0 }
by A2, A7;
let n be Element of NAT ; :: thesis: ( n in dom <*r,(1 - r)*> implies ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) )

assume n in dom <*r,(1 - r)*> ; :: thesis: ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )

then n in Seg (len <*r,(1 - r)*>) by FINSEQ_1:def 3;

then A12: n in {1,2} by FINSEQ_1:2, FINSEQ_1:44;

end;assume n in dom <*r,(1 - r)*> ; :: thesis: ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )

then n in Seg (len <*r,(1 - r)*>) by FINSEQ_1:def 3;

then A12: n in {1,2} by FINSEQ_1:2, FINSEQ_1:44;

now :: thesis: ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )end;

hence
( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )
; :: thesis: verumper cases
( n = 1 or n = 2 )
by A12, TARSKI:def 2;

end;

then u in Carrier L by RLVECT_2:def 4;

then A15: ( Carrier L c= {u,v} & {u,v} c= Carrier L ) by A10, RLVECT_2:def 6, ZFMISC_1:32;

take F = <*u,v*>; :: according to CONVEX1:def 3 :: thesis: ( F is one-to-one & rng F = Carrier L & ex b

( len b

( not b

A16: Sum <*r,(1 - r)*> = r + (1 - r) by RVSUM_1:77

.= 1 ;

thus F is one-to-one by A6, FINSEQ_3:94; :: thesis: ( rng F = Carrier L & ex b

( len b

( not b

thus rng F = (rng <*u*>) \/ (rng <*v*>) by FINSEQ_1:31

.= {u} \/ (rng <*v*>) by FINSEQ_1:38

.= {u} \/ {v} by FINSEQ_1:38

.= {u,v} by ENUMSET1:1

.= Carrier L by A15, XBOOLE_0:def 10 ; :: thesis: ex b

( len b

( not b

reconsider r = r as Element of REAL by XREAL_0:def 1;

reconsider jr = 1 - r as Element of REAL by XREAL_0:def 1;

take f = <*r,jr*>; :: thesis: ( len f = len F & Sum f = 1 & ( for b

( not b

len <*r,(1 - r)*> = 2 by FINSEQ_1:44

.= len <*u,v*> by FINSEQ_1:44 ;

hence ( 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 A16, A11; :: thesis: verum

hence (rr * u) + ((1 - rr) * v) in M by A1, A5, A8; :: thesis: verum

suppose A17:
u = v
; :: thesis: (rr * u) + ((1 - rr) * v) in M

consider L being Linear_Combination of {u} such that

A18: L . u = jj by RLVECT_4:37;

reconsider L = L as Linear_Combination of N by A17, ENUMSET1:29;

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 ) ) ) )

then A23: Sum L in M by A1, A5;

(r * u) + ((1 - r) * v) = (r + (1 - r)) * u by A17, RLVECT_1:def 6

.= (0 + 1) * u ;

hence (rr * u) + ((1 - rr) * v) in M by A18, A23, RLVECT_2:32; :: thesis: verum

end;A18: L . u = jj by RLVECT_4:37;

reconsider L = L as Linear_Combination of N by A17, ENUMSET1:29;

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 ) ) ) )

proof

then
L is convex
;
take
<*u*>
; :: thesis: ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex f being FinSequence of REAL st

( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds

( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) )

A19: ex f being FinSequence of REAL st

( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds

( f . n = L . (<*u*> . n) & f . n >= 0 ) ) )

then A22: u in Carrier L by RLVECT_2:def 4;

v in { w where w is Element of V : L . w <> 0 } by A17, A18;

then v in Carrier L by RLVECT_2:def 4;

then ( Carrier L c= {u,v} & {u,v} c= Carrier L ) by A22, RLVECT_2:def 6, ZFMISC_1:32;

then Carrier L = {u,v} by XBOOLE_0:def 10;

then Carrier L = {u} by A17, ENUMSET1:29;

hence ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex f being FinSequence of REAL st

( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds

( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) ) by A19, FINSEQ_1:38, FINSEQ_3:93; :: thesis: verum

end;( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds

( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) )

A19: ex f being FinSequence of REAL st

( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds

( f . n = L . (<*u*> . n) & f . n >= 0 ) ) )

proof

u in { w where w is Element of V : L . w <> 0 }
by A18;
take
<*rr*>
; :: thesis: ( len <*rr*> = len <*u*> & Sum <*rr*> = 1 & ( for n being Nat st n in dom <*rr*> holds

( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ) )

A20: for n being Element of NAT st n in dom <*rr*> holds

( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 )

.= len <*u*> by FINSEQ_1:39 ;

hence ( len <*rr*> = len <*u*> & Sum <*rr*> = 1 & ( for n being Nat st n in dom <*rr*> holds

( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ) ) by A20, FINSOP_1:11; :: thesis: verum

end;( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ) )

A20: for n being Element of NAT st n in dom <*rr*> holds

( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 )

proof

len <*1*> =
1
by FINSEQ_1:39
let n be Element of NAT ; :: thesis: ( n in dom <*rr*> implies ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) )

assume n in dom <*rr*> ; :: thesis: ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 )

then n in {1} by FINSEQ_1:2, FINSEQ_1:38;

then A21: n = 1 by TARSKI:def 1;

then <*rr*> . n = 1 by FINSEQ_1:40

.= L . (<*u*> . n) by A18, A21, FINSEQ_1:40 ;

hence ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ; :: thesis: verum

end;assume n in dom <*rr*> ; :: thesis: ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 )

then n in {1} by FINSEQ_1:2, FINSEQ_1:38;

then A21: n = 1 by TARSKI:def 1;

then <*rr*> . n = 1 by FINSEQ_1:40

.= L . (<*u*> . n) by A18, A21, FINSEQ_1:40 ;

hence ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ; :: thesis: verum

.= len <*u*> by FINSEQ_1:39 ;

hence ( len <*rr*> = len <*u*> & Sum <*rr*> = 1 & ( for n being Nat st n in dom <*rr*> holds

( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ) ) by A20, FINSOP_1:11; :: thesis: verum

then A22: u in Carrier L by RLVECT_2:def 4;

v in { w where w is Element of V : L . w <> 0 } by A17, A18;

then v in Carrier L by RLVECT_2:def 4;

then ( Carrier L c= {u,v} & {u,v} c= Carrier L ) by A22, RLVECT_2:def 6, ZFMISC_1:32;

then Carrier L = {u,v} by XBOOLE_0:def 10;

then Carrier L = {u} by A17, ENUMSET1:29;

hence ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex f being FinSequence of REAL st

( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds

( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) ) by A19, FINSEQ_1:38, FINSEQ_3:93; :: thesis: verum

then A23: Sum L in M by A1, A5;

(r * u) + ((1 - r) * v) = (r + (1 - r)) * u by A17, RLVECT_1:def 6

.= (0 + 1) * u ;

hence (rr * u) + ((1 - rr) * v) in M by A18, A23, RLVECT_2:32; :: thesis: verum