let V be ComplexLinearSpace; :: 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 CONVEX4:def 23 :: thesis: for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) & w1 in v + M & w2 in v + M holds
(z * w1) + ((1r - z) * w2) in v + M
let z be Complex; :: thesis: ( ex r being Real st
( z = r & 0 < r & r < 1 ) & w1 in v + M & w2 in v + M implies (z * w1) + ((1r - z) * w2) in v + M )
assume that
A3: ex r being Real st
( z = r & 0 < r & r < 1 ) and
A4: ( w1 in v + M & w2 in v + M ) ; :: thesis: (z * w1) + ((1r - z) * w2) in v + M
consider x1 being VECTOR of V such that
A5: ( w1 = v + x1 & x1 in M ) by A4;
consider x2 being VECTOR of V such that
A6: ( w2 = v + x2 & x2 in M ) by A4;
A7: (z * x1) + ((1r - z) * x2) in M by A2, A3, A5, A6, Def202;
(z * w1) + ((1r - z) * w2) = ((z * v) + (z * x1)) + ((1r - z) * (v + x2)) by A5, A6, CLVECT_1:def 2
.= ((z * v) + (z * x1)) + (((1r - z) * v) + ((1r - z) * x2)) by CLVECT_1:def 2
.= (((z * v) + (z * x1)) + ((1r - z) * v)) + ((1r - z) * x2) by RLVECT_1:def 6
.= (((z * v) + ((1r - z) * v)) + (z * x1)) + ((1r - z) * x2) by RLVECT_1:def 6
.= (((z + (1r - z)) * v) + (z * x1)) + ((1r - z) * x2) by CLVECT_1:def 2
.= (v + (z * x1)) + ((1r - z) * x2) by CLVECT_1:def 2
.= v + ((z * x1) + ((1r - z) * x2)) by RLVECT_1:def 6 ;
hence (z * w1) + ((1r - z) * w2) in v + M by A7; :: 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 CONVEX4:def 23 :: thesis: for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) & w1 in M & w2 in M holds
(z * w1) + ((1r - z) * w2) in M
let z be Complex; :: thesis: ( ex r being Real st
( z = r & 0 < r & r < 1 ) & w1 in M & w2 in M implies (z * w1) + ((1r - z) * w2) in M )
assume that
A9: ex r being Real st
( z = r & 0 < r & r < 1 ) and
A10: ( w1 in M & w2 in M ) ; :: thesis: (z * w1) + ((1r - z) * w2) in M
set x1 = v + w1;
set x2 = v + w2;
A11: v + w1 in v + M by A10;
v + w2 in { (v + w) where w is VECTOR of V : w in M } by A10;
then A12: (z * (v + w1)) + ((1r - z) * (v + w2)) in v + M by A8, A9, A11, Def202;
(z * (v + w1)) + ((1r - z) * (v + w2)) = ((z * v) + (z * w1)) + ((1r - z) * (v + w2)) by CLVECT_1:def 2
.= ((z * v) + (z * w1)) + (((1r - z) * v) + ((1r - z) * w2)) by CLVECT_1:def 2
.= (((z * v) + (z * w1)) + ((1r - z) * v)) + ((1r - z) * w2) by RLVECT_1:def 6
.= (((z * v) + ((1r - z) * v)) + (z * w1)) + ((1r - z) * w2) by RLVECT_1:def 6
.= (((z + (1r - z)) * v) + (z * w1)) + ((1r - z) * w2) by CLVECT_1:def 2
.= (v + (z * w1)) + ((1r - z) * w2) by CLVECT_1:def 2
.= v + ((z * w1) + ((1r - z) * w2)) by RLVECT_1:def 6 ;
then ex w being VECTOR of V st
( v + ((z * w1) + ((1r - z) * w2)) = v + w & w in M ) by A12;
hence (z * w1) + ((1r - z) * w2) in M by RLVECT_1:21; :: thesis: verum

end;

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