convex1.miz



    begin

    definition

      let V be non empty RLSStruct, M be Subset of V, r be Real;

      :: CONVEX1:def1

      func r * M -> Subset of V equals { (r * v) where v be Element of V : v in M };

      coherence

      proof

        deffunc F( Element of V) = (r * $1);

        defpred P[ set] means $1 in M;

        { F(v) where v be Element of V : P[v] } is Subset of V from DOMAIN_1:sch 8;

        hence thesis;

      end;

    end

    definition

      let V be non empty RLSStruct, M be Subset of V;

      :: CONVEX1:def2

      attr M is convex means

      : Def2: for u,v be VECTOR of V, r be Real st 0 < r & r < 1 & u in M & v in M holds ((r * u) + ((1 - r) * v)) in M;

    end

    theorem :: CONVEX1:1

    for V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M be Subset of V, r be Real st M is convex holds (r * M) is convex

    proof

      let V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct;

      let M be Subset of V;

      let r be Real;

      assume

       A1: M is convex;

      for u,v be VECTOR of V, p be Real st 0 < p & p < 1 & u in (r * M) & v in (r * M) holds ((p * u) + ((1 - p) * v)) in (r * M)

      proof

        let u,v be VECTOR of V;

        let p be Real;

        assume that

         A2: 0 < p & p < 1 and

         A3: u in (r * M) and

         A4: v in (r * M);

        consider v9 be Element of V such that

         A5: v = (r * v9) and

         A6: v9 in M by A4;

        consider u9 be 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 thesis by A9;

      end;

      hence thesis;

    end;

    theorem :: CONVEX1:2

    for V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M,N be Subset of V st M is convex & N is convex holds (M + N) is convex

    proof

      let V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct;

      let M,N be Subset of V;

      assume

       A1: M is convex & N is convex;

      for u,v be VECTOR of V, r be Real st 0 < r & r < 1 & u in (M + N) & v in (M + N) holds ((r * u) + ((1 - r) * v)) in (M + N)

      proof

        let u,v be VECTOR of V;

        let r be Real;

        assume that

         A2: 0 < r & r < 1 and

         A3: u in (M + N) and

         A4: v in (M + N);

        v in { (x + y) where x,y be Element of V : x in M & y in N } by A4, RUSUB_4:def 9;

        then

        consider x2,y2 be Element of V such that

         A5: v = (x2 + y2) and

         A6: x2 in M & y2 in N;

        u in { (x + y) where x,y be Element of V : x in M & y in N } by A3, RUSUB_4:def 9;

        then

        consider x1,y1 be Element of V such that

         A7: u = (x1 + y1) and

         A8: x1 in M & y1 in N;

        

         A9: ((r * u) + ((1 - r) * v)) = (((r * x1) + (r * y1)) + ((1 - r) * (x2 + y2))) by A7, A5, RLVECT_1:def 5

        .= (((r * x1) + (r * y1)) + (((1 - r) * x2) + ((1 - r) * y2))) by RLVECT_1:def 5

        .= ((((r * x1) + (r * y1)) + ((1 - r) * x2)) + ((1 - r) * y2)) by RLVECT_1:def 3

        .= ((((r * x1) + ((1 - r) * x2)) + (r * y1)) + ((1 - r) * y2)) by RLVECT_1:def 3

        .= (((r * x1) + ((1 - r) * x2)) + ((r * y1) + ((1 - r) * y2))) by RLVECT_1:def 3;

        ((r * x1) + ((1 - r) * x2)) in M & ((r * y1) + ((1 - r) * y2)) in N by A1, A2, A8, A6;

        then ((r * u) + ((1 - r) * v)) in { (x + y) where x,y be Element of V : x in M & y in N } by A9;

        hence thesis by RUSUB_4:def 9;

      end;

      hence thesis;

    end;

    theorem :: CONVEX1:3

    for V be RealLinearSpace, M,N be Subset of V st M is convex & N is convex holds (M - N) is convex

    proof

      let V be RealLinearSpace;

      let M,N be Subset of V;

      assume

       A1: M is convex & N is convex;

      for u,v be VECTOR of V, r be Real st 0 < r & r < 1 & u in (M - N) & v in (M - N) holds ((r * u) + ((1 - r) * v)) in (M - N)

      proof

        let u,v be VECTOR of V;

        let r be Real;

        assume that

         A2: 0 < r & r < 1 and

         A3: u in (M - N) and

         A4: v in (M - N);

        v in { (x - y) where x,y be Element of V : x in M & y in N } by A4, RUSUB_5:def 2;

        then

        consider x2,y2 be Element of V such that

         A5: v = (x2 - y2) and

         A6: x2 in M & y2 in N;

        u in { (x - y) where x,y be Element of V : x in M & y in N } by A3, RUSUB_5:def 2;

        then

        consider x1,y1 be Element of V such that

         A7: u = (x1 - y1) and

         A8: x1 in M & y1 in N;

        

         A9: ((r * u) + ((1 - r) * v)) = (((r * x1) - (r * y1)) + ((1 - r) * (x2 - y2))) by A7, A5, RLVECT_1: 34

        .= (((r * x1) - (r * y1)) + (((1 - r) * x2) - ((1 - r) * y2))) by RLVECT_1: 34

        .= ((((r * x1) - (r * y1)) + ((1 - r) * x2)) - ((1 - r) * y2)) by RLVECT_1:def 3

        .= (((r * x1) - ((r * y1) - ((1 - r) * x2))) - ((1 - r) * y2)) by RLVECT_1: 29

        .= (((r * x1) + (((1 - r) * x2) + ( - (r * y1)))) - ((1 - r) * y2)) by RLVECT_1: 33

        .= ((((r * x1) + ((1 - r) * x2)) + ( - (r * y1))) - ((1 - r) * y2)) by RLVECT_1:def 3

        .= (((r * x1) + ((1 - r) * x2)) + (( - (r * y1)) - ((1 - r) * y2))) by RLVECT_1:def 3

        .= (((r * x1) + ((1 - r) * x2)) - ((r * y1) + ((1 - r) * y2))) by RLVECT_1: 30;

        ((r * x1) + ((1 - r) * x2)) in M & ((r * y1) + ((1 - r) * y2)) in N by A1, A2, A8, A6;

        then ((r * u) + ((1 - r) * v)) in { (x - y) where x,y be Element of V : x in M & y in N } by A9;

        hence thesis by RUSUB_5:def 2;

      end;

      hence thesis;

    end;

    theorem :: CONVEX1:4

    

     Th4: for V be non empty RLSStruct, M be Subset of V holds M is convex iff for r be Real st 0 < r & r < 1 holds ((r * M) + ((1 - r) * M)) c= M

    proof

      let V be non empty RLSStruct;

      let M be Subset of V;

      thus M is convex implies for r be Real st 0 < r & r < 1 holds ((r * M) + ((1 - r) * M)) c= M

      proof

        assume

         A1: M is convex;

        let r be Real;

        assume

         A2: 0 < r & r < 1;

        for x be Element of V st x in ((r * M) + ((1 - r) * M)) holds x in M

        proof

          let x be Element of V;

          assume x in ((r * M) + ((1 - r) * M));

          then x in { (u + v) where u,v be Element of V : u in (r * M) & v in ((1 - r) * M) } by RUSUB_4:def 9;

          then

          consider u,v be Element of V such that

           A3: x = (u + v) and

           A4: u in (r * M) & v in ((1 - r) * M);

          (ex w1 be Element of V st u = (r * w1) & w1 in M) & ex w2 be Element of V st v = ((1 - r) * w2) & w2 in M by A4;

          hence thesis by A1, A2, A3;

        end;

        hence thesis;

      end;

      assume

       A5: for r be Real st 0 < r & r < 1 holds ((r * M) + ((1 - r) * M)) c= M;

      let u,v be VECTOR of V;

      let r be Real;

      assume 0 < r & r < 1;

      then

       A6: ((r * M) + ((1 - r) * M)) c= M by A5;

      assume u in M & v in M;

      then (r * u) in (r * M) & ((1 - r) * v) in { ((1 - r) * w) where w be Element of V : w in M };

      then ((r * u) + ((1 - r) * v)) in { (p + q) where p,q be Element of V : p in (r * M) & q in ((1 - r) * M) };

      then ((r * u) + ((1 - r) * v)) in ((r * M) + ((1 - r) * M)) by RUSUB_4:def 9;

      hence thesis by A6;

    end;

    theorem :: CONVEX1:5

    for V be Abelian non empty RLSStruct, M be Subset of V st M is convex holds for r be Real st 0 < r & r < 1 holds (((1 - r) * M) + (r * M)) c= M

    proof

      let V be Abelian non empty RLSStruct;

      let M be Subset of V;

      assume

       A1: M is convex;

      let r be Real;

      assume

       A2: 0 < r & r < 1;

      for x be Element of V st x in (((1 - r) * M) + (r * M)) holds x in M

      proof

        let x be Element of V;

        assume x in (((1 - r) * M) + (r * M));

        then x in { (u + v) where u,v be Element of V : u in ((1 - r) * M) & v in (r * M) } by RUSUB_4:def 9;

        then

        consider u,v be Element of V such that

         A3: x = (u + v) and

         A4: u in ((1 - r) * M) & v in (r * M);

        (ex w1 be Element of V st u = ((1 - r) * w1) & w1 in M) & ex w2 be Element of V st v = (r * w2) & w2 in M by A4;

        hence thesis by A1, A2, A3;

      end;

      hence thesis;

    end;

    theorem :: CONVEX1:6

    for V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M,N be Subset of V st M is convex & N is convex holds for r be Real holds ((r * M) + ((1 - r) * N)) is convex

    proof

      let V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct;

      let M,N be Subset of V;

      assume that

       A1: M is convex and

       A2: N is convex;

      let r be Real;

      let u,v be VECTOR of V;

      let p be Real;

      assume that

       A3: 0 < p & p < 1 and

       A4: u in ((r * M) + ((1 - r) * N)) and

       A5: v in ((r * M) + ((1 - r) * N));

      

       A6: u in { (x1 + y1) where x1,y1 be VECTOR of V : x1 in (r * M) & y1 in ((1 - r) * N) } by A4, RUSUB_4:def 9;

      v in { (x2 + y2) where x2,y2 be VECTOR of V : x2 in (r * M) & y2 in ((1 - r) * N) } by A5, RUSUB_4:def 9;

      then

      consider x2,y2 be VECTOR of V such that

       A7: v = (x2 + y2) and

       A8: x2 in (r * M) and

       A9: y2 in ((1 - r) * N);

      consider x1,y1 be VECTOR of V such that

       A10: u = (x1 + y1) and

       A11: x1 in (r * M) and

       A12: y1 in ((1 - r) * N) by A6;

      consider mx2 be VECTOR of V such that

       A13: x2 = (r * mx2) and

       A14: mx2 in M by A8;

      consider mx1 be VECTOR of V such that

       A15: x1 = (r * mx1) and

       A16: mx1 in M by A11;

      

       A17: ((p * x1) + ((1 - p) * x2)) = (((p * r) * mx1) + ((1 - p) * (r * mx2))) by A15, A13, RLVECT_1:def 7

      .= (((p * r) * mx1) + (((1 - p) * r) * mx2)) by RLVECT_1:def 7

      .= ((r * (p * mx1)) + (((1 - p) * r) * mx2)) by RLVECT_1:def 7

      .= ((r * (p * mx1)) + (r * ((1 - p) * mx2))) by RLVECT_1:def 7

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

      consider ny2 be VECTOR of V such that

       A18: y2 = ((1 - r) * ny2) and

       A19: ny2 in N by A9;

      consider ny1 be VECTOR of V such that

       A20: y1 = ((1 - r) * ny1) and

       A21: ny1 in N by A12;

      

       A22: ((p * y1) + ((1 - p) * y2)) = (((p * (1 - r)) * ny1) + ((1 - p) * ((1 - r) * ny2))) by A20, A18, RLVECT_1:def 7

      .= (((p * (1 - r)) * ny1) + (((1 - p) * (1 - r)) * ny2)) by RLVECT_1:def 7

      .= (((1 - r) * (p * ny1)) + (((1 - p) * (1 - r)) * ny2)) by RLVECT_1:def 7

      .= (((1 - r) * (p * ny1)) + ((1 - r) * ((1 - p) * ny2))) by RLVECT_1:def 7

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

      ((p * ny1) + ((1 - p) * ny2)) in N by A2, A3, A21, A19;

      then

       A23: ((p * y1) + ((1 - p) * y2)) in ((1 - r) * N) by A22;

      ((p * mx1) + ((1 - p) * mx2)) in M by A1, A3, A16, A14;

      then

       A24: ((p * x1) + ((1 - p) * x2)) in { (r * w) where w be VECTOR of V : w in M } by A17;

      ((p * u) + ((1 - p) * v)) = (((p * x1) + (p * y1)) + ((1 - p) * (x2 + y2))) by A10, A7, RLVECT_1:def 5

      .= (((p * x1) + (p * y1)) + (((1 - p) * x2) + ((1 - p) * y2))) by RLVECT_1:def 5

      .= ((((p * x1) + (p * y1)) + ((1 - p) * x2)) + ((1 - p) * y2)) by RLVECT_1:def 3

      .= ((((p * x1) + ((1 - p) * x2)) + (p * y1)) + ((1 - p) * y2)) by RLVECT_1:def 3

      .= (((p * x1) + ((1 - p) * x2)) + ((p * y1) + ((1 - p) * y2))) by RLVECT_1:def 3;

      then ((p * u) + ((1 - p) * v)) in { (w1 + w2) where w1,w2 be VECTOR of V : w1 in (r * M) & w2 in ((1 - r) * N) } by A24, A23;

      hence thesis by RUSUB_4:def 9;

    end;

    

     Lm1: for V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M be Subset of V holds (1 * M) = M

    proof

      let V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct;

      let M be Subset of V;

      for v be Element of V st v in M holds v in (1 * M)

      proof

        let v be Element of V;

        

         A1: v = (1 * v) by RLVECT_1:def 8;

        assume v in M;

        hence thesis by A1;

      end;

      then

       A2: M c= (1 * M);

      for v be Element of V st v in (1 * M) holds v in M

      proof

        let v be Element of V;

        assume v in (1 * M);

        then ex x be Element of V st v = (1 * x) & x in M;

        hence thesis by RLVECT_1:def 8;

      end;

      then (1 * M) c= M;

      hence thesis by A2;

    end;

    

     Lm2: for V be RealLinearSpace, M be non empty Subset of V holds ( 0 * M) = {( 0. V)}

    proof

      let V be RealLinearSpace;

      let M be non empty Subset of V;

      for v be Element of V st v in {( 0. V)} holds v in ( 0 * M)

      proof

        let v be Element of V;

        consider x be object such that

         A1: x in M by XBOOLE_0:def 1;

        reconsider x as Element of V by A1;

        assume v in {( 0. V)};

        then v = ( 0. V) by TARSKI:def 1;

        then v = ( 0 * x) by RLVECT_1: 10;

        hence thesis by A1;

      end;

      then

       A2: {( 0. V)} c= ( 0 * M);

      for v be Element of V st v in ( 0 * M) holds v in {( 0. V)}

      proof

        let v be Element of V;

        assume v in ( 0 * M);

        then ex x be Element of V st v = ( 0 * x) & x in M;

        then v = ( 0. V) by RLVECT_1: 10;

        hence thesis by TARSKI:def 1;

      end;

      then ( 0 * M) c= {( 0. V)};

      hence thesis by A2;

    end;

    

     Lm3: for V be add-associative non empty addLoopStr, M1,M2,M3 be Subset of V holds ((M1 + M2) + M3) = (M1 + (M2 + M3))

    proof

      let V be add-associative non empty addLoopStr;

      let M1,M2,M3 be Subset of V;

      for x be Element of V st x in (M1 + (M2 + M3)) holds x in ((M1 + M2) + M3)

      proof

        let x be Element of V;

        assume x in (M1 + (M2 + M3));

        then x in { (u + v) where u,v be Element of V : u in M1 & v in (M2 + M3) } by RUSUB_4:def 9;

        then

        consider x1,x9 be Element of V such that

         A1: x = (x1 + x9) and

         A2: x1 in M1 and

         A3: x9 in (M2 + M3);

        x9 in { (u + v) where u,v be Element of V : u in M2 & v in M3 } by A3, RUSUB_4:def 9;

        then

        consider x2,x3 be Element of V such that

         A4: x9 = (x2 + x3) and

         A5: x2 in M2 and

         A6: x3 in M3;

        (x1 + x2) in { (u + v) where u,v be Element of V : u in M1 & v in M2 } by A2, A5;

        then

         A7: (x1 + x2) in (M1 + M2) by RUSUB_4:def 9;

        x = ((x1 + x2) + x3) by A1, A4, RLVECT_1:def 3;

        then x in { (u + v) where u,v be Element of V : u in (M1 + M2) & v in M3 } by A6, A7;

        hence thesis by RUSUB_4:def 9;

      end;

      then

       A8: (M1 + (M2 + M3)) c= ((M1 + M2) + M3);

      for x be Element of V st x in ((M1 + M2) + M3) holds x in (M1 + (M2 + M3))

      proof

        let x be Element of V;

        assume x in ((M1 + M2) + M3);

        then x in { (u + v) where u,v be Element of V : u in (M1 + M2) & v in M3 } by RUSUB_4:def 9;

        then

        consider x9,x3 be Element of V such that

         A9: x = (x9 + x3) and

         A10: x9 in (M1 + M2) and

         A11: x3 in M3;

        x9 in { (u + v) where u,v be Element of V : u in M1 & v in M2 } by A10, RUSUB_4:def 9;

        then

        consider x1,x2 be Element of V such that

         A12: x9 = (x1 + x2) and

         A13: x1 in M1 and

         A14: x2 in M2;

        (x2 + x3) in { (u + v) where u,v be Element of V : u in M2 & v in M3 } by A11, A14;

        then

         A15: (x2 + x3) in (M2 + M3) by RUSUB_4:def 9;

        x = (x1 + (x2 + x3)) by A9, A12, RLVECT_1:def 3;

        then x in { (u + v) where u,v be Element of V : u in M1 & v in (M2 + M3) } by A13, A15;

        hence thesis by RUSUB_4:def 9;

      end;

      then ((M1 + M2) + M3) c= (M1 + (M2 + M3));

      hence thesis by A8;

    end;

    

     Lm4: for V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M be Subset of V, r1,r2 be Real holds (r1 * (r2 * M)) = ((r1 * r2) * M)

    proof

      let V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct;

      let M be Subset of V;

      let r1,r2 be Real;

      for x be VECTOR of V st x in (r1 * (r2 * M)) holds x in ((r1 * r2) * M)

      proof

        let x be VECTOR of V;

        assume x in (r1 * (r2 * M));

        then

        consider w1 be VECTOR of V such that

         A1: x = (r1 * w1) and

         A2: w1 in (r2 * M);

        consider w2 be VECTOR of V such that

         A3: w1 = (r2 * w2) and

         A4: w2 in M by A2;

        x = ((r1 * r2) * w2) by A1, A3, RLVECT_1:def 7;

        hence thesis by A4;

      end;

      then

       A5: (r1 * (r2 * M)) c= ((r1 * r2) * M);

      for x be VECTOR of V st x in ((r1 * r2) * M) holds x in (r1 * (r2 * M))

      proof

        let x be VECTOR of V;

        assume x in ((r1 * r2) * M);

        then

        consider w1 be VECTOR of V such that

         A6: x = ((r1 * r2) * w1) & w1 in M;

        x = (r1 * (r2 * w1)) & (r2 * w1) in (r2 * M) by A6, RLVECT_1:def 7;

        hence thesis;

      end;

      then ((r1 * r2) * M) c= (r1 * (r2 * M));

      hence thesis by A5;

    end;

    

     Lm5: for V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M1,M2 be Subset of V, r be Real holds (r * (M1 + M2)) = ((r * M1) + (r * M2))

    proof

      let V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct;

      let M1,M2 be Subset of V;

      let r be Real;

      for x be VECTOR of V st x in ((r * M1) + (r * M2)) holds x in (r * (M1 + M2))

      proof

        let x be VECTOR of V;

        assume x in ((r * M1) + (r * M2));

        then x in { (u + v) where u,v be VECTOR of V : u in (r * M1) & v in (r * M2) } by RUSUB_4:def 9;

        then

        consider w1,w2 be VECTOR of V such that

         A1: x = (w1 + w2) and

         A2: w1 in (r * M1) and

         A3: w2 in (r * M2);

        consider v2 be VECTOR of V such that

         A4: w2 = (r * v2) and

         A5: v2 in M2 by A3;

        consider v1 be VECTOR of V such that

         A6: w1 = (r * v1) and

         A7: v1 in M1 by A2;

        (v1 + v2) in { (u + v) where u,v be VECTOR of V : u in M1 & v in M2 } by A7, A5;

        then

         A8: (v1 + v2) in (M1 + M2) by RUSUB_4:def 9;

        x = (r * (v1 + v2)) by A1, A6, A4, RLVECT_1:def 5;

        hence thesis by A8;

      end;

      then

       A9: ((r * M1) + (r * M2)) c= (r * (M1 + M2));

      for x be VECTOR of V st x in (r * (M1 + M2)) holds x in ((r * M1) + (r * M2))

      proof

        let x be VECTOR of V;

        assume x in (r * (M1 + M2));

        then

        consider w9 be VECTOR of V such that

         A10: x = (r * w9) and

         A11: w9 in (M1 + M2);

        w9 in { (u + v) where u,v be VECTOR of V : u in M1 & v in M2 } by A11, RUSUB_4:def 9;

        then

        consider w1,w2 be VECTOR of V such that

         A12: w9 = (w1 + w2) and

         A13: w1 in M1 & w2 in M2;

        

         A14: (r * w1) in (r * M1) & (r * w2) in { (r * w) where w be VECTOR of V : w in M2 } by A13;

        x = ((r * w1) + (r * w2)) by A10, A12, RLVECT_1:def 5;

        then x in { (u + v) where u,v be VECTOR of V : u in (r * M1) & v in (r * M2) } by A14;

        hence thesis by RUSUB_4:def 9;

      end;

      then (r * (M1 + M2)) c= ((r * M1) + (r * M2));

      hence thesis by A9;

    end;

    theorem :: CONVEX1:7

    for V be RealLinearSpace, M be Subset of V, v be VECTOR of V holds M is convex iff (v + M) is convex

    proof

      let V be RealLinearSpace;

      let M be Subset of V;

      let v be VECTOR of V;

      

       A1: (v + M) is convex implies M is convex

      proof

        assume

         A2: (v + M) is convex;

        let w1,w2 be VECTOR of V;

        let r be Real;

        assume that

         A3: 0 < r & r < 1 and

         A4: w1 in M and

         A5: w2 in M;

        set x2 = (v + w2);

        x2 in { (v + w) where w be VECTOR of V : w in M } by A5;

        then

         A6: x2 in (v + M) by RUSUB_4:def 8;

        set x1 = (v + w1);

        

         A7: ((r * x1) + ((1 - r) * x2)) = (((r * v) + (r * w1)) + ((1 - r) * (v + w2))) by RLVECT_1:def 5

        .= (((r * v) + (r * w1)) + (((1 - r) * v) + ((1 - r) * w2))) by RLVECT_1:def 5

        .= ((((r * v) + (r * w1)) + ((1 - r) * v)) + ((1 - r) * w2)) by RLVECT_1:def 3

        .= ((((r * v) + ((1 - r) * v)) + (r * w1)) + ((1 - r) * w2)) by RLVECT_1:def 3

        .= ((((r + (1 - r)) * v) + (r * w1)) + ((1 - r) * w2)) by RLVECT_1:def 6

        .= ((v + (r * w1)) + ((1 - r) * w2)) by RLVECT_1:def 8

        .= (v + ((r * w1) + ((1 - r) * w2))) by RLVECT_1:def 3;

        x1 in { (v + w) where w be VECTOR of V : w in M } by A4;

        then x1 in (v + M) by RUSUB_4:def 8;

        then ((r * x1) + ((1 - r) * x2)) in (v + M) by A2, A3, A6;

        then (v + ((r * w1) + ((1 - r) * w2))) in { (v + w) where w be VECTOR of V : w in M } by A7, RUSUB_4:def 8;

        then ex w be VECTOR of V st (v + ((r * w1) + ((1 - r) * w2))) = (v + w) & w in M;

        hence thesis by RLVECT_1: 8;

      end;

      M is convex implies (v + M) is convex

      proof

        assume

         A8: M is convex;

        let w1,w2 be VECTOR of V;

        let r be Real;

        assume that

         A9: 0 < r & r < 1 and

         A10: w1 in (v + M) and

         A11: w2 in (v + M);

        w2 in { (v + w) where w be VECTOR of V : w in M } by A11, RUSUB_4:def 8;

        then

        consider x2 be VECTOR of V such that

         A12: w2 = (v + x2) and

         A13: x2 in M;

        w1 in { (v + w) where w be VECTOR of V : w in M } by A10, RUSUB_4:def 8;

        then

        consider x1 be VECTOR of V such that

         A14: w1 = (v + x1) and

         A15: x1 in M;

        

         A16: ((r * w1) + ((1 - r) * w2)) = (((r * v) + (r * x1)) + ((1 - r) * (v + x2))) by A14, A12, RLVECT_1:def 5

        .= (((r * v) + (r * x1)) + (((1 - r) * v) + ((1 - r) * x2))) by RLVECT_1:def 5

        .= ((((r * v) + (r * x1)) + ((1 - r) * v)) + ((1 - r) * x2)) by RLVECT_1:def 3

        .= ((((r * v) + ((1 - r) * v)) + (r * x1)) + ((1 - r) * x2)) by RLVECT_1:def 3

        .= ((((r + (1 - r)) * v) + (r * x1)) + ((1 - r) * x2)) by RLVECT_1:def 6

        .= ((v + (r * x1)) + ((1 - r) * x2)) by RLVECT_1:def 8

        .= (v + ((r * x1) + ((1 - r) * x2))) by RLVECT_1:def 3;

        ((r * x1) + ((1 - r) * x2)) in M by A8, A9, A15, A13;

        then ((r * w1) + ((1 - r) * w2)) in { (v + w) where w be VECTOR of V : w in M } by A16;

        hence thesis by RUSUB_4:def 8;

      end;

      hence thesis by A1;

    end;

    theorem :: CONVEX1:8

    for V be RealLinearSpace holds ( Up ( (0). V)) is convex

    proof

      let V be RealLinearSpace;

      let u,v be VECTOR of V;

      let r be Real;

      assume that 0 < r and r < 1 and

       A1: u in ( Up ( (0). V)) and

       A2: v in ( Up ( (0). V));

      v in the carrier of ( (0). V) by A2, RUSUB_4:def 5;

      then v in {( 0. V)} by RLSUB_1:def 3;

      then

       A3: v = ( 0. V) by TARSKI:def 1;

      u in the carrier of ( (0). V) by A1, RUSUB_4:def 5;

      then u in {( 0. V)} by RLSUB_1:def 3;

      then u = ( 0. V) by TARSKI:def 1;

      

      then ((r * u) + ((1 - r) * v)) = (( 0. V) + ((1 - r) * ( 0. V))) by A3

      .= (( 0. V) + ( 0. V))

      .= ( 0. V);

      then ((r * u) + ((1 - r) * v)) in {( 0. V)} by TARSKI:def 1;

      then ((r * u) + ((1 - r) * v)) in the carrier of ( (0). V) by RLSUB_1:def 3;

      hence thesis by RUSUB_4:def 5;

    end;

    theorem :: CONVEX1:9

    

     Th9: for V be RealLinearSpace holds ( Up ( (Omega). V)) is convex

    proof

      let V be RealLinearSpace;

      let u,v be VECTOR of V;

      let r be Real;

      ( (Omega). V) = the RLSStruct of V by RLSUB_1:def 4;

      then ((r * u) + ((1 - r) * v)) in the carrier of ( (Omega). V);

      hence thesis by RUSUB_4:def 5;

    end;

    theorem :: CONVEX1:10

    for V be non empty RLSStruct, M be Subset of V st M = {} holds M is convex;

    theorem :: CONVEX1:11

    

     Th11: for V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M1,M2 be Subset of V, r1,r2 be Real st M1 is convex & M2 is convex holds ((r1 * M1) + (r2 * M2)) is convex

    proof

      let V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct;

      let M1,M2 be Subset of V;

      let r1,r2 be Real;

      assume that

       A1: M1 is convex and

       A2: M2 is convex;

      let u,v be VECTOR of V;

      let p be Real;

      assume that

       A3: 0 < p & p < 1 and

       A4: u in ((r1 * M1) + (r2 * M2)) and

       A5: v in ((r1 * M1) + (r2 * M2));

      v in { (x + y) where x,y be VECTOR of V : x in (r1 * M1) & y in (r2 * M2) } by A5, RUSUB_4:def 9;

      then

      consider v1,v2 be VECTOR of V such that

       A6: v = (v1 + v2) and

       A7: v1 in (r1 * M1) and

       A8: v2 in (r2 * M2);

      u in { (x + y) where x,y be VECTOR of V : x in (r1 * M1) & y in (r2 * M2) } by A4, RUSUB_4:def 9;

      then

      consider u1,u2 be VECTOR of V such that

       A9: u = (u1 + u2) and

       A10: u1 in (r1 * M1) and

       A11: u2 in (r2 * M2);

      consider y1 be VECTOR of V such that

       A12: v1 = (r1 * y1) and

       A13: y1 in M1 by A7;

      consider x1 be VECTOR of V such that

       A14: u1 = (r1 * x1) and

       A15: x1 in M1 by A10;

      

       A16: ((p * u1) + ((1 - p) * v1)) = (((r1 * p) * x1) + ((1 - p) * (r1 * y1))) by A14, A12, RLVECT_1:def 7

      .= (((r1 * p) * x1) + ((r1 * (1 - p)) * y1)) by RLVECT_1:def 7

      .= ((r1 * (p * x1)) + ((r1 * (1 - p)) * y1)) by RLVECT_1:def 7

      .= ((r1 * (p * x1)) + (r1 * ((1 - p) * y1))) by RLVECT_1:def 7

      .= (r1 * ((p * x1) + ((1 - p) * y1))) by RLVECT_1:def 5;

      consider y2 be VECTOR of V such that

       A17: v2 = (r2 * y2) and

       A18: y2 in M2 by A8;

      consider x2 be VECTOR of V such that

       A19: u2 = (r2 * x2) and

       A20: x2 in M2 by A11;

      

       A21: ((p * u2) + ((1 - p) * v2)) = (((r2 * p) * x2) + ((1 - p) * (r2 * y2))) by A19, A17, RLVECT_1:def 7

      .= (((r2 * p) * x2) + ((r2 * (1 - p)) * y2)) by RLVECT_1:def 7

      .= ((r2 * (p * x2)) + ((r2 * (1 - p)) * y2)) by RLVECT_1:def 7

      .= ((r2 * (p * x2)) + (r2 * ((1 - p) * y2))) by RLVECT_1:def 7

      .= (r2 * ((p * x2) + ((1 - p) * y2))) by RLVECT_1:def 5;

      ((p * x2) + ((1 - p) * y2)) in M2 by A2, A3, A20, A18;

      then

       A22: ((p * u2) + ((1 - p) * v2)) in (r2 * M2) by A21;

      ((p * x1) + ((1 - p) * y1)) in M1 by A1, A3, A15, A13;

      then

       A23: ((p * u1) + ((1 - p) * v1)) in { (r1 * x) where x be VECTOR of V : x in M1 } by A16;

      ((p * (u1 + u2)) + ((1 - p) * (v1 + v2))) = (((p * u1) + (p * u2)) + ((1 - p) * (v1 + v2))) by RLVECT_1:def 5

      .= (((p * u1) + (p * u2)) + (((1 - p) * v1) + ((1 - p) * v2))) by RLVECT_1:def 5

      .= ((((p * u1) + (p * u2)) + ((1 - p) * v1)) + ((1 - p) * v2)) by RLVECT_1:def 3

      .= ((((p * u1) + ((1 - p) * v1)) + (p * u2)) + ((1 - p) * v2)) by RLVECT_1:def 3

      .= (((p * u1) + ((1 - p) * v1)) + ((p * u2) + ((1 - p) * v2))) by RLVECT_1:def 3;

      then ((p * (u1 + u2)) + ((1 - p) * (v1 + v2))) in { (x + y) where x,y be VECTOR of V : x in (r1 * M1) & y in (r2 * M2) } by A23, A22;

      hence thesis by A9, A6, RUSUB_4:def 9;

    end;

    theorem :: CONVEX1:12

    

     Th12: for V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M be Subset of V, r1,r2 be Real holds ((r1 + r2) * M) c= ((r1 * M) + (r2 * M))

    proof

      let V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct;

      let M be Subset of V;

      let r1,r2 be Real;

      for x be VECTOR of V st x in ((r1 + r2) * M) holds x in ((r1 * M) + (r2 * M))

      proof

        let x be VECTOR of V;

        assume x in ((r1 + r2) * M);

        then

        consider w be VECTOR of V such that

         A1: x = ((r1 + r2) * w) and

         A2: w in M;

        

         A3: (r2 * w) in { (r2 * u) where u be VECTOR of V : u in M } by A2;

        x = ((r1 * w) + (r2 * w)) & (r1 * w) in (r1 * M) by A1, A2, RLVECT_1:def 6;

        then x in { (u + v) where u,v be VECTOR of V : u in (r1 * M) & v in (r2 * M) } by A3;

        hence thesis by RUSUB_4:def 9;

      end;

      hence thesis;

    end;

    

     Lm6: for V be non empty RLSStruct, M,N be Subset of V, r be Real st M c= N holds (r * M) c= (r * N)

    proof

      let V be non empty RLSStruct;

      let M,N be Subset of V;

      let r be Real;

      assume

       A1: M c= N;

      for x be VECTOR of V st x in (r * M) holds x in (r * N)

      proof

        let x be VECTOR of V;

        assume x in (r * M);

        then ex w be VECTOR of V st x = (r * w) & w in M;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    

     Lm7: for V be non empty RLSStruct, M be empty Subset of V, r be Real holds (r * M) = {}

    proof

      let V be non empty RLSStruct;

      let M be empty Subset of V;

      let r be Real;

      for x be VECTOR of V st x in (r * M) holds x in {}

      proof

        let x be VECTOR of V;

        assume x in (r * M);

        then ex v be VECTOR of V st x = (r * v) & v in {} ;

        hence thesis;

      end;

      then (r * M) c= {} ;

      hence thesis;

    end;

    

     Lm8: for V be non empty addLoopStr, M be empty Subset of V, N be Subset of V holds (M + N) = {}

    proof

      let V be non empty addLoopStr;

      let M be empty Subset of V;

      let N be Subset of V;

      

       A1: (M + N) = { (u + v) where u,v be Element of V : u in {} & v in N } by RUSUB_4:def 9;

      for x be Element of V st x in (M + N) holds x in {}

      proof

        let x be Element of V;

        assume x in (M + N);

        then ex u,v be Element of V st x = (u + v) & u in {} & v in N by A1;

        hence thesis;

      end;

      then (M + N) c= {} ;

      hence thesis;

    end;

    

     Lm9: for V be right_zeroed non empty addLoopStr, M be Subset of V holds (M + {( 0. V)}) = M

    proof

      let V be right_zeroed non empty addLoopStr;

      let M be Subset of V;

      for x be Element of V st x in (M + {( 0. V)}) holds x in M

      proof

        let x be Element of V;

        assume x in (M + {( 0. V)});

        then x in { (u + v) where u,v be Element of V : u in M & v in {( 0. V)} } by RUSUB_4:def 9;

        then

        consider u,v be Element of V such that

         A1: x = (u + v) & u in M and

         A2: v in {( 0. V)};

        v = ( 0. V) by A2, TARSKI:def 1;

        hence thesis by A1, RLVECT_1:def 4;

      end;

      then

       A3: (M + {( 0. V)}) c= M;

      for x be Element of V st x in M holds x in (M + {( 0. V)})

      proof

        let x be Element of V;

        

         A4: x = (x + ( 0. V)) & ( 0. V) in {( 0. V)} by RLVECT_1:def 4, TARSKI:def 1;

        assume x in M;

        then x in { (u + v) where u,v be Element of V : u in M & v in {( 0. V)} } by A4;

        hence thesis by RUSUB_4:def 9;

      end;

      then M c= (M + {( 0. V)});

      hence thesis by A3;

    end;

    

     Lm10: for V be RealLinearSpace, M be Subset of V, r1,r2 be Real st r1 >= 0 & r2 >= 0 & M is convex holds ((r1 * M) + (r2 * M)) c= ((r1 + r2) * M)

    proof

      let V be RealLinearSpace;

      let M be Subset of V;

      let r1,r2 be Real;

      assume that

       A1: r1 >= 0 and

       A2: r2 >= 0 and

       A3: M is convex;

      per cases ;

        suppose M is empty;

        then (r1 * M) = {} & ((r1 + r2) * M) = {} by Lm7;

        hence thesis by Lm8;

      end;

        suppose

         A4: M is non empty;

        per cases ;

          suppose

           A5: r1 = 0 ;

          then (r1 * M) = {( 0. V)} by A4, Lm2;

          hence thesis by A5, Lm9;

        end;

          suppose

           A6: r2 = 0 ;

          then (r2 * M) = {( 0. V)} by A4, Lm2;

          hence thesis by A6, Lm9;

        end;

          suppose

           A7: r1 <> 0 & r2 <> 0 ;

          then (r1 + r2) > r1 by A2, XREAL_1: 29;

          then

           A8: (r1 / (r1 + r2)) < 1 by A1, XREAL_1: 189;

           0 < (r1 / (r1 + r2)) by A1, A2, A7, XREAL_1: 139;

          then (((r1 / (r1 + r2)) * M) + ((1 - (r1 / (r1 + r2))) * M)) c= M by A3, A8, Th4;

          then

           A9: ((r1 + r2) * (((r1 / (r1 + r2)) * M) + ((1 - (r1 / (r1 + r2))) * M))) c= ((r1 + r2) * M) by Lm6;

          (1 - (r1 / (r1 + r2))) = (((r1 + r2) / (r1 + r2)) - (r1 / (r1 + r2))) by A1, A2, A7, XCMPLX_1: 60

          .= (((r1 + r2) - r1) / (r1 + r2)) by XCMPLX_1: 120

          .= (r2 / (r1 + r2));

          

          then

           A10: ((r1 + r2) * ((1 - (r1 / (r1 + r2))) * M)) = (((r2 / (r1 + r2)) * (r1 + r2)) * M) by Lm4

          .= (r2 * M) by A1, A2, A7, XCMPLX_1: 87;

          ((r1 + r2) * ((r1 / (r1 + r2)) * M)) = (((r1 / (r1 + r2)) * (r1 + r2)) * M) by Lm4

          .= (r1 * M) by A1, A2, A7, XCMPLX_1: 87;

          hence thesis by A9, A10, Lm5;

        end;

      end;

    end;

    theorem :: CONVEX1:13

    for V be RealLinearSpace, M be Subset of V, r1,r2 be Real st r1 >= 0 & r2 >= 0 & M is convex holds ((r1 * M) + (r2 * M)) = ((r1 + r2) * M) by Lm10, Th12;

    theorem :: CONVEX1:14

    for V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M1,M2,M3 be Subset of V, r1,r2,r3 be Real st M1 is convex & M2 is convex & M3 is convex holds (((r1 * M1) + (r2 * M2)) + (r3 * M3)) is convex

    proof

      let V be Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct;

      let M1,M2,M3 be Subset of V;

      let r1,r2,r3 be Real;

      assume that

       A1: M1 is convex & M2 is convex and

       A2: M3 is convex;

      ((r1 * M1) + (r2 * M2)) is convex by A1, Th11;

      then ((1 * ((r1 * M1) + (r2 * M2))) + (r3 * M3)) is convex by A2, Th11;

      hence thesis by Lm1;

    end;

    theorem :: CONVEX1:15

    

     Th15: for V be non empty RLSStruct, F be Subset-Family of V st (for M be Subset of V st M in F holds M is convex) holds ( meet F) is convex

    proof

      let V be non empty RLSStruct;

      let F be Subset-Family of V;

      assume

       A1: for M be Subset of V st M in F holds M is convex;

      per cases ;

        suppose F = {} ;

        then ( meet F) = {} by SETFAM_1:def 1;

        hence thesis;

      end;

        suppose

         A2: F <> {} ;

        ( meet F) is convex

        proof

          let u,v be VECTOR of V;

          let r be Real;

          assume that

           A3: 0 < r & r < 1 and

           A4: u in ( meet F) and

           A5: v in ( meet F);

          for M be set st M in F holds ((r * u) + ((1 - r) * v)) in M

          proof

            let M be set;

            assume

             A6: M in F;

            then

            reconsider M as Subset of V;

            

             A7: v in M by A5, A6, SETFAM_1:def 1;

            M is convex & u in M by A1, A4, A6, SETFAM_1:def 1;

            hence thesis by A3, A7;

          end;

          hence thesis by A2, SETFAM_1:def 1;

        end;

        hence thesis;

      end;

    end;

    theorem :: CONVEX1:16

    

     Th16: for V be non empty RLSStruct, M be Subset of V st M is Affine holds M is convex

    proof

      let V be non empty RLSStruct;

      let M be Subset of V;

      assume

       A1: M is Affine;

      let u,v be VECTOR of V;

      let r be Real;

      assume that 0 < r and r < 1 and

       A2: u in M & v in M;

      set p = (1 - r);

      (1 - p) = r;

      hence thesis by A1, A2, RUSUB_4:def 4;

    end;

    registration

      let V be non empty RLSStruct;

      cluster non empty convex for Subset of V;

      existence

      proof

        set M = the non empty Affine Subset of V;

        M is convex by Th16;

        hence thesis;

      end;

    end

    registration

      let V be non empty RLSStruct;

      cluster empty convex for Subset of V;

      existence

      proof

        ( {} V) is convex;

        hence thesis;

      end;

    end

    theorem :: CONVEX1:17

    for V be RealUnitarySpace-like non empty UNITSTR, M be Subset of V, v be VECTOR of V, r be Real st M = { u where u be VECTOR of V : (u .|. v) >= r } holds M is convex

    proof

      let V be RealUnitarySpace-like non empty UNITSTR;

      let M be Subset of V;

      let v be VECTOR of V;

      let r be Real;

      assume

       A1: M = { u where u be VECTOR of V : (u .|. v) >= r };

      let x,y be VECTOR of V;

      let p be Real;

      assume that

       A2: 0 < p and

       A3: p < 1 and

       A4: x in M and

       A5: y in M;

      ( 0 + p) < 1 by A3;

      then

       A6: 0 < (1 - p) by XREAL_1: 20;

      consider u2 be VECTOR of V such that

       A7: y = u2 and

       A8: (u2 .|. v) >= r by A1, A5;

      (((1 - p) * y) .|. v) = ((1 - p) * (u2 .|. v)) by A7, BHSP_1:def 2;

      then

       A9: (((1 - p) * y) .|. v) >= ((1 - p) * r) by A8, A6, XREAL_1: 64;

      consider u1 be VECTOR of V such that

       A10: x = u1 and

       A11: (u1 .|. v) >= r by A1, A4;

      ((p * x) .|. v) = (p * (u1 .|. v)) by A10, BHSP_1:def 2;

      then

       A12: ((p * x) .|. v) >= (p * r) by A2, A11, XREAL_1: 64;

      (((p * x) + ((1 - p) * y)) .|. v) = (((p * x) .|. v) + (((1 - p) * y) .|. v)) by BHSP_1:def 2;

      then (((p * x) + ((1 - p) * y)) .|. v) >= ((p * r) + ((1 - p) * r)) by A12, A9, XREAL_1: 7;

      hence thesis by A1;

    end;

    theorem :: CONVEX1:18

    for V be RealUnitarySpace-like non empty UNITSTR, M be Subset of V, v be VECTOR of V, r be Real st M = { u where u be VECTOR of V : (u .|. v) > r } holds M is convex

    proof

      let V be RealUnitarySpace-like non empty UNITSTR;

      let M be Subset of V;

      let v be VECTOR of V;

      let r be Real;

      assume

       A1: M = { u where u be VECTOR of V : (u .|. v) > r };

      let x,y be VECTOR of V;

      let p be Real;

      assume that

       A2: 0 < p and

       A3: p < 1 and

       A4: x in M and

       A5: y in M;

      ( 0 + p) < 1 by A3;

      then

       A6: 0 < (1 - p) by XREAL_1: 20;

      consider u2 be VECTOR of V such that

       A7: y = u2 and

       A8: (u2 .|. v) > r by A1, A5;

      (((1 - p) * y) .|. v) = ((1 - p) * (u2 .|. v)) by A7, BHSP_1:def 2;

      then

       A9: (((1 - p) * y) .|. v) > ((1 - p) * r) by A8, A6, XREAL_1: 68;

      consider u1 be VECTOR of V such that

       A10: x = u1 and

       A11: (u1 .|. v) > r by A1, A4;

      ((p * x) .|. v) = (p * (u1 .|. v)) by A10, BHSP_1:def 2;

      then

       A12: ((p * x) .|. v) > (p * r) by A2, A11, XREAL_1: 68;

      (((p * x) + ((1 - p) * y)) .|. v) = (((p * x) .|. v) + (((1 - p) * y) .|. v)) by BHSP_1:def 2;

      then (((p * x) + ((1 - p) * y)) .|. v) > ((p * r) + ((1 - p) * r)) by A12, A9, XREAL_1: 8;

      hence thesis by A1;

    end;

    theorem :: CONVEX1:19

    for V be RealUnitarySpace-like non empty UNITSTR, M be Subset of V, v be VECTOR of V, r be Real st M = { u where u be VECTOR of V : (u .|. v) <= r } holds M is convex

    proof

      let V be RealUnitarySpace-like non empty UNITSTR;

      let M be Subset of V;

      let v be VECTOR of V;

      let r be Real;

      assume

       A1: M = { u where u be VECTOR of V : (u .|. v) <= r };

      let x,y be VECTOR of V;

      let p be Real;

      assume that

       A2: 0 < p and

       A3: p < 1 and

       A4: x in M and

       A5: y in M;

      ( 0 + p) < 1 by A3;

      then

       A6: 0 < (1 - p) by XREAL_1: 20;

      consider u2 be VECTOR of V such that

       A7: y = u2 and

       A8: (u2 .|. v) <= r by A1, A5;

      (((1 - p) * y) .|. v) = ((1 - p) * (u2 .|. v)) by A7, BHSP_1:def 2;

      then

       A9: (((1 - p) * y) .|. v) <= ((1 - p) * r) by A8, A6, XREAL_1: 64;

      consider u1 be VECTOR of V such that

       A10: x = u1 and

       A11: (u1 .|. v) <= r by A1, A4;

      ((p * x) .|. v) = (p * (u1 .|. v)) by A10, BHSP_1:def 2;

      then

       A12: ((p * x) .|. v) <= (p * r) by A2, A11, XREAL_1: 64;

      (((p * x) + ((1 - p) * y)) .|. v) = (((p * x) .|. v) + (((1 - p) * y) .|. v)) by BHSP_1:def 2;

      then (((p * x) + ((1 - p) * y)) .|. v) <= ((p * r) + ((1 - p) * r)) by A12, A9, XREAL_1: 7;

      hence thesis by A1;

    end;

    theorem :: CONVEX1:20

    for V be RealUnitarySpace-like non empty UNITSTR, M be Subset of V, v be VECTOR of V, r be Real st M = { u where u be VECTOR of V : (u .|. v) < r } holds M is convex

    proof

      let V be RealUnitarySpace-like non empty UNITSTR;

      let M be Subset of V;

      let v be VECTOR of V;

      let r be Real;

      assume

       A1: M = { u where u be VECTOR of V : (u .|. v) < r };

      let x,y be VECTOR of V;

      let p be Real;

      assume that

       A2: 0 < p and

       A3: p < 1 and

       A4: x in M and

       A5: y in M;

      ( 0 + p) < 1 by A3;

      then

       A6: 0 < (1 - p) by XREAL_1: 20;

      consider u2 be VECTOR of V such that

       A7: y = u2 and

       A8: (u2 .|. v) < r by A1, A5;

      (((1 - p) * y) .|. v) = ((1 - p) * (u2 .|. v)) by A7, BHSP_1:def 2;

      then

       A9: (((1 - p) * y) .|. v) < ((1 - p) * r) by A8, A6, XREAL_1: 68;

      consider u1 be VECTOR of V such that

       A10: x = u1 and

       A11: (u1 .|. v) < r by A1, A4;

      ((p * x) .|. v) = (p * (u1 .|. v)) by A10, BHSP_1:def 2;

      then

       A12: ((p * x) .|. v) < (p * r) by A2, A11, XREAL_1: 68;

      (((p * x) + ((1 - p) * y)) .|. v) = (((p * x) .|. v) + (((1 - p) * y) .|. v)) by BHSP_1:def 2;

      then (((p * x) + ((1 - p) * y)) .|. v) < ((p * r) + ((1 - p) * r)) by A12, A9, XREAL_1: 8;

      hence thesis by A1;

    end;

    begin

    definition

      let V be RealLinearSpace, L be Linear_Combination of V;

      :: CONVEX1:def3

      attr L is convex means ex F be FinSequence of the carrier of V st F is one-to-one & ( rng F) = ( Carrier L) & ex f be FinSequence of REAL st ( len f) = ( len F) & ( Sum f) = 1 & for n be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0 ;

    end

    theorem :: CONVEX1:21

    

     Th21: for V be RealLinearSpace, L be Linear_Combination of V st L is convex holds ( Carrier L) <> {}

    proof

      let V be RealLinearSpace;

      let L be Linear_Combination of V;

      assume L is convex;

      then

      consider F be FinSequence of the carrier of V such that

       A1: F is one-to-one & ( rng F) = ( Carrier L) and

       A2: ex f be FinSequence of REAL st ( len f) = ( len F) & ( Sum f) = 1 & for n be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0 ;

      consider f be FinSequence of REAL such that

       A3: ( len f) = ( len F) & ( Sum f) = 1 & for n be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0 by A2;

      assume ( Carrier L) = {} ;

      then ( len F) = 0 by A1, CARD_1: 27, FINSEQ_4: 62;

      then f = ( <*> REAL ) by A3;

      hence contradiction by A3, RVSUM_1: 72;

    end;

    theorem :: CONVEX1:22

    for V be RealLinearSpace, L be Linear_Combination of V, v be VECTOR of V st L is convex & (L . v) <= 0 holds not v in ( Carrier L)

    proof

      let V be RealLinearSpace;

      let L be Linear_Combination of V;

      let v be VECTOR of V;

      assume that

       A1: L is convex and

       A2: (L . v) <= 0 ;

      per cases by A2;

        suppose (L . v) = 0 ;

        hence thesis by RLVECT_2: 19;

      end;

        suppose

         A3: (L . v) < 0 ;

        now

          consider F be FinSequence of the carrier of V such that F is one-to-one and

           A4: ( rng F) = ( Carrier L) and

           A5: ex f be FinSequence of REAL st ( len f) = ( len F) & ( Sum f) = 1 & for n be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0 by A1;

          assume v in ( Carrier L);

          then

          consider n be object such that

           A6: n in ( dom F) and

           A7: (F . n) = v by A4, FUNCT_1:def 3;

          reconsider n as Element of NAT by A6;

          consider f be FinSequence of REAL such that

           A8: ( len f) = ( len F) and ( Sum f) = 1 and

           A9: for n be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0 by A5;

          n in ( Seg ( len F)) by A6, FINSEQ_1:def 3;

          then

           A10: n in ( dom f) by A8, FINSEQ_1:def 3;

          then (L . v) = (f . n) by A9, A7;

          hence contradiction by A3, A9, A10;

        end;

        hence thesis;

      end;

    end;

    theorem :: CONVEX1:23

    for V be RealLinearSpace, L be Linear_Combination of V st L is convex holds L <> ( ZeroLC V) by Th21, RLVECT_2:def 5;

    

     Lm11: for V be RealLinearSpace, v be VECTOR of V, L be Linear_Combination of V st L is convex & ( Carrier L) = {v} holds (L . v) = 1 & ( Sum L) = ((L . v) * v)

    proof

      let V be RealLinearSpace;

      let v be VECTOR of V;

      let L be Linear_Combination of V;

      assume that

       A1: L is convex and

       A2: ( Carrier L) = {v};

      reconsider L as Linear_Combination of {v} by A2, RLVECT_2:def 6;

      consider F be FinSequence of the carrier of V such that

       A3: F is one-to-one & ( rng F) = ( Carrier L) and

       A4: ex f be FinSequence of REAL st ( len f) = ( len F) & ( Sum f) = 1 & for n be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0 by A1;

      

       A5: F = <*v*> by A2, A3, FINSEQ_3: 97;

      consider f be FinSequence of REAL such that

       A6: ( len f) = ( len F) and

       A7: ( Sum f) = 1 and

       A8: for n be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0 by A4;

      reconsider r = (f /. 1) as Element of REAL ;

      ( card ( Carrier L)) = 1 by A2, CARD_1: 30;

      then ( len F) = 1 by A3, FINSEQ_4: 62;

      then

       A9: ( dom f) = ( Seg 1) by A6, FINSEQ_1:def 3;

      then

       A10: 1 in ( dom f) by FINSEQ_1: 2, TARSKI:def 1;

      then

       A11: (f . 1) = (f /. 1) by PARTFUN1:def 6;

      then f = <*r*> by A9, FINSEQ_1:def 8;

      then

       A12: ( Sum f) = r by FINSOP_1: 11;

      (f . 1) = (L . (F . 1)) by A8, A10;

      hence thesis by A7, A11, A12, A5, FINSEQ_1:def 8, RLVECT_2: 32;

    end;

    

     Lm12: for V be RealLinearSpace, v1,v2 be VECTOR of V, L be Linear_Combination of V st L is convex & ( Carrier L) = {v1, v2} & v1 <> v2 holds ((L . v1) + (L . v2)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & ( Sum L) = (((L . v1) * v1) + ((L . v2) * v2))

    proof

      let V be RealLinearSpace;

      let v1,v2 be VECTOR of V;

      let L be Linear_Combination of V;

      assume that

       A1: L is convex and

       A2: ( Carrier L) = {v1, v2} and

       A3: v1 <> v2;

      reconsider L as Linear_Combination of {v1, v2} by A2, RLVECT_2:def 6;

      consider F be FinSequence of the carrier of V such that

       A4: F is one-to-one & ( rng F) = ( Carrier L) and

       A5: ex f be FinSequence of REAL st ( len f) = ( len F) & ( Sum f) = 1 & for n be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0 by A1;

      consider f be FinSequence of REAL such that

       A6: ( len f) = ( len F) and

       A7: ( Sum f) = 1 and

       A8: for n be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0 by A5;

      ( len F) = ( card {v1, v2}) by A2, A4, FINSEQ_4: 62;

      then

       A9: ( len f) = 2 by A3, A6, CARD_2: 57;

      then

       A10: ( dom f) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

      then

       A11: 1 in ( dom f) by TARSKI:def 2;

      then

       A12: (f . 1) = (L . (F . 1)) by A8;

      then (f /. 1) = (L . (F . 1)) by A11, PARTFUN1:def 6;

      then

      reconsider r1 = (L . (F . 1)) as Element of REAL ;

      

       A13: 2 in ( dom f) by A10, TARSKI:def 2;

      then

       A14: (f . 2) = (L . (F . 2)) by A8;

      then (f /. 2) = (L . (F . 2)) by A13, PARTFUN1:def 6;

      then

      reconsider r2 = (L . (F . 2)) as Element of REAL ;

      

       A15: f = <*r1, r2*> by A9, A12, A14, FINSEQ_1: 44;

      now

        per cases by A2, A3, A4, FINSEQ_3: 99;

          suppose F = <*v1, v2*>;

          then (F . 1) = v1 & (F . 2) = v2 by FINSEQ_1: 44;

          hence ((L . v1) + (L . v2)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 by A7, A8, A11, A13, A12, A14, A15, RVSUM_1: 77;

        end;

          suppose F = <*v2, v1*>;

          then (F . 1) = v2 & (F . 2) = v1 by FINSEQ_1: 44;

          hence ((L . v1) + (L . v2)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 by A7, A8, A11, A13, A12, A14, A15, RVSUM_1: 77;

        end;

      end;

      hence thesis by A3, RLVECT_2: 33;

    end;

    

     Lm13: for p be FinSequence, x,y,z be set st p is one-to-one & ( rng p) = {x, y, z} & x <> y & y <> z & z <> x holds p = <*x, y, z*> or p = <*x, z, y*> or p = <*y, x, z*> or p = <*y, z, x*> or p = <*z, x, y*> or p = <*z, y, x*>

    proof

      let p be FinSequence;

      let x,y,z be set;

      assume that

       A1: p is one-to-one and

       A2: ( rng p) = {x, y, z} and

       A3: x <> y & y <> z & z <> x;

      

       A4: ( len p) = 3 by A1, A2, A3, FINSEQ_3: 101;

      then

       A5: ( dom p) = {1, 2, 3} by FINSEQ_1:def 3, FINSEQ_3: 1;

      then

       A6: 2 in ( dom p) by ENUMSET1:def 1;

      then

       A7: (p . 2) in ( rng p) by FUNCT_1:def 3;

      

       A8: 3 in ( dom p) by A5, ENUMSET1:def 1;

      then

       A9: (p . 3) in ( rng p) by FUNCT_1:def 3;

      

       A10: 1 in ( dom p) by A5, ENUMSET1:def 1;

      then (p . 1) in ( rng p) by FUNCT_1:def 3;

      then (p . 1) = x & (p . 2) = x & (p . 3) = x or (p . 1) = x & (p . 2) = x & (p . 3) = y or (p . 1) = x & (p . 2) = x & (p . 3) = z or (p . 1) = x & (p . 2) = y & (p . 3) = x or (p . 1) = x & (p . 2) = y & (p . 3) = y or (p . 1) = x & (p . 2) = y & (p . 3) = z or (p . 1) = x & (p . 2) = z & (p . 3) = x or (p . 1) = x & (p . 2) = z & (p . 3) = y or (p . 1) = x & (p . 2) = z & (p . 3) = z or (p . 1) = y & (p . 2) = x & (p . 3) = x or (p . 1) = y & (p . 2) = x & (p . 3) = y or (p . 1) = y & (p . 2) = x & (p . 3) = z or (p . 1) = y & (p . 2) = y & (p . 3) = x or (p . 1) = y & (p . 2) = y & (p . 3) = y or (p . 1) = y & (p . 2) = y & (p . 3) = z or (p . 1) = y & (p . 2) = z & (p . 3) = x or (p . 1) = y & (p . 2) = z & (p . 3) = y or (p . 1) = y & (p . 2) = z & (p . 3) = z or (p . 1) = z & (p . 2) = x & (p . 3) = x or (p . 1) = z & (p . 2) = x & (p . 3) = y or (p . 1) = z & (p . 2) = x & (p . 3) = z or (p . 1) = z & (p . 2) = y & (p . 3) = x or (p . 1) = z & (p . 2) = y & (p . 3) = y or (p . 1) = z & (p . 2) = y & (p . 3) = z or (p . 1) = z & (p . 2) = z & (p . 3) = x or (p . 1) = z & (p . 2) = z & (p . 3) = y or (p . 1) = z & (p . 2) = z & (p . 3) = z by A2, A7, A9, ENUMSET1:def 1;

      hence thesis by A1, A4, A10, A6, A8, FINSEQ_1: 45, FUNCT_1:def 4;

    end;

    

     Lm14: for V be RealLinearSpace, v1,v2,v3 be VECTOR of V, L be Linear_Combination of {v1, v2, v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 holds ( Sum L) = ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3))

    proof

      let V be RealLinearSpace;

      let v1,v2,v3 be VECTOR of V;

      let L be Linear_Combination of {v1, v2, v3};

      assume that

       A1: v1 <> v2 and

       A2: v2 <> v3 and

       A3: v3 <> v1;

      

       A4: ( Carrier L) c= {v1, v2, v3} by RLVECT_2:def 6;

      per cases by A4, ZFMISC_1: 118;

        suppose ( Carrier L) = {} ;

        then

         A5: L = ( ZeroLC V) by RLVECT_2:def 5;

        

        then ( Sum L) = ( 0. V) by RLVECT_2: 30

        .= (( 0. V) + ( 0. V))

        .= ((( 0. V) + ( 0. V)) + ( 0. V))

        .= ((( 0 * v1) + ( 0. V)) + ( 0. V)) by RLVECT_1: 10

        .= ((( 0 * v1) + ( 0 * v2)) + ( 0. V)) by RLVECT_1: 10

        .= ((( 0 * v1) + ( 0 * v2)) + ( 0 * v3)) by RLVECT_1: 10

        .= ((((L . v1) * v1) + ( 0 * v2)) + ( 0 * v3)) by A5, RLVECT_2: 20

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ( 0 * v3)) by A5, RLVECT_2: 20

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)) by A5, RLVECT_2: 20;

        hence thesis;

      end;

        suppose

         A6: ( Carrier L) = {v1};

        then

        reconsider L as Linear_Combination of {v1} by RLVECT_2:def 6;

        

         A7: not v2 in ( Carrier L) by A1, A6, TARSKI:def 1;

        

         A8: not v3 in ( Carrier L) by A3, A6, TARSKI:def 1;

        ( Sum L) = ((L . v1) * v1) by RLVECT_2: 32

        .= (((L . v1) * v1) + ( 0. V))

        .= ((((L . v1) * v1) + ( 0. V)) + ( 0. V))

        .= ((((L . v1) * v1) + ( 0 * v2)) + ( 0. V)) by RLVECT_1: 10

        .= ((((L . v1) * v1) + ( 0 * v2)) + ( 0 * v3)) by RLVECT_1: 10

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ( 0 * v3)) by A7, RLVECT_2: 19

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)) by A8, RLVECT_2: 19;

        hence thesis;

      end;

        suppose

         A9: ( Carrier L) = {v2};

        then

        reconsider L as Linear_Combination of {v2} by RLVECT_2:def 6;

        

         A10: not v1 in ( Carrier L) by A1, A9, TARSKI:def 1;

        

         A11: not v3 in ( Carrier L) by A2, A9, TARSKI:def 1;

        ( Sum L) = ((L . v2) * v2) by RLVECT_2: 32

        .= (( 0. V) + ((L . v2) * v2))

        .= ((( 0. V) + ((L . v2) * v2)) + ( 0. V))

        .= ((( 0 * v1) + ((L . v2) * v2)) + ( 0. V)) by RLVECT_1: 10

        .= ((( 0 * v1) + ((L . v2) * v2)) + ( 0 * v3)) by RLVECT_1: 10

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ( 0 * v3)) by A10, RLVECT_2: 19

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)) by A11, RLVECT_2: 19;

        hence thesis;

      end;

        suppose

         A12: ( Carrier L) = {v3};

        then

        reconsider L as Linear_Combination of {v3} by RLVECT_2:def 6;

        

         A13: not v1 in ( Carrier L) by A3, A12, TARSKI:def 1;

        

         A14: not v2 in ( Carrier L) by A2, A12, TARSKI:def 1;

        ( Sum L) = ((L . v3) * v3) by RLVECT_2: 32

        .= (( 0. V) + ((L . v3) * v3))

        .= ((( 0. V) + ( 0. V)) + ((L . v3) * v3))

        .= ((( 0 * v1) + ( 0. V)) + ((L . v3) * v3)) by RLVECT_1: 10

        .= ((( 0 * v1) + ( 0 * v2)) + ((L . v3) * v3)) by RLVECT_1: 10

        .= ((((L . v1) * v1) + ( 0 * v2)) + ((L . v3) * v3)) by A13, RLVECT_2: 19

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)) by A14, RLVECT_2: 19;

        hence thesis;

      end;

        suppose

         A15: ( Carrier L) = {v1, v2};

        

        then

         A16: ( Sum L) = (((L . v1) * v1) + ((L . v2) * v2)) by A1, RLVECT_2: 36

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ( 0. V))

        .= ((((L . v1) * v1) + ((L . v2) * v2)) + ( 0 * v3)) by RLVECT_1: 10;

         not v3 in ( Carrier L) by A2, A3, A15, TARSKI:def 2;

        hence thesis by A16, RLVECT_2: 19;

      end;

        suppose

         A17: ( Carrier L) = {v1, v3};

        

        then

         A18: ( Sum L) = (((L . v1) * v1) + ((L . v3) * v3)) by A3, RLVECT_2: 36

        .= ((((L . v1) * v1) + ( 0. V)) + ((L . v3) * v3))

        .= ((((L . v1) * v1) + ( 0 * v2)) + ((L . v3) * v3)) by RLVECT_1: 10;

         not v2 in ( Carrier L) by A1, A2, A17, TARSKI:def 2;

        hence thesis by A18, RLVECT_2: 19;

      end;

        suppose

         A19: ( Carrier L) = {v2, v3};

        

        then

         A20: ( Sum L) = (((L . v2) * v2) + ((L . v3) * v3)) by A2, RLVECT_2: 36

        .= ((( 0. V) + ((L . v2) * v2)) + ((L . v3) * v3))

        .= ((( 0 * v1) + ((L . v2) * v2)) + ((L . v3) * v3)) by RLVECT_1: 10;

         not v1 in ( Carrier L) by A1, A3, A19, TARSKI:def 2;

        hence thesis by A20, RLVECT_2: 19;

      end;

        suppose ( Carrier L) = {v1, v2, v3};

        then

        consider F be FinSequence of the carrier of V such that

         A21: F is one-to-one & ( rng F) = {v1, v2, v3} and

         A22: ( Sum L) = ( Sum (L (#) F)) by RLVECT_2:def 8;

        F = <*v1, v2, v3*> or F = <*v1, v3, v2*> or F = <*v2, v1, v3*> or F = <*v2, v3, v1*> or F = <*v3, v1, v2*> or F = <*v3, v2, v1*> by A1, A2, A3, A21, Lm13;

        then (L (#) F) = <*((L . v1) * v1), ((L . v2) * v2), ((L . v3) * v3)*> or (L (#) F) = <*((L . v1) * v1), ((L . v3) * v3), ((L . v2) * v2)*> or (L (#) F) = <*((L . v2) * v2), ((L . v1) * v1), ((L . v3) * v3)*> or (L (#) F) = <*((L . v2) * v2), ((L . v3) * v3), ((L . v1) * v1)*> or (L (#) F) = <*((L . v3) * v3), ((L . v1) * v1), ((L . v2) * v2)*> or (L (#) F) = <*((L . v3) * v3), ((L . v2) * v2), ((L . v1) * v1)*> by RLVECT_2: 28;

        then ( Sum L) = ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)) or ( Sum L) = (((L . v1) * v1) + (((L . v2) * v2) + ((L . v3) * v3))) or ( Sum L) = (((L . v2) * v2) + (((L . v1) * v1) + ((L . v3) * v3))) by A22, RLVECT_1: 46;

        hence thesis by RLVECT_1:def 3;

      end;

    end;

    

     Lm15: for V be RealLinearSpace, v1,v2,v3 be VECTOR of V, L be Linear_Combination of V st L is convex & ( Carrier L) = {v1, v2, v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds (((L . v1) + (L . v2)) + (L . v3)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & (L . v3) >= 0 & ( Sum L) = ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3))

    proof

      let V be RealLinearSpace;

      let v1,v2,v3 be VECTOR of V;

      let L be Linear_Combination of V;

      assume that

       A1: L is convex and

       A2: ( Carrier L) = {v1, v2, v3} and

       A3: v1 <> v2 & v2 <> v3 & v3 <> v1;

      reconsider L as Linear_Combination of {v1, v2, v3} by A2, RLVECT_2:def 6;

      consider F be FinSequence of the carrier of V such that

       A4: F is one-to-one & ( rng F) = ( Carrier L) and

       A5: ex f be FinSequence of REAL st ( len f) = ( len F) & ( Sum f) = 1 & for n be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0 by A1;

      consider f be FinSequence of REAL such that

       A6: ( len f) = ( len F) and

       A7: ( Sum f) = 1 and

       A8: for n be Nat st n in ( dom f) holds (f . n) = (L . (F . n)) & (f . n) >= 0 by A5;

      ( len F) = ( card {v1, v2, v3}) by A2, A4, FINSEQ_4: 62;

      then

       A9: ( len f) = 3 by A3, A6, CARD_2: 58;

      then

       A10: ( dom f) = {1, 2, 3} by FINSEQ_1:def 3, FINSEQ_3: 1;

      then

       A11: 1 in ( dom f) by ENUMSET1:def 1;

      then

       A12: (f . 1) = (L . (F . 1)) by A8;

      then (f /. 1) = (L . (F . 1)) by A11, PARTFUN1:def 6;

      then

      reconsider r1 = (L . (F . 1)) as Element of REAL ;

      

       A13: 3 in ( dom f) by A10, ENUMSET1:def 1;

      then

       A14: (f . 3) = (L . (F . 3)) by A8;

      then (f /. 3) = (L . (F . 3)) by A13, PARTFUN1:def 6;

      then

      reconsider r3 = (L . (F . 3)) as Element of REAL ;

      

       A15: 2 in ( dom f) by A10, ENUMSET1:def 1;

      then

       A16: (f . 2) = (L . (F . 2)) by A8;

      then (f /. 2) = (L . (F . 2)) by A15, PARTFUN1:def 6;

      then

      reconsider r2 = (L . (F . 2)) as Element of REAL ;

      

       A17: f = <*r1, r2, r3*> by A9, A12, A16, A14, FINSEQ_1: 45;

      then

       A18: (((L . (F . 1)) + (L . (F . 2))) + (L . (F . 3))) = 1 by A7, RVSUM_1: 78;

      now

        per cases by A2, A3, A4, Lm13;

          suppose

           A19: F = <*v1, v2, v3*>;

          then

           A20: (F . 3) = v3 by FINSEQ_1: 45;

          (F . 1) = v1 & (F . 2) = v2 by A19, FINSEQ_1: 45;

          hence (((L . v1) + (L . v2)) + (L . v3)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & (L . v3) >= 0 by A7, A8, A11, A15, A13, A12, A16, A14, A17, A20, RVSUM_1: 78;

        end;

          suppose

           A21: F = <*v1, v3, v2*>;

          then

           A22: (F . 3) = v2 by FINSEQ_1: 45;

          (F . 1) = v1 & (F . 2) = v3 by A21, FINSEQ_1: 45;

          hence (((L . v1) + (L . v2)) + (L . v3)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & (L . v3) >= 0 by A8, A11, A15, A13, A12, A16, A14, A18, A22;

        end;

          suppose

           A23: F = <*v2, v1, v3*>;

          then

           A24: (F . 3) = v3 by FINSEQ_1: 45;

          (F . 1) = v2 & (F . 2) = v1 by A23, FINSEQ_1: 45;

          hence (((L . v1) + (L . v2)) + (L . v3)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & (L . v3) >= 0 by A7, A8, A11, A15, A13, A12, A16, A14, A17, A24, RVSUM_1: 78;

        end;

          suppose

           A25: F = <*v2, v3, v1*>;

          then

           A26: (F . 3) = v1 by FINSEQ_1: 45;

          (F . 1) = v2 & (F . 2) = v3 by A25, FINSEQ_1: 45;

          hence (((L . v1) + (L . v2)) + (L . v3)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & (L . v3) >= 0 by A8, A11, A15, A13, A12, A16, A14, A18, A26;

        end;

          suppose

           A27: F = <*v3, v1, v2*>;

          then

           A28: (F . 3) = v2 by FINSEQ_1: 45;

          (F . 1) = v3 & (F . 2) = v1 by A27, FINSEQ_1: 45;

          hence (((L . v1) + (L . v2)) + (L . v3)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & (L . v3) >= 0 by A8, A11, A15, A13, A12, A16, A14, A18, A28;

        end;

          suppose

           A29: F = <*v3, v2, v1*>;

          then

           A30: (F . 3) = v1 by FINSEQ_1: 45;

          (F . 1) = v3 & (F . 2) = v2 by A29, FINSEQ_1: 45;

          hence (((L . v1) + (L . v2)) + (L . v3)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & (L . v3) >= 0 by A8, A11, A15, A13, A12, A16, A14, A18, A30;

        end;

      end;

      hence thesis by A3, Lm14;

    end;

    theorem :: CONVEX1:24

    for V be RealLinearSpace, v be VECTOR of V, L be Linear_Combination of {v} st L is convex holds (L . v) = 1 & ( Sum L) = ((L . v) * v)

    proof

      let V be RealLinearSpace;

      let v be VECTOR of V;

      let L be Linear_Combination of {v};

      ( Carrier L) c= {v} by RLVECT_2:def 6;

      then

       A1: ( Carrier L) = {} or ( Carrier L) = {v} by ZFMISC_1: 33;

      assume L is convex;

      hence thesis by A1, Lm11, Th21;

    end;

    theorem :: CONVEX1:25

    for V be RealLinearSpace, v1,v2 be VECTOR of V, L be Linear_Combination of {v1, v2} st v1 <> v2 & L is convex holds ((L . v1) + (L . v2)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & ( Sum L) = (((L . v1) * v1) + ((L . v2) * v2))

    proof

      let V be RealLinearSpace;

      let v1,v2 be VECTOR of V;

      let L be Linear_Combination of {v1, v2};

      assume that

       A1: v1 <> v2 and

       A2: L is convex;

      

       A3: ( Carrier L) c= {v1, v2} & ( Carrier L) <> {} by A2, Th21, RLVECT_2:def 6;

      now

        per cases by A3, ZFMISC_1: 36;

          suppose

           A4: ( Carrier L) = {v1};

          then not v2 in ( Carrier L) by A1, TARSKI:def 1;

          then not v2 in { v where v be Element of V : (L . v) <> 0 } by RLVECT_2:def 4;

          then (L . v2) = 0 ;

          hence ((L . v1) + (L . v2)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 by A2, A4, Lm11;

        end;

          suppose

           A5: ( Carrier L) = {v2};

          then not v1 in ( Carrier L) by A1, TARSKI:def 1;

          then not v1 in { v where v be Element of V : (L . v) <> 0 } by RLVECT_2:def 4;

          then (L . v1) = 0 ;

          hence ((L . v1) + (L . v2)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 by A2, A5, Lm11;

        end;

          suppose ( Carrier L) = {v1, v2};

          hence ((L . v1) + (L . v2)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 by A1, A2, Lm12;

        end;

      end;

      hence thesis by A1, RLVECT_2: 33;

    end;

    theorem :: CONVEX1:26

    for V be RealLinearSpace, v1,v2,v3 be VECTOR of V, L be Linear_Combination of {v1, v2, v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 & L is convex holds (((L . v1) + (L . v2)) + (L . v3)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & (L . v3) >= 0 & ( Sum L) = ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3))

    proof

      let V be RealLinearSpace, v1,v2,v3 be VECTOR of V, L be Linear_Combination of {v1, v2, v3};

      assume that

       A1: v1 <> v2 and

       A2: v2 <> v3 and

       A3: v3 <> v1 and

       A4: L is convex;

      

       A5: ( Carrier L) c= {v1, v2, v3} & ( Carrier L) <> {} by A4, Th21, RLVECT_2:def 6;

      now

        per cases by A5, ZFMISC_1: 118;

          suppose

           A6: ( Carrier L) = {v1};

          then not v3 in ( Carrier L) by A3, TARSKI:def 1;

          then not v3 in { v where v be Element of V : (L . v) <> 0 } by RLVECT_2:def 4;

          then

           A7: (L . v3) = 0 ;

           not v2 in ( Carrier L) by A1, A6, TARSKI:def 1;

          then not v2 in { v where v be Element of V : (L . v) <> 0 } by RLVECT_2:def 4;

          then (L . v2) = 0 ;

          hence (((L . v1) + (L . v2)) + (L . v3)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & (L . v3) >= 0 by A4, A6, A7, Lm11;

        end;

          suppose

           A8: ( Carrier L) = {v2};

          then not v3 in ( Carrier L) by A2, TARSKI:def 1;

          then not v3 in { v where v be Element of V : (L . v) <> 0 } by RLVECT_2:def 4;

          then

           A9: (L . v3) = 0 ;

           not v1 in ( Carrier L) by A1, A8, TARSKI:def 1;

          then not v1 in { v where v be Element of V : (L . v) <> 0 } by RLVECT_2:def 4;

          then (L . v1) = 0 ;

          hence (((L . v1) + (L . v2)) + (L . v3)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & (L . v3) >= 0 by A4, A8, A9, Lm11;

        end;

          suppose

           A10: ( Carrier L) = {v3};

          then not v2 in ( Carrier L) by A2, TARSKI:def 1;

          then not v2 in { v where v be Element of V : (L . v) <> 0 } by RLVECT_2:def 4;

          then

           A11: (L . v2) = 0 ;

           not v1 in ( Carrier L) by A3, A10, TARSKI:def 1;

          then not v1 in { v where v be Element of V : (L . v) <> 0 } by RLVECT_2:def 4;

          then (L . v1) = 0 ;

          hence (((L . v1) + (L . v2)) + (L . v3)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & (L . v3) >= 0 by A4, A10, A11, Lm11;

        end;

          suppose

           A12: ( Carrier L) = {v1, v2};

          then not v3 in ( Carrier L) by A2, A3, TARSKI:def 2;

          then not v3 in { v where v be Element of V : (L . v) <> 0 } by RLVECT_2:def 4;

          then (L . v3) = 0 ;

          hence (((L . v1) + (L . v2)) + (L . v3)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & (L . v3) >= 0 by A1, A4, A12, Lm12;

        end;

          suppose

           A13: ( Carrier L) = {v2, v3};

          then not v1 in ( Carrier L) by A1, A3, TARSKI:def 2;

          then not v1 in { v where v be Element of V : (L . v) <> 0 } by RLVECT_2:def 4;

          then (L . v1) = 0 ;

          hence (((L . v1) + (L . v2)) + (L . v3)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & (L . v3) >= 0 by A2, A4, A13, Lm12;

        end;

          suppose

           A14: ( Carrier L) = {v1, v3};

          then not v2 in ( Carrier L) by A1, A2, TARSKI:def 2;

          then not v2 in { v where v be Element of V : (L . v) <> 0 } by RLVECT_2:def 4;

          then (L . v2) = 0 ;

          hence (((L . v1) + (L . v2)) + (L . v3)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & (L . v3) >= 0 by A3, A4, A14, Lm12;

        end;

          suppose ( Carrier L) = {v1, v2, v3};

          hence (((L . v1) + (L . v2)) + (L . v3)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & (L . v3) >= 0 by A1, A2, A3, A4, Lm15;

        end;

      end;

      hence thesis by A1, A2, A3, Lm14;

    end;

    theorem :: CONVEX1:27

    for V be RealLinearSpace, v be VECTOR of V, L be Linear_Combination of V st L is convex & ( Carrier L) = {v} holds (L . v) = 1 by Lm11;

    theorem :: CONVEX1:28

    for V be RealLinearSpace, v1,v2 be VECTOR of V, L be Linear_Combination of V st L is convex & ( Carrier L) = {v1, v2} & v1 <> v2 holds ((L . v1) + (L . v2)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 by Lm12;

    theorem :: CONVEX1:29

    for V be RealLinearSpace, v1,v2,v3 be VECTOR of V, L be Linear_Combination of V st L is convex & ( Carrier L) = {v1, v2, v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds (((L . v1) + (L . v2)) + (L . v3)) = 1 & (L . v1) >= 0 & (L . v2) >= 0 & (L . v3) >= 0 & ( Sum L) = ((((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)) by Lm15;

    begin

    definition

      let V be non empty RLSStruct, M be Subset of V;

      :: CONVEX1:def4

      func Convex-Family M -> Subset-Family of V means

      : Def4: for N be Subset of V holds N in it iff N is convex & M c= N;

      existence

      proof

        defpred P[ Subset of V] means $1 is convex & M c= $1;

        thus ex F be Subset-Family of V st for N be Subset of V holds N in F iff P[N] from SUBSET_1:sch 3;

      end;

      uniqueness

      proof

        let SF,SG be Subset-Family of V;

        assume that

         A1: for N be Subset of V holds N in SF iff N is convex & M c= N and

         A2: for N be Subset of V holds N in SG iff N is convex & M c= N;

        for Y be Subset of V holds Y in SF iff Y in SG

        proof

          let Y be Subset of V;

          hereby

            assume Y in SF;

            then Y is convex & M c= Y by A1;

            hence Y in SG by A2;

          end;

          assume Y in SG;

          then Y is convex & M c= Y by A2;

          hence thesis by A1;

        end;

        hence thesis by SETFAM_1: 31;

      end;

    end

    definition

      let V be non empty RLSStruct, M be Subset of V;

      :: CONVEX1:def5

      func conv (M) -> convex Subset of V equals ( meet ( Convex-Family M));

      coherence

      proof

        for N be Subset of V st N in ( Convex-Family M) holds N is convex by Def4;

        hence thesis by Th15;

      end;

    end

    theorem :: CONVEX1:30

    for V be non empty RLSStruct, M be Subset of V, N be convex Subset of V st M c= N holds ( conv M) c= N

    proof

      let V be non empty RLSStruct;

      let M be Subset of V;

      let N be convex Subset of V;

      assume M c= N;

      then N in ( Convex-Family M) by Def4;

      hence thesis by SETFAM_1: 3;

    end;

    begin

    theorem :: CONVEX1:31

    for p be FinSequence, x,y,z be set st p is one-to-one & ( rng p) = {x, y, z} & x <> y & y <> z & z <> x holds p = <*x, y, z*> or p = <*x, z, y*> or p = <*y, x, z*> or p = <*y, z, x*> or p = <*z, x, y*> or p = <*z, y, x*> by Lm13;

    theorem :: CONVEX1:32

    for V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M be Subset of V holds (1 * M) = M by Lm1;

    theorem :: CONVEX1:33

    for V be non empty RLSStruct, M be empty Subset of V, r be Real holds (r * M) = {} by Lm7;

    theorem :: CONVEX1:34

    for V be RealLinearSpace, M be non empty Subset of V holds ( 0 * M) = {( 0. V)} by Lm2;

    theorem :: CONVEX1:35

    for V be right_zeroed non empty addLoopStr, M be Subset of V holds (M + {( 0. V)}) = M by Lm9;

    theorem :: CONVEX1:36

    for V be add-associative non empty addLoopStr, M1,M2,M3 be Subset of V holds ((M1 + M2) + M3) = (M1 + (M2 + M3)) by Lm3;

    theorem :: CONVEX1:37

    for V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M be Subset of V, r1,r2 be Real holds (r1 * (r2 * M)) = ((r1 * r2) * M) by Lm4;

    theorem :: CONVEX1:38

    for V be vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M1,M2 be Subset of V, r be Real holds (r * (M1 + M2)) = ((r * M1) + (r * M2)) by Lm5;

    theorem :: CONVEX1:39

    for V be non empty RLSStruct, M,N be Subset of V, r be Real st M c= N holds (r * M) c= (r * N) by Lm6;

    theorem :: CONVEX1:40

    for V be non empty addLoopStr, M be empty Subset of V, N be Subset of V holds (M + N) = {} by Lm8;

    begin

    registration

      let V be non empty RLSStruct, M,N be convex Subset of V;

      cluster (M /\ N) -> convex;

      coherence

      proof

        now

          let x,y be VECTOR of V;

          let r be Real;

          assume that

           A1: 0 < r & r < 1 and

           A2: x in (M /\ N) & y in (M /\ N);

          x in N & y in N by A2, XBOOLE_0:def 4;

          then

           A3: ((r * x) + ((1 - r) * y)) in N by A1, Def2;

          x in M & y in M by A2, XBOOLE_0:def 4;

          then ((r * x) + ((1 - r) * y)) in M by A1, Def2;

          hence ((r * x) + ((1 - r) * y)) in (M /\ N) by A3, XBOOLE_0:def 4;

        end;

        hence thesis;

      end;

    end

    registration

      let V be RealLinearSpace, M be Subset of V;

      cluster ( Convex-Family M) -> non empty;

      coherence

      proof

        

         A1: M c= ( Up ( (Omega). V))

        proof

          let x be object;

          assume x in M;

          then

          reconsider x as Element of V;

          x in the carrier of the RLSStruct of V;

          then x in the carrier of ( (Omega). V) by RLSUB_1:def 4;

          hence thesis by RUSUB_4:def 5;

        end;

        ( Up ( (Omega). V)) is convex by Th9;

        hence thesis by A1, Def4;

      end;

    end

    theorem :: CONVEX1:41

    for V be RealLinearSpace, M be Subset of V holds M c= ( conv M)

    proof

      let V be RealLinearSpace;

      let M be Subset of V;

      let v be object;

      assume

       A1: v in M;

      for Y be set holds Y in ( Convex-Family M) implies v in Y

      proof

        let Y be set;

        assume

         A2: Y in ( Convex-Family M);

        then

        reconsider Y as Subset of V;

        M c= Y by A2, Def4;

        hence thesis by A1;

      end;

      hence thesis by SETFAM_1:def 1;

    end;