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

for v being VECTOR of V holds

( M is convex iff v + M is convex )

let M be Subset of V; :: thesis: for v being VECTOR of V holds

( M is convex iff v + M is convex )

let v be VECTOR of V; :: thesis: ( M is convex iff v + M is convex )

A1: ( v + M is convex implies M is convex )

for v being VECTOR of V holds

( M is convex iff v + M is convex )

let M be Subset of V; :: thesis: for v being VECTOR of V holds

( M is convex iff v + M is convex )

let v be VECTOR of V; :: thesis: ( M is convex iff v + M is convex )

A1: ( v + M is convex implies M is convex )

proof

( M is convex implies v + M is convex )
assume A2:
v + M is convex
; :: thesis: M is convex

let w1, w2 be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for r being Real st 0 < r & r < 1 & w1 in M & w2 in M holds

(r * w1) + ((1 - r) * w2) in M

let r be Real; :: thesis: ( 0 < r & r < 1 & w1 in M & w2 in M implies (r * w1) + ((1 - r) * w2) in M )

assume that

A3: ( 0 < r & r < 1 ) and

A4: w1 in M and

A5: w2 in M ; :: thesis: (r * w1) + ((1 - r) * w2) in M

set x2 = v + w2;

v + w2 in { (v + w) where w is VECTOR of V : w in M } by A5;

then A6: v + w2 in v + M by RUSUB_4:def 8;

set x1 = v + w1;

A7: (r * (v + w1)) + ((1 - r) * (v + w2)) = ((r * v) + (r * w1)) + ((1 - r) * (v + w2)) by RLVECT_1:def 5

.= ((r * v) + (r * w1)) + (((1 - r) * v) + ((1 - r) * w2)) by RLVECT_1:def 5

.= (((r * v) + (r * w1)) + ((1 - r) * v)) + ((1 - r) * w2) by RLVECT_1:def 3

.= (((r * v) + ((1 - r) * v)) + (r * w1)) + ((1 - r) * w2) by RLVECT_1:def 3

.= (((r + (1 - r)) * v) + (r * w1)) + ((1 - r) * w2) by RLVECT_1:def 6

.= (v + (r * w1)) + ((1 - r) * w2) by RLVECT_1:def 8

.= v + ((r * w1) + ((1 - r) * w2)) by RLVECT_1:def 3 ;

v + w1 in { (v + w) where w is VECTOR of V : w in M } by A4;

then v + w1 in v + M by RUSUB_4:def 8;

then (r * (v + w1)) + ((1 - r) * (v + w2)) in v + M by A2, A3, A6;

then v + ((r * w1) + ((1 - r) * w2)) in { (v + w) where w is VECTOR of V : w in M } by A7, RUSUB_4:def 8;

then ex w being VECTOR of V st

( v + ((r * w1) + ((1 - r) * w2)) = v + w & w in M ) ;

hence (r * w1) + ((1 - r) * w2) in M by RLVECT_1:8; :: thesis: verum

end;let w1, w2 be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for r being Real st 0 < r & r < 1 & w1 in M & w2 in M holds

(r * w1) + ((1 - r) * w2) in M

let r be Real; :: thesis: ( 0 < r & r < 1 & w1 in M & w2 in M implies (r * w1) + ((1 - r) * w2) in M )

assume that

A3: ( 0 < r & r < 1 ) and

A4: w1 in M and

A5: w2 in M ; :: thesis: (r * w1) + ((1 - r) * w2) in M

set x2 = v + w2;

v + w2 in { (v + w) where w is VECTOR of V : w in M } by A5;

then A6: v + w2 in v + M by RUSUB_4:def 8;

set x1 = v + w1;

A7: (r * (v + w1)) + ((1 - r) * (v + w2)) = ((r * v) + (r * w1)) + ((1 - r) * (v + w2)) by RLVECT_1:def 5

.= ((r * v) + (r * w1)) + (((1 - r) * v) + ((1 - r) * w2)) by RLVECT_1:def 5

.= (((r * v) + (r * w1)) + ((1 - r) * v)) + ((1 - r) * w2) by RLVECT_1:def 3

.= (((r * v) + ((1 - r) * v)) + (r * w1)) + ((1 - r) * w2) by RLVECT_1:def 3

.= (((r + (1 - r)) * v) + (r * w1)) + ((1 - r) * w2) by RLVECT_1:def 6

.= (v + (r * w1)) + ((1 - r) * w2) by RLVECT_1:def 8

.= v + ((r * w1) + ((1 - r) * w2)) by RLVECT_1:def 3 ;

v + w1 in { (v + w) where w is VECTOR of V : w in M } by A4;

then v + w1 in v + M by RUSUB_4:def 8;

then (r * (v + w1)) + ((1 - r) * (v + w2)) in v + M by A2, A3, A6;

