let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for v being Element of R holds conv {v} = {v}

let v be Element of R; :: thesis: conv {v} = {v}

{v} is convex

hence conv {v} = {v} by ZFMISC_1:33; :: thesis: verum

let v be Element of R; :: thesis: conv {v} = {v}

{v} is convex

proof

then
conv {v} c= {v}
by CONVEX1:30;
let u1, u2 be VECTOR of R; :: according to CONVEX1:def 2 :: thesis: for b_{1} being object holds

( b_{1} <= 0 or 1 <= b_{1} or not u1 in {v} or not u2 in {v} or (b_{1} * u1) + ((1 - b_{1}) * u2) in {v} )

let r be Real; :: thesis: ( r <= 0 or 1 <= r or not u1 in {v} or not u2 in {v} or (r * u1) + ((1 - r) * u2) in {v} )

assume that

0 < r and

r < 1 ; :: thesis: ( not u1 in {v} or not u2 in {v} or (r * u1) + ((1 - r) * u2) in {v} )

assume that

A1: u1 in {v} and

A2: u2 in {v} ; :: thesis: (r * u1) + ((1 - r) * u2) in {v}

( u1 = v & u2 = v ) by A1, A2, TARSKI:def 1;

then (r * u1) + ((1 - r) * u2) = (r + (1 - r)) * u1 by RLVECT_1:def 6

.= u1 by RLVECT_1:def 8 ;

hence (r * u1) + ((1 - r) * u2) in {v} by A1; :: thesis: verum

end;( b

let r be Real; :: thesis: ( r <= 0 or 1 <= r or not u1 in {v} or not u2 in {v} or (r * u1) + ((1 - r) * u2) in {v} )

assume that

0 < r and

r < 1 ; :: thesis: ( not u1 in {v} or not u2 in {v} or (r * u1) + ((1 - r) * u2) in {v} )

assume that

A1: u1 in {v} and

A2: u2 in {v} ; :: thesis: (r * u1) + ((1 - r) * u2) in {v}

( u1 = v & u2 = v ) by A1, A2, TARSKI:def 1;

then (r * u1) + ((1 - r) * u2) = (r + (1 - r)) * u1 by RLVECT_1:def 6

.= u1 by RLVECT_1:def 8 ;

hence (r * u1) + ((1 - r) * u2) in {v} by A1; :: thesis: verum

hence conv {v} = {v} by ZFMISC_1:33; :: thesis: verum