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
proof
let u1, u2 be VECTOR of R; :: according to CONVEX1:def 2 :: thesis: for b1 being object holds
( b1 <= 0 or 1 <= b1 or not u1 in {v} or not u2 in {v} or (b1 * u1) + ((1 - b1) * 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;
then conv {v} c= {v} by CONVEX1:30;
hence conv {v} = {v} by ZFMISC_1:33; :: thesis: verum