then v + ((r * w1) + ((1 - r) * w2)) in { (v + w) where w is VECTOR of V : w in M } by A7, RUSUB_4:def 8;

then ex w being VECTOR of V st

( v + ((r * w1) + ((1 - r) * w2)) = v + w & w in M ) ;

hence (r * w1) + ((1 - r) * w2) in M by RLVECT_1:8; :: thesis: verum

proof

hence
( M is convex iff v + M is convex )
by A1; :: thesis: verum
assume A8:
M is convex
; :: thesis: v + M is convex

let w1, w2 be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for r being Real st 0 < r & r < 1 & w1 in v + M & w2 in v + M holds

(r * w1) + ((1 - r) * w2) in v + M

let r be Real; :: thesis: ( 0 < r & r < 1 & w1 in v + M & w2 in v + M implies (r * w1) + ((1 - r) * w2) in v + M )

assume that

A9: ( 0 < r & r < 1 ) and

A10: w1 in v + M and

A11: w2 in v + M ; :: thesis: (r * w1) + ((1 - r) * w2) in v + M

w2 in { (v + w) where w is VECTOR of V : w in M } by A11, RUSUB_4:def 8;

then consider x2 being VECTOR of V such that

A12: w2 = v + x2 and

A13: x2 in M ;

w1 in { (v + w) where w is VECTOR of V : w in M } by A10, RUSUB_4:def 8;

then consider x1 being VECTOR of V such that

A14: w1 = v + x1 and

A15: x1 in M ;

A16: (r * w1) + ((1 - r) * w2) = ((r * v) + (r * x1)) + ((1 - r) * (v + x2)) by A14, A12, RLVECT_1:def 5

.= ((r * v) + (r * x1)) + (((1 - r) * v) + ((1 - r) * x2)) by RLVECT_1:def 5

.= (((r * v) + (r * x1)) + ((1 - r) * v)) + ((1 - r) * x2) by RLVECT_1:def 3

.= (((r * v) + ((1 - r) * v)) + (r * x1)) + ((1 - r) * x2) by RLVECT_1:def 3

.= (((r + (1 - r)) * v) + (r * x1)) + ((1 - r) * x2) by RLVECT_1:def 6

.= (v + (r * x1)) + ((1 - r) * x2) by RLVECT_1:def 8

.= v + ((r * x1) + ((1 - r) * x2)) by RLVECT_1:def 3 ;

(r * x1) + ((1 - r) * x2) in M by A8, A9, A15, A13;

then (r * w1) + ((1 - r) * w2) in { (v + w) where w is VECTOR of V : w in M } by A16;

hence (r * w1) + ((1 - r) * w2) in v + M by RUSUB_4:def 8; :: thesis: verum

end;let w1, w2 be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for r being Real st 0 < r & r < 1 & w1 in v + M & w2 in v + M holds

(r * w1) + ((1 - r) * w2) in v + M

let r be Real; :: thesis: ( 0 < r & r < 1 & w1 in v + M & w2 in v + M implies (r * w1) + ((1 - r) * w2) in v + M )

assume that

A9: ( 0 < r & r < 1 ) and

A10: w1 in v + M and

A11: w2 in v + M ; :: thesis: (r * w1) + ((1 - r) * w2) in v + M

w2 in { (v + w) where w is VECTOR of V : w in M } by A11, RUSUB_4:def 8;

then consider x2 being VECTOR of V such that

A12: w2 = v + x2 and

A13: x2 in M ;

w1 in { (v + w) where w is VECTOR of V : w in M } by A10, RUSUB_4:def 8;

then consider x1 being VECTOR of V such that

A14: w1 = v + x1 and

A15: x1 in M ;

A16: (r * w1) + ((1 - r) * w2) = ((r * v) + (r * x1)) + ((1 - r) * (v + x2)) by A14, A12, RLVECT_1:def 5

.= ((r * v) + (r * x1)) + (((1 - r) * v) + ((1 - r) * x2)) by RLVECT_1:def 5

.= (((r * v) + (r * x1)) + ((1 - r) * v)) + ((1 - r) * x2) by RLVECT_1:def 3

.= (((r * v) + ((1 - r) * v)) + (r * x1)) + ((1 - r) * x2) by RLVECT_1:def 3

.= (((r + (1 - r)) * v) + (r * x1)) + ((1 - r) * x2) by RLVECT_1:def 6

.= (v + (r * x1)) + ((1 - r) * x2) by RLVECT_1:def 8

.= v + ((r * x1) + ((1 - r) * x2)) by RLVECT_1:def 3 ;

(r * x1) + ((1 - r) * x2) in M by A8, A9, A15, A13;

then (r * w1) + ((1 - r) * w2) in { (v + w) where w is VECTOR of V : w in M } by A16;

hence (r * w1) + ((1 - r) * w2) in v + M by RUSUB_4:def 8; :: thesis: verum