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: ( M is convex implies v + M is convex )

proof

assume A2: 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
A3: ( 0 < r & r < 1 ) and
A4: ( w1 in v + M & w2 in v + M ) ; :: thesis: (r * w1) + ((1 - r) * w2) in v + M
w1 in { (v + w) where w is VECTOR of V : w in M } by A4, RUSUB_4:def 9;
then consider x1 being VECTOR of V such that
A5: ( w1 = v + x1 & x1 in M ) ;
w2 in { (v + w) where w is VECTOR of V : w in M } by A4, RUSUB_4:def 9;
then consider x2 being VECTOR of V such that
A6: ( w2 = v + x2 & x2 in M ) ;
A7: (r * x1) + ((1 - r) * x2) in M by A2, A3, A5, A6, Def2;
(r * w1) + ((1 - r) * w2) = ((r * v) + (r * x1)) + ((1 - r) * (v + x2)) by A5, A6, RLVECT_1:def 9
.= ((r * v) + (r * x1)) + (((1 - r) * v) + ((1 - r) * x2)) by RLVECT_1:def 9
.= (((r * v) + (r * x1)) + ((1 - r) * v)) + ((1 - r) * x2) by RLVECT_1:def 6
.= (((r * v) + ((1 - r) * v)) + (r * x1)) + ((1 - r) * x2) by RLVECT_1:def 6
.= (((r + (1 - r)) * v) + (r * x1)) + ((1 - r) * x2) by RLVECT_1:def 9
.= (v + (r * x1)) + ((1 - r) * x2) by RLVECT_1:def 9
.= v + ((r * x1) + ((1 - r) * x2)) by RLVECT_1:def 6 ;
then (r * w1) + ((1 - r) * w2) in { (v + w) where w is VECTOR of V : w in M } by A7;
hence (r * w1) + ((1 - r) * w2) in v + M by RUSUB_4:def 9; :: thesis: verum

end;

( v + M is convex implies M is convex )

proof

assume A8: 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
A9: ( 0 < r & r < 1 ) and
A10: ( w1 in M & w2 in M ) ; :: thesis: (r * w1) + ((1 - r) * w2) in M
set x1 = v + w1;
set x2 = v + w2;
v + w1 in { (v + w) where w is VECTOR of V : w in M } by A10;
then A11: v + w1 in v + M by RUSUB_4:def 9;
v + w2 in { (v + w) where w is VECTOR of V : w in M } by A10;
then v + w2 in v + M by RUSUB_4:def 9;
then A12: (r * (v + w1)) + ((1 - r) * (v + w2)) in v + M by A8, A9, A11, Def2;
(r * (v + w1)) + ((1 - r) * (v + w2)) = ((r * v) + (r * w1)) + ((1 - r) * (v + w2)) by RLVECT_1:def 9
.= ((r * v) + (r * w1)) + (((1 - r) * v) + ((1 - r) * w2)) by RLVECT_1:def 9
.= (((r * v) + (r * w1)) + ((1 - r) * v)) + ((1 - r) * w2) by RLVECT_1:def 6
.= (((r * v) + ((1 - r) * v)) + (r * w1)) + ((1 - r) * w2) by RLVECT_1:def 6
.= (((r + (1 - r)) * v) + (r * w1)) + ((1 - r) * w2) by RLVECT_1:def 9
.= (v + (r * w1)) + ((1 - r) * w2) by RLVECT_1:def 9
.= v + ((r * w1) + ((1 - r) * w2)) by RLVECT_1:def 6 ;
then v + ((r * w1) + ((1 - r) * w2)) in { (v + w) where w is VECTOR of V : w in M } by A12, RUSUB_4:def 9;
then consider w being VECTOR of V such that
A13: ( v + ((r * w1) + ((1 - r) * w2)) = v + w & w in M ) ;
thus (r * w1) + ((1 - r) * w2) in M by A13, RLVECT_1:21; :: thesis: verum

end;

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