:: CONVEX1 semantic presentation begin definition let V be non empty RLSStruct ; let M be Subset of V; let r be Real; funcr * M -> Subset of V equals :: CONVEX1:def 1 { (r * v) where v is Element of V : v in M } ; coherence { (r * v) where v is Element of V : v in M } is Subset of V proof deffunc H1( Element of V) -> Element of the carrier of V = r * $1; defpred S1[ set ] means $1 in M; { H1(v) where v is Element of V : S1[v] } is Subset of V from DOMAIN_1:sch_8(); hence { (r * v) where v is Element of V : v in M } is Subset of V ; ::_thesis: verum end; end; :: deftheorem defines * CONVEX1:def_1_:_ for V being non empty RLSStruct for M being Subset of V for r being Real holds r * M = { (r * v) where v is Element of V : v in M } ; definition let V be non empty RLSStruct ; let M be Subset of V; attrM is convex means :Def2: :: CONVEX1:def 2 for u, v being VECTOR of V for r being Real st 0 < r & r < 1 & u in M & v in M holds (r * u) + ((1 - r) * v) in M; end; :: deftheorem Def2 defines convex CONVEX1:def_2_:_ for V being non empty RLSStruct for M being Subset of V holds ( M is convex iff for u, v being VECTOR of V for r being Real st 0 < r & r < 1 & u in M & v in M holds (r * u) + ((1 - r) * v) in M ); theorem :: CONVEX1:1 for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct for M being Subset of V for r being Real st M is convex holds r * M is convex proof 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 proof 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, Def2; hence (p * u) + ((1 - p) * v) in r * M by A9; ::_thesis: verum end; hence r * M is convex by Def2; ::_thesis: verum end; theorem :: CONVEX1:2 for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct for M, N being Subset of V st M is convex & N is convex holds M + N is convex proof let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M, N being Subset of V st M is convex & N is convex holds M + N is convex let M, N be Subset of V; ::_thesis: ( M is convex & N is convex implies M + N is convex ) assume A1: ( M is convex & N is convex ) ; ::_thesis: M + N is convex for u, v being VECTOR of V for r being 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; ::_thesis: for r being Real st 0 < r & r < 1 & u in M + N & v in M + N holds (r * u) + ((1 - r) * v) in M + N let r be Real; ::_thesis: ( 0 < r & r < 1 & u in M + N & v in M + N implies (r * u) + ((1 - r) * v) in M + N ) assume that A2: ( 0 < r & r < 1 ) and A3: u in M + N and A4: v in M + N ; ::_thesis: (r * u) + ((1 - r) * v) in M + N v in { (x + y) where x, y is Element of V : ( x in M & y in N ) } by A4, RUSUB_4:def_9; then consider x2, y2 being Element of V such that A5: v = x2 + y2 and A6: ( x2 in M & y2 in N ) ; u in { (x + y) where x, y is Element of V : ( x in M & y in N ) } by A3, RUSUB_4:def_9; then consider x1, y1 being 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, Def2; then (r * u) + ((1 - r) * v) in { (x + y) where x, y is Element of V : ( x in M & y in N ) } by A9; hence (r * u) + ((1 - r) * v) in M + N by RUSUB_4:def_9; ::_thesis: verum end; hence M + N is convex by Def2; ::_thesis: verum end; theorem :: CONVEX1:3 for V being RealLinearSpace for M, N being Subset of V st M is convex & N is convex holds M - N is convex proof let V be RealLinearSpace; ::_thesis: for M, N being Subset of V st M is convex & N is convex holds M - N is convex let M, N be Subset of V; ::_thesis: ( M is convex & N is convex implies M - N is convex ) assume A1: ( M is convex & N is convex ) ; ::_thesis: M - N is convex for u, v being VECTOR of V for r being 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; ::_thesis: for r being Real st 0 < r & r < 1 & u in M - N & v in M - N holds (r * u) + ((1 - r) * v) in M - N let r be Real; ::_thesis: ( 0 < r & r < 1 & u in M - N & v in M - N implies (r * u) + ((1 - r) * v) in M - N ) assume that A2: ( 0 < r & r < 1 ) and A3: u in M - N and A4: v in M - N ; ::_thesis: (r * u) + ((1 - r) * v) in M - N v in { (x - y) where x, y is Element of V : ( x in M & y in N ) } by A4, RUSUB_5:def_2; then consider x2, y2 being Element of V such that A5: v = x2 - y2 and A6: ( x2 in M & y2 in N ) ; u in { (x - y) where x, y is Element of V : ( x in M & y in N ) } by A3, RUSUB_5:def_2; then consider x1, y1 being 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, Def2; then (r * u) + ((1 - r) * v) in { (x - y) where x, y is Element of V : ( x in M & y in N ) } by A9; hence (r * u) + ((1 - r) * v) in M - N by RUSUB_5:def_2; ::_thesis: verum end; hence M - N is convex by Def2; ::_thesis: verum end; theorem Th4: :: CONVEX1:4 for V being non empty RLSStruct for M being Subset of V holds ( M is convex iff for r being Real st 0 < r & r < 1 holds (r * M) + ((1 - r) * M) c= M ) proof let V be non empty RLSStruct ; ::_thesis: for M being Subset of V holds ( M is convex iff for r being Real st 0 < r & r < 1 holds (r * M) + ((1 - r) * M) c= M ) let M be Subset of V; ::_thesis: ( M is convex iff for r being Real st 0 < r & r < 1 holds (r * M) + ((1 - r) * M) c= M ) A1: ( M is convex implies for r being Real st 0 < r & r < 1 holds (r * M) + ((1 - r) * M) c= M ) proof assume A2: M is convex ; ::_thesis: for r being Real st 0 < r & r < 1 holds (r * M) + ((1 - r) * M) c= M let r be Real; ::_thesis: ( 0 < r & r < 1 implies (r * M) + ((1 - r) * M) c= M ) assume A3: ( 0 < r & r < 1 ) ; ::_thesis: (r * M) + ((1 - r) * M) c= M for x being Element of V st x in (r * M) + ((1 - r) * M) holds x in M proof let x be Element of V; ::_thesis: ( x in (r * M) + ((1 - r) * M) implies x in M ) assume x in (r * M) + ((1 - r) * M) ; ::_thesis: x in M then x in { (u + v) where u, v is Element of V : ( u in r * M & v in (1 - r) * M ) } by RUSUB_4:def_9; then consider u, v being Element of V such that A4: x = u + v and A5: ( u in r * M & v in (1 - r) * M ) ; ( ex w1 being Element of V st ( u = r * w1 & w1 in M ) & ex w2 being Element of V st ( v = (1 - r) * w2 & w2 in M ) ) by A5; hence x in M by A2, A3, A4, Def2; ::_thesis: verum end; hence (r * M) + ((1 - r) * M) c= M by SUBSET_1:2; ::_thesis: verum end; ( ( for r being Real st 0 < r & r < 1 holds (r * M) + ((1 - r) * M) c= M ) implies M is convex ) proof assume A6: for r being Real st 0 < r & r < 1 holds (r * M) + ((1 - r) * M) c= M ; ::_thesis: M is convex let u, v be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & u in M & v in M holds (r * u) + ((1 - r) * v) in M let r be Real; ::_thesis: ( 0 < r & r < 1 & u in M & v in M implies (r * u) + ((1 - r) * v) in M ) assume ( 0 < r & r < 1 ) ; ::_thesis: ( not u in M or not v in M or (r * u) + ((1 - r) * v) in M ) then A7: (r * M) + ((1 - r) * M) c= M by A6; assume ( u in M & v in M ) ; ::_thesis: (r * u) + ((1 - r) * v) in M then ( r * u in r * M & (1 - r) * v in { ((1 - r) * w) where w is Element of V : w in M } ) ; then (r * u) + ((1 - r) * v) in { (p + q) where p, q is 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 (r * u) + ((1 - r) * v) in M by A7; ::_thesis: verum end; hence ( M is convex iff for r being Real st 0 < r & r < 1 holds (r * M) + ((1 - r) * M) c= M ) by A1; ::_thesis: verum end; theorem :: CONVEX1:5 for V being non empty Abelian RLSStruct for M being Subset of V st M is convex holds for r being Real st 0 < r & r < 1 holds ((1 - r) * M) + (r * M) c= M proof let V be non empty Abelian RLSStruct ; ::_thesis: for M being Subset of V st M is convex holds for r being Real st 0 < r & r < 1 holds ((1 - r) * M) + (r * M) c= M let M be Subset of V; ::_thesis: ( M is convex implies for r being Real st 0 < r & r < 1 holds ((1 - r) * M) + (r * M) c= M ) assume A1: M is convex ; ::_thesis: for r being Real st 0 < r & r < 1 holds ((1 - r) * M) + (r * M) c= M let r be Real; ::_thesis: ( 0 < r & r < 1 implies ((1 - r) * M) + (r * M) c= M ) assume A2: ( 0 < r & r < 1 ) ; ::_thesis: ((1 - r) * M) + (r * M) c= M for x being Element of V st x in ((1 - r) * M) + (r * M) holds x in M proof let x be Element of V; ::_thesis: ( x in ((1 - r) * M) + (r * M) implies x in M ) assume x in ((1 - r) * M) + (r * M) ; ::_thesis: x in M then x in { (u + v) where u, v is Element of V : ( u in (1 - r) * M & v in r * M ) } by RUSUB_4:def_9; then consider u, v being Element of V such that A3: x = u + v and A4: ( u in (1 - r) * M & v in r * M ) ; ( ex w1 being Element of V st ( u = (1 - r) * w1 & w1 in M ) & ex w2 being Element of V st ( v = r * w2 & w2 in M ) ) by A4; hence x in M by A1, A2, A3, Def2; ::_thesis: verum end; hence ((1 - r) * M) + (r * M) c= M by SUBSET_1:2; ::_thesis: verum end; theorem :: CONVEX1:6 for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct for M, N being Subset of V st M is convex & N is convex holds for r being Real holds (r * M) + ((1 - r) * N) is convex proof let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M, N being Subset of V st M is convex & N is convex holds for r being Real holds (r * M) + ((1 - r) * N) is convex let M, N be Subset of V; ::_thesis: ( M is convex & N is convex implies for r being Real holds (r * M) + ((1 - r) * N) is convex ) assume that A1: M is convex and A2: N is convex ; ::_thesis: for r being Real holds (r * M) + ((1 - r) * N) is convex let r be Real; ::_thesis: (r * M) + ((1 - r) * N) is convex let u, v be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & u in (r * M) + ((1 - r) * N) & v in (r * M) + ((1 - r) * N) holds (r * u) + ((1 - r) * v) in (r * M) + ((1 - r) * N) let p be Real; ::_thesis: ( 0 < p & p < 1 & u in (r * M) + ((1 - r) * N) & v in (r * M) + ((1 - r) * N) implies (p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N) ) 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) ; ::_thesis: (p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N) A6: u in { (x1 + y1) where x1, y1 is 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 is VECTOR of V : ( x2 in r * M & y2 in (1 - r) * N ) } by A5, RUSUB_4:def_9; then consider x2, y2 being 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 being 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 being VECTOR of V such that A13: x2 = r * mx2 and A14: mx2 in M by A8; consider mx1 being 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 being VECTOR of V such that A18: y2 = (1 - r) * ny2 and A19: ny2 in N by A9; consider ny1 being 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, Def2; 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, Def2; then A24: (p * x1) + ((1 - p) * x2) in { (r * w) where w is 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 is VECTOR of V : ( w1 in r * M & w2 in (1 - r) * N ) } by A24, A23; hence (p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N) by RUSUB_4:def_9; ::_thesis: verum end; Lm1: for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct for M being Subset of V holds 1 * M = M proof let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M being Subset of V holds 1 * M = M let M be Subset of V; ::_thesis: 1 * M = M for v being Element of V st v in M holds v in 1 * M proof let v be Element of V; ::_thesis: ( v in M implies v in 1 * M ) A1: v = 1 * v by RLVECT_1:def_8; assume v in M ; ::_thesis: v in 1 * M hence v in 1 * M by A1; ::_thesis: verum end; then A2: M c= 1 * M by SUBSET_1:2; for v being Element of V st v in 1 * M holds v in M proof let v be Element of V; ::_thesis: ( v in 1 * M implies v in M ) assume v in 1 * M ; ::_thesis: v in M then ex x being Element of V st ( v = 1 * x & x in M ) ; hence v in M by RLVECT_1:def_8; ::_thesis: verum end; then 1 * M c= M by SUBSET_1:2; hence 1 * M = M by A2, XBOOLE_0:def_10; ::_thesis: verum end; Lm2: for V being RealLinearSpace for M being non empty Subset of V holds 0 * M = {(0. V)} proof let V be RealLinearSpace; ::_thesis: for M being non empty Subset of V holds 0 * M = {(0. V)} let M be non empty Subset of V; ::_thesis: 0 * M = {(0. V)} for v being Element of V st v in {(0. V)} holds v in 0 * M proof let v be Element of V; ::_thesis: ( v in {(0. V)} implies v in 0 * M ) consider x being set such that A1: x in M by XBOOLE_0:def_1; reconsider x = x as Element of V by A1; assume v in {(0. V)} ; ::_thesis: v in 0 * M then v = 0. V by TARSKI:def_1; then v = 0 * x by RLVECT_1:10; hence v in 0 * M by A1; ::_thesis: verum end; then A2: {(0. V)} c= 0 * M by SUBSET_1:2; for v being Element of V st v in 0 * M holds v in {(0. V)} proof let v be Element of V; ::_thesis: ( v in 0 * M implies v in {(0. V)} ) assume v in 0 * M ; ::_thesis: v in {(0. V)} then ex x being Element of V st ( v = 0 * x & x in M ) ; then v = 0. V by RLVECT_1:10; hence v in {(0. V)} by TARSKI:def_1; ::_thesis: verum end; then 0 * M c= {(0. V)} by SUBSET_1:2; hence 0 * M = {(0. V)} by A2, XBOOLE_0:def_10; ::_thesis: verum end; Lm3: for V being non empty add-associative addLoopStr for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3) proof let V be non empty add-associative addLoopStr ; ::_thesis: for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3) let M1, M2, M3 be Subset of V; ::_thesis: (M1 + M2) + M3 = M1 + (M2 + M3) for x being Element of V st x in M1 + (M2 + M3) holds x in (M1 + M2) + M3 proof let x be Element of V; ::_thesis: ( x in M1 + (M2 + M3) implies x in (M1 + M2) + M3 ) assume x in M1 + (M2 + M3) ; ::_thesis: x in (M1 + M2) + M3 then x in { (u + v) where u, v is Element of V : ( u in M1 & v in M2 + M3 ) } by RUSUB_4:def_9; then consider x1, x9 being 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 is Element of V : ( u in M2 & v in M3 ) } by A3, RUSUB_4:def_9; then consider x2, x3 being 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 is 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 is Element of V : ( u in M1 + M2 & v in M3 ) } by A6, A7; hence x in (M1 + M2) + M3 by RUSUB_4:def_9; ::_thesis: verum end; then A8: M1 + (M2 + M3) c= (M1 + M2) + M3 by SUBSET_1:2; for x being Element of V st x in (M1 + M2) + M3 holds x in M1 + (M2 + M3) proof let x be Element of V; ::_thesis: ( x in (M1 + M2) + M3 implies x in M1 + (M2 + M3) ) assume x in (M1 + M2) + M3 ; ::_thesis: x in M1 + (M2 + M3) then x in { (u + v) where u, v is Element of V : ( u in M1 + M2 & v in M3 ) } by RUSUB_4:def_9; then consider x9, x3 being 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 is Element of V : ( u in M1 & v in M2 ) } by A10, RUSUB_4:def_9; then consider x1, x2 being 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 is 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 is Element of V : ( u in M1 & v in M2 + M3 ) } by A13, A15; hence x in M1 + (M2 + M3) by RUSUB_4:def_9; ::_thesis: verum end; then (M1 + M2) + M3 c= M1 + (M2 + M3) by SUBSET_1:2; hence (M1 + M2) + M3 = M1 + (M2 + M3) by A8, XBOOLE_0:def_10; ::_thesis: verum end; Lm4: for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct for M being Subset of V for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M proof let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M being Subset of V for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M let M be Subset of V; ::_thesis: for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M let r1, r2 be Real; ::_thesis: r1 * (r2 * M) = (r1 * r2) * M for x being VECTOR of V st x in r1 * (r2 * M) holds x in (r1 * r2) * M proof let x be VECTOR of V; ::_thesis: ( x in r1 * (r2 * M) implies x in (r1 * r2) * M ) assume x in r1 * (r2 * M) ; ::_thesis: x in (r1 * r2) * M then consider w1 being VECTOR of V such that A1: x = r1 * w1 and A2: w1 in r2 * M ; consider w2 being 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 x in (r1 * r2) * M by A4; ::_thesis: verum end; then A5: r1 * (r2 * M) c= (r1 * r2) * M by SUBSET_1:2; for x being VECTOR of V st x in (r1 * r2) * M holds x in r1 * (r2 * M) proof let x be VECTOR of V; ::_thesis: ( x in (r1 * r2) * M implies x in r1 * (r2 * M) ) assume x in (r1 * r2) * M ; ::_thesis: x in r1 * (r2 * M) then consider w1 being 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 x in r1 * (r2 * M) ; ::_thesis: verum end; then (r1 * r2) * M c= r1 * (r2 * M) by SUBSET_1:2; hence r1 * (r2 * M) = (r1 * r2) * M by A5, XBOOLE_0:def_10; ::_thesis: verum end; Lm5: for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct for M1, M2 being Subset of V for r being Real holds r * (M1 + M2) = (r * M1) + (r * M2) proof let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M1, M2 being Subset of V for r being Real holds r * (M1 + M2) = (r * M1) + (r * M2) let M1, M2 be Subset of V; ::_thesis: for r being Real holds r * (M1 + M2) = (r * M1) + (r * M2) let r be Real; ::_thesis: r * (M1 + M2) = (r * M1) + (r * M2) for x being VECTOR of V st x in (r * M1) + (r * M2) holds x in r * (M1 + M2) proof let x be VECTOR of V; ::_thesis: ( x in (r * M1) + (r * M2) implies x in r * (M1 + M2) ) assume x in (r * M1) + (r * M2) ; ::_thesis: x in r * (M1 + M2) then x in { (u + v) where u, v is VECTOR of V : ( u in r * M1 & v in r * M2 ) } by RUSUB_4:def_9; then consider w1, w2 being VECTOR of V such that A1: x = w1 + w2 and A2: w1 in r * M1 and A3: w2 in r * M2 ; consider v2 being VECTOR of V such that A4: w2 = r * v2 and A5: v2 in M2 by A3; consider v1 being VECTOR of V such that A6: w1 = r * v1 and A7: v1 in M1 by A2; v1 + v2 in { (u + v) where u, v is 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 x in r * (M1 + M2) by A8; ::_thesis: verum end; then A9: (r * M1) + (r * M2) c= r * (M1 + M2) by SUBSET_1:2; for x being VECTOR of V st x in r * (M1 + M2) holds x in (r * M1) + (r * M2) proof let x be VECTOR of V; ::_thesis: ( x in r * (M1 + M2) implies x in (r * M1) + (r * M2) ) assume x in r * (M1 + M2) ; ::_thesis: x in (r * M1) + (r * M2) then consider w9 being VECTOR of V such that A10: x = r * w9 and A11: w9 in M1 + M2 ; w9 in { (u + v) where u, v is VECTOR of V : ( u in M1 & v in M2 ) } by A11, RUSUB_4:def_9; then consider w1, w2 being 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 is 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 is VECTOR of V : ( u in r * M1 & v in r * M2 ) } by A14; hence x in (r * M1) + (r * M2) by RUSUB_4:def_9; ::_thesis: verum end; then r * (M1 + M2) c= (r * M1) + (r * M2) by SUBSET_1:2; hence r * (M1 + M2) = (r * M1) + (r * M2) by A9, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: CONVEX1:7 for V being RealLinearSpace for M being Subset of V for v being VECTOR of V holds ( M is convex iff v + M is convex ) proof let V be RealLinearSpace; ::_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: ( v + M is convex implies M is convex ) proof assume A2: v + M is convex ; ::_thesis: M is convex let w1, w2 be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & w1 in M & w2 in M holds (r * w1) + ((1 - r) * w2) in M let r be Real; ::_thesis: ( 0 < r & r < 1 & w1 in M & w2 in M implies (r * w1) + ((1 - r) * w2) in M ) assume that A3: ( 0 < r & r < 1 ) and A4: w1 in M and A5: w2 in M ; ::_thesis: (r * w1) + ((1 - r) * w2) in M set x2 = v + w2; v + w2 in { (v + w) where w is VECTOR of V : w in M } by A5; then A6: v + w2 in v + M by RUSUB_4:def_8; set x1 = v + w1; A7: (r * (v + w1)) + ((1 - r) * (v + w2)) = ((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 ; v + w1 in { (v + w) where w is VECTOR of V : w in M } by A4; then v + w1 in v + M by RUSUB_4:def_8; then (r * (v + w1)) + ((1 - r) * (v + w2)) in v + M by A2, A3, A6, Def2; then v + ((r * w1) + ((1 - r) * w2)) in { (v + w) where w is VECTOR of V : w in M } by A7, RUSUB_4:def_8; then ex w being VECTOR of V st ( v + ((r * w1) + ((1 - r) * w2)) = v + w & w in M ) ; hence (r * w1) + ((1 - r) * w2) in M by RLVECT_1:8; ::_thesis: verum end; ( M is convex implies v + M is convex ) proof assume A8: M is convex ; ::_thesis: v + M is convex let w1, w2 be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & w1 in v + M & w2 in v + M holds (r * w1) + ((1 - r) * w2) in v + M let r be Real; ::_thesis: ( 0 < r & r < 1 & w1 in v + M & w2 in v + M implies (r * w1) + ((1 - r) * w2) in v + M ) assume that A9: ( 0 < r & r < 1 ) and A10: w1 in v + M and A11: w2 in v + M ; ::_thesis: (r * w1) + ((1 - r) * w2) in v + M w2 in { (v + w) where w is VECTOR of V : w in M } by A11, RUSUB_4:def_8; then consider x2 being VECTOR of V such that A12: w2 = v + x2 and A13: x2 in M ; w1 in { (v + w) where w is VECTOR of V : w in M } by A10, RUSUB_4:def_8; then consider x1 being 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, Def2; then (r * w1) + ((1 - r) * w2) in { (v + w) where w is VECTOR of V : w in M } by A16; hence (r * w1) + ((1 - r) * w2) in v + M by RUSUB_4:def_8; ::_thesis: verum end; hence ( M is convex iff v + M is convex ) by A1; ::_thesis: verum end; theorem :: CONVEX1:8 for V being RealLinearSpace holds Up ((0). V) is convex proof let V be RealLinearSpace; ::_thesis: Up ((0). V) is convex let u, v be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & u in Up ((0). V) & v in Up ((0). V) holds (r * u) + ((1 - r) * v) in Up ((0). V) let r be Real; ::_thesis: ( 0 < r & r < 1 & u in Up ((0). V) & v in Up ((0). V) implies (r * u) + ((1 - r) * v) in Up ((0). V) ) assume that 0 < r and r < 1 and A1: u in Up ((0). V) and A2: v in Up ((0). V) ; ::_thesis: (r * u) + ((1 - r) * 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, RLVECT_1:10 .= (0. V) + (0. V) by RLVECT_1:10 .= 0. V by RLVECT_1:4 ; 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 (r * u) + ((1 - r) * v) in Up ((0). V) by RUSUB_4:def_5; ::_thesis: verum end; theorem Th9: :: CONVEX1:9 for V being RealLinearSpace holds Up ((Omega). V) is convex proof let V be RealLinearSpace; ::_thesis: Up ((Omega). V) is convex let u, v be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & u in Up ((Omega). V) & v in Up ((Omega). V) holds (r * u) + ((1 - r) * v) in Up ((Omega). V) let r be Real; ::_thesis: ( 0 < r & r < 1 & u in Up ((Omega). V) & v in Up ((Omega). V) implies (r * u) + ((1 - r) * v) in Up ((Omega). V) ) (Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by RLSUB_1:def_4; then (r * u) + ((1 - r) * v) in the carrier of ((Omega). V) ; hence ( 0 < r & r < 1 & u in Up ((Omega). V) & v in Up ((Omega). V) implies (r * u) + ((1 - r) * v) in Up ((Omega). V) ) by RUSUB_4:def_5; ::_thesis: verum end; theorem Th10: :: CONVEX1:10 for V being non empty RLSStruct for M being Subset of V st M = {} holds M is convex proof let V be non empty RLSStruct ; ::_thesis: for M being Subset of V st M = {} holds M is convex let M be Subset of V; ::_thesis: ( M = {} implies M is convex ) A1: for u, v being VECTOR of V for r being Real st 0 < r & r < 1 & u in {} & v in {} holds (r * u) + ((1 - r) * v) in {} ; assume M = {} ; ::_thesis: M is convex hence M is convex by A1, Def2; ::_thesis: verum end; theorem Th11: :: CONVEX1:11 for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct for M1, M2 being Subset of V for r1, r2 being Real st M1 is convex & M2 is convex holds (r1 * M1) + (r2 * M2) is convex proof let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M1, M2 being Subset of V for r1, r2 being Real st M1 is convex & M2 is convex holds (r1 * M1) + (r2 * M2) is convex let M1, M2 be Subset of V; ::_thesis: for r1, r2 being Real st M1 is convex & M2 is convex holds (r1 * M1) + (r2 * M2) is convex let r1, r2 be Real; ::_thesis: ( M1 is convex & M2 is convex implies (r1 * M1) + (r2 * M2) is convex ) assume that A1: M1 is convex and A2: M2 is convex ; ::_thesis: (r1 * M1) + (r2 * M2) is convex let u, v be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & u in (r1 * M1) + (r2 * M2) & v in (r1 * M1) + (r2 * M2) holds (r * u) + ((1 - r) * v) in (r1 * M1) + (r2 * M2) let p be Real; ::_thesis: ( 0 < p & p < 1 & u in (r1 * M1) + (r2 * M2) & v in (r1 * M1) + (r2 * M2) implies (p * u) + ((1 - p) * v) in (r1 * M1) + (r2 * M2) ) assume that A3: ( 0 < p & p < 1 ) and A4: u in (r1 * M1) + (r2 * M2) and A5: v in (r1 * M1) + (r2 * M2) ; ::_thesis: (p * u) + ((1 - p) * v) in (r1 * M1) + (r2 * M2) v in { (x + y) where x, y is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) } by A5, RUSUB_4:def_9; then consider v1, v2 being 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 is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) } by A4, RUSUB_4:def_9; then consider u1, u2 being VECTOR of V such that A9: u = u1 + u2 and A10: u1 in r1 * M1 and A11: u2 in r2 * M2 ; consider y1 being VECTOR of V such that A12: v1 = r1 * y1 and A13: y1 in M1 by A7; consider x1 being 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 being VECTOR of V such that A17: v2 = r2 * y2 and A18: y2 in M2 by A8; consider x2 being 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, Def2; then A22: (p * u2) + ((1 - p) * v2) in r2 * M2 by A21; (p * x1) + ((1 - p) * y1) in M1 by A1, A3, A15, A13, Def2; then A23: (p * u1) + ((1 - p) * v1) in { (r1 * x) where x is 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 is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) } by A23, A22; hence (p * u) + ((1 - p) * v) in (r1 * M1) + (r2 * M2) by A9, A6, RUSUB_4:def_9; ::_thesis: verum end; theorem Th12: :: CONVEX1:12 for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct for M being Subset of V for r1, r2 being Real holds (r1 + r2) * M c= (r1 * M) + (r2 * M) proof let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M being Subset of V for r1, r2 being Real holds (r1 + r2) * M c= (r1 * M) + (r2 * M) let M be Subset of V; ::_thesis: for r1, r2 being Real holds (r1 + r2) * M c= (r1 * M) + (r2 * M) let r1, r2 be Real; ::_thesis: (r1 + r2) * M c= (r1 * M) + (r2 * M) for x being VECTOR of V st x in (r1 + r2) * M holds x in (r1 * M) + (r2 * M) proof let x be VECTOR of V; ::_thesis: ( x in (r1 + r2) * M implies x in (r1 * M) + (r2 * M) ) assume x in (r1 + r2) * M ; ::_thesis: x in (r1 * M) + (r2 * M) then consider w being VECTOR of V such that A1: x = (r1 + r2) * w and A2: w in M ; A3: r2 * w in { (r2 * u) where u is 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 is VECTOR of V : ( u in r1 * M & v in r2 * M ) } by A3; hence x in (r1 * M) + (r2 * M) by RUSUB_4:def_9; ::_thesis: verum end; hence (r1 + r2) * M c= (r1 * M) + (r2 * M) by SUBSET_1:2; ::_thesis: verum end; Lm6: for V being non empty RLSStruct for M, N being Subset of V for r being Real st M c= N holds r * M c= r * N proof let V be non empty RLSStruct ; ::_thesis: for M, N being Subset of V for r being Real st M c= N holds r * M c= r * N let M, N be Subset of V; ::_thesis: for r being Real st M c= N holds r * M c= r * N let r be Real; ::_thesis: ( M c= N implies r * M c= r * N ) assume A1: M c= N ; ::_thesis: r * M c= r * N for x being VECTOR of V st x in r * M holds x in r * N proof let x be VECTOR of V; ::_thesis: ( x in r * M implies x in r * N ) assume x in r * M ; ::_thesis: x in r * N then ex w being VECTOR of V st ( x = r * w & w in M ) ; hence x in r * N by A1; ::_thesis: verum end; hence r * M c= r * N by SUBSET_1:2; ::_thesis: verum end; Lm7: for V being non empty RLSStruct for M being empty Subset of V for r being Real holds r * M = {} proof let V be non empty RLSStruct ; ::_thesis: for M being empty Subset of V for r being Real holds r * M = {} let M be empty Subset of V; ::_thesis: for r being Real holds r * M = {} let r be Real; ::_thesis: r * M = {} for x being VECTOR of V st x in r * M holds x in {} proof let x be VECTOR of V; ::_thesis: ( x in r * M implies x in {} ) assume x in r * M ; ::_thesis: x in {} then ex v being VECTOR of V st ( x = r * v & v in {} ) ; hence x in {} ; ::_thesis: verum end; then r * M c= {} by SUBSET_1:2; hence r * M = {} ; ::_thesis: verum end; Lm8: for V being non empty addLoopStr for M being empty Subset of V for N being Subset of V holds M + N = {} proof let V be non empty addLoopStr ; ::_thesis: for M being empty Subset of V for N being Subset of V holds M + N = {} let M be empty Subset of V; ::_thesis: for N being Subset of V holds M + N = {} let N be Subset of V; ::_thesis: M + N = {} A1: M + N = { (u + v) where u, v is Element of V : ( u in {} & v in N ) } by RUSUB_4:def_9; for x being Element of V st x in M + N holds x in {} proof let x be Element of V; ::_thesis: ( x in M + N implies x in {} ) assume x in M + N ; ::_thesis: x in {} then ex u, v being Element of V st ( x = u + v & u in {} & v in N ) by A1; hence x in {} ; ::_thesis: verum end; then M + N c= {} by SUBSET_1:2; hence M + N = {} ; ::_thesis: verum end; Lm9: for V being non empty right_zeroed addLoopStr for M being Subset of V holds M + {(0. V)} = M proof let V be non empty right_zeroed addLoopStr ; ::_thesis: for M being Subset of V holds M + {(0. V)} = M let M be Subset of V; ::_thesis: M + {(0. V)} = M for x being Element of V st x in M + {(0. V)} holds x in M proof let x be Element of V; ::_thesis: ( x in M + {(0. V)} implies x in M ) assume x in M + {(0. V)} ; ::_thesis: x in M then x in { (u + v) where u, v is Element of V : ( u in M & v in {(0. V)} ) } by RUSUB_4:def_9; then consider u, v being 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 x in M by A1, RLVECT_1:def_4; ::_thesis: verum end; then A3: M + {(0. V)} c= M by SUBSET_1:2; for x being Element of V st x in M holds x in M + {(0. V)} proof let x be Element of V; ::_thesis: ( x in M implies x in M + {(0. V)} ) A4: ( x = x + (0. V) & 0. V in {(0. V)} ) by RLVECT_1:def_4, TARSKI:def_1; assume x in M ; ::_thesis: x in M + {(0. V)} then x in { (u + v) where u, v is Element of V : ( u in M & v in {(0. V)} ) } by A4; hence x in M + {(0. V)} by RUSUB_4:def_9; ::_thesis: verum end; then M c= M + {(0. V)} by SUBSET_1:2; hence M + {(0. V)} = M by A3, XBOOLE_0:def_10; ::_thesis: verum end; Lm10: for V being RealLinearSpace for M being Subset of V for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds (r1 * M) + (r2 * M) c= (r1 + r2) * M proof let V be RealLinearSpace; ::_thesis: for M being Subset of V for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds (r1 * M) + (r2 * M) c= (r1 + r2) * M let M be Subset of V; ::_thesis: for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds (r1 * M) + (r2 * M) c= (r1 + r2) * M let r1, r2 be Real; ::_thesis: ( r1 >= 0 & r2 >= 0 & M is convex implies (r1 * M) + (r2 * M) c= (r1 + r2) * M ) assume that A1: r1 >= 0 and A2: r2 >= 0 and A3: M is convex ; ::_thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M percases ( M is empty or not M is empty ) ; suppose M is empty ; ::_thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M then ( r1 * M = {} & (r1 + r2) * M = {} ) by Lm7; hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by Lm8; ::_thesis: verum end; supposeA4: not M is empty ; ::_thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M percases ( r1 = 0 or r2 = 0 or ( r1 <> 0 & r2 <> 0 ) ) ; supposeA5: r1 = 0 ; ::_thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M then r1 * M = {(0. V)} by A4, Lm2; hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by A5, Lm9; ::_thesis: verum end; supposeA6: r2 = 0 ; ::_thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M then r2 * M = {(0. V)} by A4, Lm2; hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by A6, Lm9; ::_thesis: verum end; supposeA7: ( r1 <> 0 & r2 <> 0 ) ; ::_thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M 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 (r1 * M) + (r2 * M) c= (r1 + r2) * M by A9, A10, Lm5; ::_thesis: verum end; end; end; end; end; theorem :: CONVEX1:13 for V being RealLinearSpace for M being Subset of V for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds (r1 * M) + (r2 * M) = (r1 + r2) * M proof let V be RealLinearSpace; ::_thesis: for M being Subset of V for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds (r1 * M) + (r2 * M) = (r1 + r2) * M let M be Subset of V; ::_thesis: for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds (r1 * M) + (r2 * M) = (r1 + r2) * M let r1, r2 be Real; ::_thesis: ( r1 >= 0 & r2 >= 0 & M is convex implies (r1 * M) + (r2 * M) = (r1 + r2) * M ) assume ( r1 >= 0 & r2 >= 0 & M is convex ) ; ::_thesis: (r1 * M) + (r2 * M) = (r1 + r2) * M hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by Lm10; :: according to XBOOLE_0:def_10 ::_thesis: (r1 + r2) * M c= (r1 * M) + (r2 * M) thus (r1 + r2) * M c= (r1 * M) + (r2 * M) by Th12; ::_thesis: verum end; theorem :: CONVEX1:14 for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct for M1, M2, M3 being Subset of V for r1, r2, r3 being Real st M1 is convex & M2 is convex & M3 is convex holds ((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex proof let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M1, M2, M3 being Subset of V for r1, r2, r3 being Real st M1 is convex & M2 is convex & M3 is convex holds ((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex let M1, M2, M3 be Subset of V; ::_thesis: for r1, r2, r3 being Real st M1 is convex & M2 is convex & M3 is convex holds ((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex let r1, r2, r3 be Real; ::_thesis: ( M1 is convex & M2 is convex & M3 is convex implies ((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex ) assume that A1: ( M1 is convex & M2 is convex ) and A2: M3 is convex ; ::_thesis: ((r1 * M1) + (r2 * M2)) + (r3 * 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 ((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex by Lm1; ::_thesis: verum end; theorem Th15: :: CONVEX1:15 for V being non empty RLSStruct for F being Subset-Family of V st ( for M being Subset of V st M in F holds M is convex ) holds meet F is convex proof let V be non empty RLSStruct ; ::_thesis: for F being Subset-Family of V st ( for M being Subset of V st M in F holds M is convex ) holds meet F is convex let F be Subset-Family of V; ::_thesis: ( ( for M being Subset of V st M in F holds M is convex ) implies meet F is convex ) assume A1: for M being Subset of V st M in F holds M is convex ; ::_thesis: meet F is convex percases ( F = {} or F <> {} ) ; suppose F = {} ; ::_thesis: meet F is convex then meet F = {} by SETFAM_1:def_1; hence meet F is convex by Th10; ::_thesis: verum end; supposeA2: F <> {} ; ::_thesis: meet F is convex meet F is convex proof let u, v be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & u in meet F & v in meet F holds (r * u) + ((1 - r) * v) in meet F let r be Real; ::_thesis: ( 0 < r & r < 1 & u in meet F & v in meet F implies (r * u) + ((1 - r) * v) in meet F ) assume that A3: ( 0 < r & r < 1 ) and A4: u in meet F and A5: v in meet F ; ::_thesis: (r * u) + ((1 - r) * v) in meet F for M being set st M in F holds (r * u) + ((1 - r) * v) in M proof let M be set ; ::_thesis: ( M in F implies (r * u) + ((1 - r) * v) in M ) assume A6: M in F ; ::_thesis: (r * u) + ((1 - r) * v) in M then reconsider M = 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 (r * u) + ((1 - r) * v) in M by A3, A7, Def2; ::_thesis: verum end; hence (r * u) + ((1 - r) * v) in meet F by A2, SETFAM_1:def_1; ::_thesis: verum end; hence meet F is convex ; ::_thesis: verum end; end; end; theorem Th16: :: CONVEX1:16 for V being non empty RLSStruct for M being Subset of V st M is Affine holds M is convex proof let V be non empty RLSStruct ; ::_thesis: for M being Subset of V st M is Affine holds M is convex let M be Subset of V; ::_thesis: ( M is Affine implies M is convex ) assume A1: M is Affine ; ::_thesis: M is convex let u, v be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & u in M & v in M holds (r * u) + ((1 - r) * v) in M let r be Real; ::_thesis: ( 0 < r & r < 1 & u in M & v in M implies (r * u) + ((1 - r) * v) in M ) assume that 0 < r and r < 1 and A2: ( u in M & v in M ) ; ::_thesis: (r * u) + ((1 - r) * v) in M set p = 1 - r; 1 - (1 - r) = r ; hence (r * u) + ((1 - r) * v) in M by A1, A2, RUSUB_4:def_4; ::_thesis: verum end; registration let V be non empty RLSStruct ; cluster non empty convex for Element of K10( the carrier of V); existence ex b1 being Subset of V st ( not b1 is empty & b1 is convex ) proof set M = the non empty Affine Subset of V; the non empty Affine Subset of V is convex by Th16; hence ex b1 being Subset of V st ( not b1 is empty & b1 is convex ) ; ::_thesis: verum end; end; registration let V be non empty RLSStruct ; cluster empty convex for Element of K10( the carrier of V); existence ex b1 being Subset of V st ( b1 is empty & b1 is convex ) proof {} V is convex by Th10; hence ex b1 being Subset of V st ( b1 is empty & b1 is convex ) ; ::_thesis: verum end; end; theorem :: CONVEX1:17 for V being non empty RealUnitarySpace-like UNITSTR for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : u .|. v >= r } holds M is convex proof let V be non empty RealUnitarySpace-like UNITSTR ; ::_thesis: for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : u .|. v >= r } holds M is convex let M be Subset of V; ::_thesis: for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : u .|. v >= r } holds M is convex let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : u .|. v >= r } holds M is convex let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : u .|. v >= r } implies M is convex ) assume A1: M = { u where u is VECTOR of V : u .|. v >= r } ; ::_thesis: M is convex let x, y be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & x in M & y in M holds (r * x) + ((1 - r) * y) in M let p be Real; ::_thesis: ( 0 < p & p < 1 & x in M & y in M implies (p * x) + ((1 - p) * y) in M ) assume that A2: 0 < p and A3: p < 1 and A4: x in M and A5: y in M ; ::_thesis: (p * x) + ((1 - p) * y) in M 0 + p < 1 by A3; then A6: 0 < 1 - p by XREAL_1:20; consider u2 being 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 being 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 (p * x) + ((1 - p) * y) in M by A1; ::_thesis: verum end; theorem :: CONVEX1:18 for V being non empty RealUnitarySpace-like UNITSTR for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : u .|. v > r } holds M is convex proof let V be non empty RealUnitarySpace-like UNITSTR ; ::_thesis: for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : u .|. v > r } holds M is convex let M be Subset of V; ::_thesis: for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : u .|. v > r } holds M is convex let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : u .|. v > r } holds M is convex let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : u .|. v > r } implies M is convex ) assume A1: M = { u where u is VECTOR of V : u .|. v > r } ; ::_thesis: M is convex let x, y be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & x in M & y in M holds (r * x) + ((1 - r) * y) in M let p be Real; ::_thesis: ( 0 < p & p < 1 & x in M & y in M implies (p * x) + ((1 - p) * y) in M ) assume that A2: 0 < p and A3: p < 1 and A4: x in M and A5: y in M ; ::_thesis: (p * x) + ((1 - p) * y) in M 0 + p < 1 by A3; then A6: 0 < 1 - p by XREAL_1:20; consider u2 being 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 being 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 (p * x) + ((1 - p) * y) in M by A1; ::_thesis: verum end; theorem :: CONVEX1:19 for V being non empty RealUnitarySpace-like UNITSTR for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : u .|. v <= r } holds M is convex proof let V be non empty RealUnitarySpace-like UNITSTR ; ::_thesis: for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : u .|. v <= r } holds M is convex let M be Subset of V; ::_thesis: for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : u .|. v <= r } holds M is convex let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : u .|. v <= r } holds M is convex let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : u .|. v <= r } implies M is convex ) assume A1: M = { u where u is VECTOR of V : u .|. v <= r } ; ::_thesis: M is convex let x, y be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & x in M & y in M holds (r * x) + ((1 - r) * y) in M let p be Real; ::_thesis: ( 0 < p & p < 1 & x in M & y in M implies (p * x) + ((1 - p) * y) in M ) assume that A2: 0 < p and A3: p < 1 and A4: x in M and A5: y in M ; ::_thesis: (p * x) + ((1 - p) * y) in M 0 + p < 1 by A3; then A6: 0 < 1 - p by XREAL_1:20; consider u2 being 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 being 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 (p * x) + ((1 - p) * y) in M by A1; ::_thesis: verum end; theorem :: CONVEX1:20 for V being non empty RealUnitarySpace-like UNITSTR for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : u .|. v < r } holds M is convex proof let V be non empty RealUnitarySpace-like UNITSTR ; ::_thesis: for M being Subset of V for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : u .|. v < r } holds M is convex let M be Subset of V; ::_thesis: for v being VECTOR of V for r being Real st M = { u where u is VECTOR of V : u .|. v < r } holds M is convex let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : u .|. v < r } holds M is convex let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : u .|. v < r } implies M is convex ) assume A1: M = { u where u is VECTOR of V : u .|. v < r } ; ::_thesis: M is convex let x, y be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & x in M & y in M holds (r * x) + ((1 - r) * y) in M let p be Real; ::_thesis: ( 0 < p & p < 1 & x in M & y in M implies (p * x) + ((1 - p) * y) in M ) assume that A2: 0 < p and A3: p < 1 and A4: x in M and A5: y in M ; ::_thesis: (p * x) + ((1 - p) * y) in M 0 + p < 1 by A3; then A6: 0 < 1 - p by XREAL_1:20; consider u2 being 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 being 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 (p * x) + ((1 - p) * y) in M by A1; ::_thesis: verum end; begin definition let V be RealLinearSpace; let L be Linear_Combination of V; attrL is convex means :Def3: :: CONVEX1:def 3 ex F being FinSequence of the carrier of V st ( F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) ) ) ); end; :: deftheorem Def3 defines convex CONVEX1:def_3_:_ for V being RealLinearSpace for L being Linear_Combination of V holds ( L is convex iff ex F being FinSequence of the carrier of V st ( F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) ) ) ) ); theorem Th21: :: CONVEX1:21 for V being RealLinearSpace for L being Linear_Combination of V st L is convex holds Carrier L <> {} proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V st L is convex holds Carrier L <> {} let L be Linear_Combination of V; ::_thesis: ( L is convex implies Carrier L <> {} ) assume L is convex ; ::_thesis: Carrier L <> {} then consider F being FinSequence of the carrier of V such that A1: ( F is one-to-one & rng F = Carrier L ) and A2: ex f being FinSequence of REAL st ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) ) ) by Def3; consider f being FinSequence of REAL such that A3: ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) ) ) by A2; assume Carrier L = {} ; ::_thesis: contradiction then len F = 0 by A1, CARD_1:27, FINSEQ_4:62; then f = <*> REAL by A3; hence contradiction by A3, RVSUM_1:72; ::_thesis: verum end; theorem :: CONVEX1:22 for V being RealLinearSpace for L being Linear_Combination of V for v being VECTOR of V st L is convex & L . v <= 0 holds not v in Carrier L proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V for v being VECTOR of V st L is convex & L . v <= 0 holds not v in Carrier L let L be Linear_Combination of V; ::_thesis: for v being VECTOR of V st L is convex & L . v <= 0 holds not v in Carrier L let v be VECTOR of V; ::_thesis: ( L is convex & L . v <= 0 implies not v in Carrier L ) assume that A1: L is convex and A2: L . v <= 0 ; ::_thesis: not v in Carrier L percases ( L . v = 0 or L . v < 0 ) by A2; suppose L . v = 0 ; ::_thesis: not v in Carrier L hence not v in Carrier L by RLVECT_2:19; ::_thesis: verum end; supposeA3: L . v < 0 ; ::_thesis: not v in Carrier L now__::_thesis:_not_v_in_Carrier_L consider F being FinSequence of the carrier of V such that F is one-to-one and A4: rng F = Carrier L and A5: ex f being FinSequence of REAL st ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) ) ) by A1, Def3; assume v in Carrier L ; ::_thesis: contradiction then consider n being set such that A6: n in dom F and A7: F . n = v by A4, FUNCT_1:def_3; reconsider n = n as Element of NAT by A6; consider f being FinSequence of REAL such that A8: len f = len F and Sum f = 1 and A9: for n being 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; ::_thesis: verum end; hence not v in Carrier L ; ::_thesis: verum end; end; end; theorem :: CONVEX1:23 for V being RealLinearSpace for L being Linear_Combination of V st L is convex holds L <> ZeroLC V proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V st L is convex holds L <> ZeroLC V let L be Linear_Combination of V; ::_thesis: ( L is convex implies L <> ZeroLC V ) assume L is convex ; ::_thesis: L <> ZeroLC V then A1: Carrier L <> {} by Th21; assume L = ZeroLC V ; ::_thesis: contradiction hence contradiction by A1, RLVECT_2:def_5; ::_thesis: verum end; Lm11: for V being RealLinearSpace for v being VECTOR of V for L being 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; ::_thesis: for v being VECTOR of V for L being Linear_Combination of V st L is convex & Carrier L = {v} holds ( L . v = 1 & Sum L = (L . v) * v ) let v be VECTOR of V; ::_thesis: for L being Linear_Combination of V st L is convex & Carrier L = {v} holds ( L . v = 1 & Sum L = (L . v) * v ) let L be Linear_Combination of V; ::_thesis: ( L is convex & Carrier L = {v} implies ( L . v = 1 & Sum L = (L . v) * v ) ) assume that A1: L is convex and A2: Carrier L = {v} ; ::_thesis: ( L . v = 1 & Sum L = (L . v) * v ) reconsider L = L as Linear_Combination of {v} by A2, RLVECT_2:def_6; consider F being FinSequence of the carrier of V such that A3: ( F is one-to-one & rng F = Carrier L ) and A4: ex f being FinSequence of REAL st ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) ) ) by A1, Def3; A5: F = <*v*> by A2, A3, FINSEQ_3:97; consider f being FinSequence of REAL such that A6: len f = len F and A7: Sum f = 1 and A8: for n being 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 ( L . v = 1 & Sum L = (L . v) * v ) by A7, A11, A12, A5, FINSEQ_1:def_8, RLVECT_2:32; ::_thesis: verum end; Lm12: for V being RealLinearSpace for v1, v2 being VECTOR of V for L being 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; ::_thesis: for v1, v2 being VECTOR of V for L being 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) ) let v1, v2 be VECTOR of V; ::_thesis: for L being 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) ) let L be Linear_Combination of V; ::_thesis: ( L is convex & Carrier L = {v1,v2} & v1 <> v2 implies ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) ) assume that A1: L is convex and A2: Carrier L = {v1,v2} and A3: v1 <> v2 ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) reconsider L = L as Linear_Combination of {v1,v2} by A2, RLVECT_2:def_6; consider F being FinSequence of the carrier of V such that A4: ( F is one-to-one & rng F = Carrier L ) and A5: ex f being FinSequence of REAL st ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) ) ) by A1, Def3; consider f being FinSequence of REAL such that A6: len f = len F and A7: Sum f = 1 and A8: for n being 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__::_thesis:_(_(L_._v1)_+_(L_._v2)_=_1_&_L_._v1_>=_0_&_L_._v2_>=_0_) percases ( F = <*v1,v2*> or F = <*v2,v1*> ) by A2, A3, A4, FINSEQ_3:99; suppose F = <*v1,v2*> ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) 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; ::_thesis: verum end; suppose F = <*v2,v1*> ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) 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; ::_thesis: verum end; end; end; hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) by A3, RLVECT_2:33; ::_thesis: verum end; Lm13: for p being FinSequence for x, y, z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x & not p = <*x,y,z*> & not p = <*x,z,y*> & not p = <*y,x,z*> & not p = <*y,z,x*> & not p = <*z,x,y*> holds p = <*z,y,x*> proof let p be FinSequence; ::_thesis: for x, y, z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x & not p = <*x,y,z*> & not p = <*x,z,y*> & not p = <*y,x,z*> & not p = <*y,z,x*> & not p = <*z,x,y*> holds p = <*z,y,x*> let x, y, z be set ; ::_thesis: ( p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x & not p = <*x,y,z*> & not p = <*x,z,y*> & not p = <*y,x,z*> & not p = <*y,z,x*> & not p = <*z,x,y*> implies p = <*z,y,x*> ) assume that A1: p is one-to-one and A2: rng p = {x,y,z} and A3: ( x <> y & y <> z & z <> x ) ; ::_thesis: ( 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*> ) 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 ( 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 A1, A4, A10, A6, A8, FINSEQ_1:45, FUNCT_1:def_4; ::_thesis: verum end; Lm14: for V being RealLinearSpace for v1, v2, v3 being VECTOR of V for L being 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; ::_thesis: for v1, v2, v3 being VECTOR of V for L being 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) let v1, v2, v3 be VECTOR of V; ::_thesis: for L being 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) let L be Linear_Combination of {v1,v2,v3}; ::_thesis: ( v1 <> v2 & v2 <> v3 & v3 <> v1 implies Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ) assume that A1: v1 <> v2 and A2: v2 <> v3 and A3: v3 <> v1 ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) A4: Carrier L c= {v1,v2,v3} by RLVECT_2:def_6; percases ( Carrier L = {} or Carrier L = {v1} or Carrier L = {v2} or Carrier L = {v3} or Carrier L = {v1,v2} or Carrier L = {v1,v3} or Carrier L = {v2,v3} or Carrier L = {v1,v2,v3} ) by A4, ZFMISC_1:118; suppose Carrier L = {} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) then A5: L = ZeroLC V by RLVECT_2:def_5; then Sum L = 0. V by RLVECT_2:30 .= (0. V) + (0. V) by RLVECT_1:4 .= ((0. V) + (0. V)) + (0. V) by RLVECT_1:4 .= ((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 Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; ::_thesis: verum end; supposeA6: Carrier L = {v1} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) then reconsider L = 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) by RLVECT_1:4 .= (((L . v1) * v1) + (0. V)) + (0. V) by RLVECT_1:4 .= (((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 Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; ::_thesis: verum end; supposeA9: Carrier L = {v2} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) then reconsider L = 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) by RLVECT_1:4 .= ((0. V) + ((L . v2) * v2)) + (0. V) by RLVECT_1:4 .= ((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 Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; ::_thesis: verum end; supposeA12: Carrier L = {v3} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) then reconsider L = 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) by RLVECT_1:4 .= ((0. V) + (0. V)) + ((L . v3) * v3) by RLVECT_1:4 .= ((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 Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; ::_thesis: verum end; supposeA15: Carrier L = {v1,v2} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) then A16: Sum L = ((L . v1) * v1) + ((L . v2) * v2) by A1, RLVECT_2:36 .= (((L . v1) * v1) + ((L . v2) * v2)) + (0. V) by RLVECT_1:4 .= (((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 Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A16, RLVECT_2:19; ::_thesis: verum end; supposeA17: Carrier L = {v1,v3} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) then A18: Sum L = ((L . v1) * v1) + ((L . v3) * v3) by A3, RLVECT_2:36 .= (((L . v1) * v1) + (0. V)) + ((L . v3) * v3) by RLVECT_1:4 .= (((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 Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A18, RLVECT_2:19; ::_thesis: verum end; supposeA19: Carrier L = {v2,v3} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) then A20: Sum L = ((L . v2) * v2) + ((L . v3) * v3) by A2, RLVECT_2:36 .= ((0. V) + ((L . v2) * v2)) + ((L . v3) * v3) by RLVECT_1:4 .= ((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 Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A20, RLVECT_2:19; ::_thesis: verum end; suppose Carrier L = {v1,v2,v3} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) then consider F being 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 Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by RLVECT_1:def_3; ::_thesis: verum end; end; end; Lm15: for V being RealLinearSpace for v1, v2, v3 being VECTOR of V for L being 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; ::_thesis: for v1, v2, v3 being VECTOR of V for L being 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) ) let v1, v2, v3 be VECTOR of V; ::_thesis: for L being 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) ) let L be Linear_Combination of V; ::_thesis: ( L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 implies ( ((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) ) ) assume that A1: L is convex and A2: Carrier L = {v1,v2,v3} and A3: ( v1 <> v2 & v2 <> v3 & v3 <> v1 ) ; ::_thesis: ( ((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) ) reconsider L = L as Linear_Combination of {v1,v2,v3} by A2, RLVECT_2:def_6; consider F being FinSequence of the carrier of V such that A4: ( F is one-to-one & rng F = Carrier L ) and A5: ex f being FinSequence of REAL st ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) ) ) by A1, Def3; consider f being FinSequence of REAL such that A6: len f = len F and A7: Sum f = 1 and A8: for n being 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__::_thesis:_(_((L_._v1)_+_(L_._v2))_+_(L_._v3)_=_1_&_L_._v1_>=_0_&_L_._v2_>=_0_&_L_._v3_>=_0_) percases ( 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 A2, A3, A4, Lm13; supposeA19: F = <*v1,v2,v3*> ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) 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; ::_thesis: verum end; supposeA21: F = <*v1,v3,v2*> ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) 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; ::_thesis: verum end; supposeA23: F = <*v2,v1,v3*> ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) 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; ::_thesis: verum end; supposeA25: F = <*v2,v3,v1*> ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) 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; ::_thesis: verum end; supposeA27: F = <*v3,v1,v2*> ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) 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; ::_thesis: verum end; supposeA29: F = <*v3,v2,v1*> ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) 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; ::_thesis: verum end; end; end; hence ( ((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 A3, Lm14; ::_thesis: verum end; theorem :: CONVEX1:24 for V being RealLinearSpace for v being VECTOR of V for L being Linear_Combination of {v} st L is convex holds ( L . v = 1 & Sum L = (L . v) * v ) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for L being Linear_Combination of {v} st L is convex holds ( L . v = 1 & Sum L = (L . v) * v ) let v be VECTOR of V; ::_thesis: for L being Linear_Combination of {v} st L is convex holds ( L . v = 1 & Sum L = (L . v) * v ) let L be Linear_Combination of {v}; ::_thesis: ( L is convex implies ( L . v = 1 & Sum L = (L . v) * 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 ; ::_thesis: ( L . v = 1 & Sum L = (L . v) * v ) hence ( L . v = 1 & Sum L = (L . v) * v ) by A1, Lm11, Th21; ::_thesis: verum end; theorem :: CONVEX1:25 for V being RealLinearSpace for v1, v2 being VECTOR of V for L being 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; ::_thesis: for v1, v2 being VECTOR of V for L being 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) ) let v1, v2 be VECTOR of V; ::_thesis: for L being 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) ) let L be Linear_Combination of {v1,v2}; ::_thesis: ( v1 <> v2 & L is convex implies ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) ) assume that A1: v1 <> v2 and A2: L is convex ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) A3: ( Carrier L c= {v1,v2} & Carrier L <> {} ) by A2, Th21, RLVECT_2:def_6; now__::_thesis:_(_(L_._v1)_+_(L_._v2)_=_1_&_L_._v1_>=_0_&_L_._v2_>=_0_) percases ( Carrier L = {v1} or Carrier L = {v2} or Carrier L = {v1,v2} ) by A3, ZFMISC_1:36; supposeA4: Carrier L = {v1} ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) then not v2 in Carrier L by A1, TARSKI:def_1; then not v2 in { v where v is 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; ::_thesis: verum end; supposeA5: Carrier L = {v2} ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) then not v1 in Carrier L by A1, TARSKI:def_1; then not v1 in { v where v is 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; ::_thesis: verum end; suppose Carrier L = {v1,v2} ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by A1, A2, Lm12; ::_thesis: verum end; end; end; hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) by A1, RLVECT_2:33; ::_thesis: verum end; theorem :: CONVEX1:26 for V being RealLinearSpace for v1, v2, v3 being VECTOR of V for L being 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; ::_thesis: for v1, v2, v3 being VECTOR of V for L being 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) ) let v1, v2, v3 be VECTOR of V; ::_thesis: for L being 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) ) let L be Linear_Combination of {v1,v2,v3}; ::_thesis: ( v1 <> v2 & v2 <> v3 & v3 <> v1 & L is convex implies ( ((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) ) ) assume that A1: v1 <> v2 and A2: v2 <> v3 and A3: v3 <> v1 and A4: L is convex ; ::_thesis: ( ((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) ) A5: ( Carrier L c= {v1,v2,v3} & Carrier L <> {} ) by A4, Th21, RLVECT_2:def_6; now__::_thesis:_(_((L_._v1)_+_(L_._v2))_+_(L_._v3)_=_1_&_L_._v1_>=_0_&_L_._v2_>=_0_&_L_._v3_>=_0_) percases ( Carrier L = {v1} or Carrier L = {v2} or Carrier L = {v3} or Carrier L = {v1,v2} or Carrier L = {v2,v3} or Carrier L = {v1,v3} or Carrier L = {v1,v2,v3} ) by A5, ZFMISC_1:118; supposeA6: Carrier L = {v1} ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) then not v3 in Carrier L by A3, TARSKI:def_1; then not v3 in { v where v is 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 is 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; ::_thesis: verum end; supposeA8: Carrier L = {v2} ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) then not v3 in Carrier L by A2, TARSKI:def_1; then not v3 in { v where v is 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 is 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; ::_thesis: verum end; supposeA10: Carrier L = {v3} ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) then not v2 in Carrier L by A2, TARSKI:def_1; then not v2 in { v where v is 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 is 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; ::_thesis: verum end; supposeA12: Carrier L = {v1,v2} ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) then not v3 in Carrier L by A2, A3, TARSKI:def_2; then not v3 in { v where v is 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; ::_thesis: verum end; supposeA13: Carrier L = {v2,v3} ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) then not v1 in Carrier L by A1, A3, TARSKI:def_2; then not v1 in { v where v is 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; ::_thesis: verum end; supposeA14: Carrier L = {v1,v3} ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) then not v2 in Carrier L by A1, A2, TARSKI:def_2; then not v2 in { v where v is 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; ::_thesis: verum end; suppose Carrier L = {v1,v2,v3} ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) hence ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) by A1, A2, A3, A4, Lm15; ::_thesis: verum end; end; end; hence ( ((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 A1, A2, A3, Lm14; ::_thesis: verum end; theorem :: CONVEX1:27 for V being RealLinearSpace for v being VECTOR of V for L being Linear_Combination of V st L is convex & Carrier L = {v} holds L . v = 1 by Lm11; theorem :: CONVEX1:28 for V being RealLinearSpace for v1, v2 being VECTOR of V for L being 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 being RealLinearSpace for v1, v2, v3 being VECTOR of V for L being 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 ; let M be Subset of V; func Convex-Family M -> Subset-Family of V means :Def4: :: CONVEX1:def 4 for N being Subset of V holds ( N in it iff ( N is convex & M c= N ) ); existence ex b1 being Subset-Family of V st for N being Subset of V holds ( N in b1 iff ( N is convex & M c= N ) ) proof defpred S1[ Subset of V] means ( $1 is convex & M c= $1 ); thus ex F being Subset-Family of V st for N being Subset of V holds ( N in F iff S1[N] ) from SUBSET_1:sch_3(); ::_thesis: verum end; uniqueness for b1, b2 being Subset-Family of V st ( for N being Subset of V holds ( N in b1 iff ( N is convex & M c= N ) ) ) & ( for N being Subset of V holds ( N in b2 iff ( N is convex & M c= N ) ) ) holds b1 = b2 proof let SF, SG be Subset-Family of V; ::_thesis: ( ( for N being Subset of V holds ( N in SF iff ( N is convex & M c= N ) ) ) & ( for N being Subset of V holds ( N in SG iff ( N is convex & M c= N ) ) ) implies SF = SG ) assume that A1: for N being Subset of V holds ( N in SF iff ( N is convex & M c= N ) ) and A2: for N being Subset of V holds ( N in SG iff ( N is convex & M c= N ) ) ; ::_thesis: SF = SG for Y being Subset of V holds ( Y in SF iff Y in SG ) proof let Y be Subset of V; ::_thesis: ( Y in SF iff Y in SG ) hereby ::_thesis: ( Y in SG implies Y in SF ) assume Y in SF ; ::_thesis: Y in SG then ( Y is convex & M c= Y ) by A1; hence Y in SG by A2; ::_thesis: verum end; assume Y in SG ; ::_thesis: Y in SF then ( Y is convex & M c= Y ) by A2; hence Y in SF by A1; ::_thesis: verum end; hence SF = SG by SETFAM_1:31; ::_thesis: verum end; end; :: deftheorem Def4 defines Convex-Family CONVEX1:def_4_:_ for V being non empty RLSStruct for M being Subset of V for b3 being Subset-Family of V holds ( b3 = Convex-Family M iff for N being Subset of V holds ( N in b3 iff ( N is convex & M c= N ) ) ); definition let V be non empty RLSStruct ; let M be Subset of V; func conv M -> convex Subset of V equals :: CONVEX1:def 5 meet (Convex-Family M); coherence meet (Convex-Family M) is convex Subset of V proof for N being Subset of V st N in Convex-Family M holds N is convex by Def4; hence meet (Convex-Family M) is convex Subset of V by Th15; ::_thesis: verum end; end; :: deftheorem defines conv CONVEX1:def_5_:_ for V being non empty RLSStruct for M being Subset of V holds conv M = meet (Convex-Family M); theorem :: CONVEX1:30 for V being non empty RLSStruct for M being Subset of V for N being convex Subset of V st M c= N holds conv M c= N proof let V be non empty RLSStruct ; ::_thesis: for M being Subset of V for N being convex Subset of V st M c= N holds conv M c= N let M be Subset of V; ::_thesis: for N being convex Subset of V st M c= N holds conv M c= N let N be convex Subset of V; ::_thesis: ( M c= N implies conv M c= N ) assume M c= N ; ::_thesis: conv M c= N then N in Convex-Family M by Def4; hence conv M c= N by SETFAM_1:3; ::_thesis: verum end; begin theorem :: CONVEX1:31 for p being FinSequence for x, y, z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x & not p = <*x,y,z*> & not p = <*x,z,y*> & not p = <*y,x,z*> & not p = <*y,z,x*> & not p = <*z,x,y*> holds p = <*z,y,x*> by Lm13; theorem :: CONVEX1:32 for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct for M being Subset of V holds 1 * M = M by Lm1; theorem :: CONVEX1:33 for V being non empty RLSStruct for M being empty Subset of V for r being Real holds r * M = {} by Lm7; theorem :: CONVEX1:34 for V being RealLinearSpace for M being non empty Subset of V holds 0 * M = {(0. V)} by Lm2; theorem :: CONVEX1:35 for V being non empty right_zeroed addLoopStr for M being Subset of V holds M + {(0. V)} = M by Lm9; theorem :: CONVEX1:36 for V being non empty add-associative addLoopStr for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3) by Lm3; theorem :: CONVEX1:37 for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct for M being Subset of V for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M by Lm4; theorem :: CONVEX1:38 for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct for M1, M2 being Subset of V for r being Real holds r * (M1 + M2) = (r * M1) + (r * M2) by Lm5; theorem :: CONVEX1:39 for V being non empty RLSStruct for M, N being Subset of V for r being Real st M c= N holds r * M c= r * N by Lm6; theorem :: CONVEX1:40 for V being non empty addLoopStr for M being empty Subset of V for N being Subset of V holds M + N = {} by Lm8; begin registration let V be non empty RLSStruct ; let M, N be convex Subset of V; clusterM /\ N -> convex for Subset of V; coherence for b1 being Subset of V st b1 = M /\ N holds b1 is convex proof now__::_thesis:_for_x,_y_being_VECTOR_of_V for_r_being_Real_st_0_<_r_&_r_<_1_&_x_in_M_/\_N_&_y_in_M_/\_N_holds_ (r_*_x)_+_((1_-_r)_*_y)_in_M_/\_N let x, y be VECTOR of V; ::_thesis: for r being Real st 0 < r & r < 1 & x in M /\ N & y in M /\ N holds (r * x) + ((1 - r) * y) in M /\ N let r be Real; ::_thesis: ( 0 < r & r < 1 & x in M /\ N & y in M /\ N implies (r * x) + ((1 - r) * y) in M /\ N ) assume that A1: ( 0 < r & r < 1 ) and A2: ( x in M /\ N & y in M /\ N ) ; ::_thesis: (r * x) + ((1 - r) * 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; ::_thesis: verum end; hence for b1 being Subset of V st b1 = M /\ N holds b1 is convex by Def2; ::_thesis: verum end; end; registration let V be RealLinearSpace; let M be Subset of V; cluster Convex-Family M -> non empty ; coherence not Convex-Family M is empty proof A1: M c= Up ((Omega). V) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in M or x in Up ((Omega). V) ) assume x in M ; ::_thesis: x in Up ((Omega). V) then reconsider x = x as Element of V ; x in the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ; then x in the carrier of ((Omega). V) by RLSUB_1:def_4; hence x in Up ((Omega). V) by RUSUB_4:def_5; ::_thesis: verum end; Up ((Omega). V) is convex by Th9; hence not Convex-Family M is empty by A1, Def4; ::_thesis: verum end; end; theorem :: CONVEX1:41 for V being RealLinearSpace for M being Subset of V holds M c= conv M proof let V be RealLinearSpace; ::_thesis: for M being Subset of V holds M c= conv M let M be Subset of V; ::_thesis: M c= conv M let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in M or v in conv M ) assume A1: v in M ; ::_thesis: v in conv M for Y being set st Y in Convex-Family M holds v in Y proof let Y be set ; ::_thesis: ( Y in Convex-Family M implies v in Y ) assume A2: Y in Convex-Family M ; ::_thesis: v in Y then reconsider Y = Y as Subset of V ; M c= Y by A2, Def4; hence v in Y by A1; ::_thesis: verum end; hence v in conv M by SETFAM_1:def_1; ::_thesis: verum end;