let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for M being Subset of V

for r being Real st M is convex holds

r * M is convex

let M be Subset of V; :: thesis: for r being Real st M is convex holds

r * M is convex

let r be Real; :: thesis: ( M is convex implies r * M is convex )

assume A1: M is convex ; :: thesis: r * M is convex

for u, v being VECTOR of V

for p being Real st 0 < p & p < 1 & u in r * M & v in r * M holds

(p * u) + ((1 - p) * v) in r * M

for r being Real st M is convex holds

r * M is convex

let M be Subset of V; :: thesis: for r being Real st M is convex holds

r * M is convex

let r be Real; :: thesis: ( M is convex implies r * M is convex )

assume A1: M is convex ; :: thesis: r * M is convex

for u, v being VECTOR of V

for p being Real st 0 < p & p < 1 & u in r * M & v in r * M holds

(p * u) + ((1 - p) * v) in r * M

proof

hence
r * M is convex
; :: thesis: verum
let u, v be VECTOR of V; :: thesis: for p being Real st 0 < p & p < 1 & u in r * M & v in r * M holds

(p * u) + ((1 - p) * v) in r * M

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

assume that

A2: ( 0 < p & p < 1 ) and

A3: u in r * M and

A4: v in r * M ; :: thesis: (p * u) + ((1 - p) * v) in r * M

consider v9 being Element of V such that

A5: v = r * v9 and

A6: v9 in M by A4;

consider u9 being Element of V such that

A7: u = r * u9 and

A8: u9 in M by A3;

A9: (p * u) + ((1 - p) * v) = ((r * p) * u9) + ((1 - p) * (r * v9)) by A7, A5, RLVECT_1:def 7

.= ((r * p) * u9) + ((r * (1 - p)) * v9) by RLVECT_1:def 7

.= (r * (p * u9)) + ((r * (1 - p)) * v9) by RLVECT_1:def 7

.= (r * (p * u9)) + (r * ((1 - p) * v9)) by RLVECT_1:def 7

.= r * ((p * u9) + ((1 - p) * v9)) by RLVECT_1:def 5 ;

(p * u9) + ((1 - p) * v9) in M by A1, A2, A8, A6;

hence (p * u) + ((1 - p) * v) in r * M by A9; :: thesis: verum

end;(p * u) + ((1 - p) * v) in r * M

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

assume that

A2: ( 0 < p & p < 1 ) and

A3: u in r * M and

A4: v in r * M ; :: thesis: (p * u) + ((1 - p) * v) in r * M

consider v9 being Element of V such that

A5: v = r * v9 and

A6: v9 in M by A4;

consider u9 being Element of V such that

A7: u = r * u9 and

A8: u9 in M by A3;

A9: (p * u) + ((1 - p) * v) = ((r * p) * u9) + ((1 - p) * (r * v9)) by A7, A5, RLVECT_1:def 7

.= ((r * p) * u9) + ((r * (1 - p)) * v9) by RLVECT_1:def 7

.= (r * (p * u9)) + ((r * (1 - p)) * v9) by RLVECT_1:def 7

.= (r * (p * u9)) + (r * ((1 - p) * v9)) by RLVECT_1:def 7

.= r * ((p * u9) + ((1 - p) * v9)) by RLVECT_1:def 5 ;

(p * u9) + ((1 - p) * v9) in M by A1, A2, A8, A6;

hence (p * u) + ((1 - p) * v) in r * M by A9; :: thesis: verum