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 )

proof

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;

( M is convex implies v + M is convex )

proof

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;

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