:: CONVEX3 semantic presentation begin definition let V be RealLinearSpace; defpred S1[ set ] means $1 is Convex_Combination of V; func ConvexComb V -> set means :Def1: :: CONVEX3:def 1 for L being set holds ( L in it iff L is Convex_Combination of V ); existence ex b1 being set st for L being set holds ( L in b1 iff L is Convex_Combination of V ) proof consider A being set such that A1: for x being set holds ( x in A iff ( x in Funcs ( the carrier of V,REAL) & S1[x] ) ) from XBOOLE_0:sch_1(); take A ; ::_thesis: for L being set holds ( L in A iff L is Convex_Combination of V ) let L be set ; ::_thesis: ( L in A iff L is Convex_Combination of V ) thus ( L in A implies L is Convex_Combination of V ) by A1; ::_thesis: ( L is Convex_Combination of V implies L in A ) assume L is Convex_Combination of V ; ::_thesis: L in A hence L in A by A1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for L being set holds ( L in b1 iff L is Convex_Combination of V ) ) & ( for L being set holds ( L in b2 iff L is Convex_Combination of V ) ) holds b1 = b2 proof thus for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum end; end; :: deftheorem Def1 defines ConvexComb CONVEX3:def_1_:_ for V being RealLinearSpace for b2 being set holds ( b2 = ConvexComb V iff for L being set holds ( L in b2 iff L is Convex_Combination of V ) ); definition let V be RealLinearSpace; let M be non empty Subset of V; defpred S1[ set ] means $1 is Convex_Combination of M; func ConvexComb M -> set means :: CONVEX3:def 2 for L being set holds ( L in it iff L is Convex_Combination of M ); existence ex b1 being set st for L being set holds ( L in b1 iff L is Convex_Combination of M ) proof consider A being set such that A1: for x being set holds ( x in A iff ( x in Funcs ( the carrier of V,REAL) & S1[x] ) ) from XBOOLE_0:sch_1(); take A ; ::_thesis: for L being set holds ( L in A iff L is Convex_Combination of M ) let L be set ; ::_thesis: ( L in A iff L is Convex_Combination of M ) thus ( L in A implies L is Convex_Combination of M ) by A1; ::_thesis: ( L is Convex_Combination of M implies L in A ) assume L is Convex_Combination of M ; ::_thesis: L in A hence L in A by A1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for L being set holds ( L in b1 iff L is Convex_Combination of M ) ) & ( for L being set holds ( L in b2 iff L is Convex_Combination of M ) ) holds b1 = b2 proof thus for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum end; end; :: deftheorem defines ConvexComb CONVEX3:def_2_:_ for V being RealLinearSpace for M being non empty Subset of V for b3 being set holds ( b3 = ConvexComb M iff for L being set holds ( L in b3 iff L is Convex_Combination of M ) ); theorem Th1: :: CONVEX3:1 for V being RealLinearSpace for v being VECTOR of V ex L being Convex_Combination of V st ( Sum L = v & ( for A being non empty Subset of V st v in A holds L is Convex_Combination of A ) ) proof let V be RealLinearSpace; ::_thesis: for v being VECTOR of V ex L being Convex_Combination of V st ( Sum L = v & ( for A being non empty Subset of V st v in A holds L is Convex_Combination of A ) ) let v be VECTOR of V; ::_thesis: ex L being Convex_Combination of V st ( Sum L = v & ( for A being non empty Subset of V st v in A holds L is Convex_Combination of A ) ) consider L being Linear_Combination of {v} such that A1: L . v = 1 by RLVECT_4:37; consider F being FinSequence of the carrier of V such that A2: ( F is one-to-one & rng F = Carrier L ) and Sum L = Sum (L (#) F) by RLVECT_2:def_8; v in Carrier L by A1, RLVECT_2:19; then ( Carrier L c= {v} & {v} c= Carrier L ) by RLVECT_2:def_6, ZFMISC_1:31; then A3: {v} = Carrier L by XBOOLE_0:def_10; then F = <*v*> by A2, FINSEQ_3:97; then A4: F . 1 = v by FINSEQ_1:def_8; deffunc H1( set ) -> set = L . (F . $1); consider f being FinSequence such that A5: ( len f = len F & ( for n being Nat st n in dom f holds f . n = H1(n) ) ) from FINSEQ_1:sch_2(); A6: len F = 1 by A3, A2, FINSEQ_3:96; then 1 in dom f by A5, FINSEQ_3:25; then A7: f . 1 = L . (F . 1) by A5; then f = <*1*> by A1, A5, A6, A4, FINSEQ_1:40; then rng f = {1} by FINSEQ_1:38; then rng f c= REAL by ZFMISC_1:31; then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4; A8: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) proof let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) ) assume A9: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 ) then n in Seg (len f) by FINSEQ_1:def_3; hence ( f . n = L . (F . n) & f . n >= 0 ) by A1, A5, A6, A7, A4, A9, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum end; f = <*1*> by A1, A5, A6, A7, A4, FINSEQ_1:40; then Sum f = 1 by FINSOP_1:11; then reconsider L = L as Convex_Combination of V by A2, A5, A8, CONVEX1:def_3; A10: for A being non empty Subset of V st v in A holds L is Convex_Combination of A proof let A be non empty Subset of V; ::_thesis: ( v in A implies L is Convex_Combination of A ) assume v in A ; ::_thesis: L is Convex_Combination of A then {v} c= A by ZFMISC_1:31; hence L is Convex_Combination of A by A3, RLVECT_2:def_6; ::_thesis: verum end; take L ; ::_thesis: ( Sum L = v & ( for A being non empty Subset of V st v in A holds L is Convex_Combination of A ) ) Sum L = 1 * v by A1, A3, RLVECT_2:35; hence ( Sum L = v & ( for A being non empty Subset of V st v in A holds L is Convex_Combination of A ) ) by A10, RLVECT_1:def_8; ::_thesis: verum end; theorem :: CONVEX3:2 for V being RealLinearSpace for v1, v2 being VECTOR of V st v1 <> v2 holds ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is Convex_Combination of A proof let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V st v1 <> v2 holds ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is Convex_Combination of A let v1, v2 be VECTOR of V; ::_thesis: ( v1 <> v2 implies ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is Convex_Combination of A ) assume A1: v1 <> v2 ; ::_thesis: ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is Convex_Combination of A consider L being Linear_Combination of {v1,v2} such that A2: ( L . v1 = 1 / 2 & L . v2 = 1 / 2 ) by A1, RLVECT_4:38; consider F being FinSequence of the carrier of V such that A3: ( F is one-to-one & rng F = Carrier L ) and Sum L = Sum (L (#) F) by RLVECT_2:def_8; deffunc H1( set ) -> set = L . (F . $1); consider f being FinSequence such that A4: ( len f = len F & ( for n being Nat st n in dom f holds f . n = H1(n) ) ) from FINSEQ_1:sch_2(); ( v1 in Carrier L & v2 in Carrier L ) by A2, RLVECT_2:19; then ( Carrier L c= {v1,v2} & {v1,v2} c= Carrier L ) by RLVECT_2:def_6, ZFMISC_1:32; then A5: {v1,v2} = Carrier L by XBOOLE_0:def_10; then A6: len F = 2 by A1, A3, FINSEQ_3:98; then 2 in dom f by A4, FINSEQ_3:25; then A7: f . 2 = L . (F . 2) by A4; 1 in dom f by A4, A6, FINSEQ_3:25; then A8: f . 1 = L . (F . 1) by A4; now__::_thesis:_ex_L,_L_being_Convex_Combination_of_V_st_ for_A_being_non_empty_Subset_of_V_st_{v1,v2}_c=_A_holds_ L_is_Convex_Combination_of_A percases ( F = <*v1,v2*> or F = <*v2,v1*> ) by A1, A5, A3, FINSEQ_3:99; suppose F = <*v1,v2*> ; ::_thesis: ex L, L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is Convex_Combination of A then A9: ( F . 1 = v1 & F . 2 = v2 ) by FINSEQ_1:44; then f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, FINSEQ_1:44; then f = <*(1 / 2)*> ^ <*(1 / 2)*> by FINSEQ_1:def_9; then rng f = (rng <*(1 / 2)*>) \/ (rng <*(1 / 2)*>) by FINSEQ_1:31 .= {(1 / 2)} by FINSEQ_1:38 ; then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4; A10: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) proof let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) ) assume A11: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 ) then n in Seg (len f) by FINSEQ_1:def_3; hence ( f . n = L . (F . n) & f . n >= 0 ) by A2, A4, A6, A8, A7, A9, A11, FINSEQ_1:2, TARSKI:def_2; ::_thesis: verum end; f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, A9, FINSEQ_1:44; then Sum f = (1 / 2) + (1 / 2) by RVSUM_1:77 .= 1 ; then reconsider L = L as Convex_Combination of V by A3, A4, A10, CONVEX1:def_3; take L = L; ::_thesis: ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is Convex_Combination of A for A being non empty Subset of V st {v1,v2} c= A holds L is Convex_Combination of A by A5, RLVECT_2:def_6; hence ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is Convex_Combination of A ; ::_thesis: verum end; suppose F = <*v2,v1*> ; ::_thesis: ex L, L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is Convex_Combination of A then A12: ( F . 1 = v2 & F . 2 = v1 ) by FINSEQ_1:44; then f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, FINSEQ_1:44; then f = <*(1 / 2)*> ^ <*(1 / 2)*> by FINSEQ_1:def_9; then rng f = (rng <*(1 / 2)*>) \/ (rng <*(1 / 2)*>) by FINSEQ_1:31 .= {(1 / 2)} by FINSEQ_1:38 ; then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4; A13: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) proof let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) ) assume A14: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 ) then n in Seg (len f) by FINSEQ_1:def_3; hence ( f . n = L . (F . n) & f . n >= 0 ) by A2, A4, A6, A8, A7, A12, A14, FINSEQ_1:2, TARSKI:def_2; ::_thesis: verum end; f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, A12, FINSEQ_1:44; then Sum f = (1 / 2) + (1 / 2) by RVSUM_1:77 .= 1 ; then reconsider L = L as Convex_Combination of V by A3, A4, A13, CONVEX1:def_3; take L = L; ::_thesis: ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is Convex_Combination of A for A being non empty Subset of V st {v1,v2} c= A holds L is Convex_Combination of A by A5, RLVECT_2:def_6; hence ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is Convex_Combination of A ; ::_thesis: verum end; end; end; hence ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2} c= A holds L is Convex_Combination of A ; ::_thesis: verum end; theorem :: CONVEX3:3 for V being RealLinearSpace for v1, v2, v3 being VECTOR of V st v1 <> v2 & v1 <> v3 & v2 <> v3 holds ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A proof let V be RealLinearSpace; ::_thesis: for v1, v2, v3 being VECTOR of V st v1 <> v2 & v1 <> v3 & v2 <> v3 holds ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A let v1, v2, v3 be VECTOR of V; ::_thesis: ( v1 <> v2 & v1 <> v3 & v2 <> v3 implies ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A ) assume that A1: v1 <> v2 and A2: v1 <> v3 and A3: v2 <> v3 ; ::_thesis: ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A consider L being Linear_Combination of {v1,v2,v3} such that A4: ( L . v1 = 1 / 3 & L . v2 = 1 / 3 & L . v3 = 1 / 3 ) by A1, A2, A3, RLVECT_4:39; consider F being FinSequence of the carrier of V such that A5: ( F is one-to-one & rng F = Carrier L ) and Sum L = Sum (L (#) F) by RLVECT_2:def_8; deffunc H1( set ) -> set = L . (F . $1); consider f being FinSequence such that A6: ( len f = len F & ( for n being Nat st n in dom f holds f . n = H1(n) ) ) from FINSEQ_1:sch_2(); for x being set st x in {v1,v2,v3} holds x in Carrier L proof let x be set ; ::_thesis: ( x in {v1,v2,v3} implies x in Carrier L ) assume A7: x in {v1,v2,v3} ; ::_thesis: x in Carrier L then reconsider x = x as VECTOR of V ; ( x = v1 or x = v2 or x = v3 ) by A7, ENUMSET1:def_1; hence x in Carrier L by A4, RLVECT_2:19; ::_thesis: verum end; then ( Carrier L c= {v1,v2,v3} & {v1,v2,v3} c= Carrier L ) by RLVECT_2:def_6, TARSKI:def_3; then A8: {v1,v2,v3} = Carrier L by XBOOLE_0:def_10; then A9: len F = 3 by A1, A2, A3, A5, FINSEQ_3:101; then 2 in dom f by A6, FINSEQ_3:25; then A10: f . 2 = L . (F . 2) by A6; 3 in dom f by A6, A9, FINSEQ_3:25; then A11: f . 3 = L . (F . 3) by A6; 1 in dom f by A6, A9, FINSEQ_3:25; then A12: f . 1 = L . (F . 1) by A6; now__::_thesis:_ex_L,_L_being_Convex_Combination_of_V_st_ for_A_being_non_empty_Subset_of_V_st_{v1,v2,v3}_c=_A_holds_ L_is_Convex_Combination_of_A 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 A1, A2, A3, A8, A5, CONVEX1:31; supposeA13: F = <*v1,v2,v3*> ; ::_thesis: ex L, L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A then A14: F . 3 = v3 by FINSEQ_1:45; A15: ( F . 1 = v1 & F . 2 = v2 ) by A13, FINSEQ_1:45; then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A14, FINSEQ_1:45; then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def_10; then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31 .= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31 .= {(1 / 3)} by FINSEQ_1:38 ; then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4; A16: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) proof let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) ) assume A17: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 ) then n in Seg (len f) by FINSEQ_1:def_3; hence ( f . n = L . (F . n) & f . n >= 0 ) by A4, A6, A9, A12, A10, A11, A15, A14, A17, ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: verum end; f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A15, A14, FINSEQ_1:45; then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78 .= 1 ; then reconsider L = L as Convex_Combination of V by A5, A6, A16, CONVEX1:def_3; take L = L; ::_thesis: ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A by A8, RLVECT_2:def_6; hence ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A ; ::_thesis: verum end; supposeA18: F = <*v1,v3,v2*> ; ::_thesis: ex L, L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A then A19: F . 3 = v2 by FINSEQ_1:45; A20: ( F . 1 = v1 & F . 2 = v3 ) by A18, FINSEQ_1:45; then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A19, FINSEQ_1:45; then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def_10; then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31 .= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31 .= {(1 / 3)} by FINSEQ_1:38 ; then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4; A21: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) proof let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) ) assume A22: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 ) then n in Seg (len f) by FINSEQ_1:def_3; hence ( f . n = L . (F . n) & f . n >= 0 ) by A4, A6, A9, A12, A10, A11, A20, A19, A22, ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: verum end; f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A20, A19, FINSEQ_1:45; then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78 .= 1 ; then reconsider L = L as Convex_Combination of V by A5, A6, A21, CONVEX1:def_3; take L = L; ::_thesis: ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A by A8, RLVECT_2:def_6; hence ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A ; ::_thesis: verum end; supposeA23: F = <*v2,v1,v3*> ; ::_thesis: ex L, L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A then A24: F . 3 = v3 by FINSEQ_1:45; A25: ( F . 1 = v2 & F . 2 = v1 ) by A23, FINSEQ_1:45; then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A24, FINSEQ_1:45; then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def_10; then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31 .= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31 .= {(1 / 3)} by FINSEQ_1:38 ; then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4; A26: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) proof let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) ) assume A27: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 ) then n in Seg (len f) by FINSEQ_1:def_3; hence ( f . n = L . (F . n) & f . n >= 0 ) by A4, A6, A9, A12, A10, A11, A25, A24, A27, ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: verum end; f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A25, A24, FINSEQ_1:45; then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78 .= 1 ; then reconsider L = L as Convex_Combination of V by A5, A6, A26, CONVEX1:def_3; take L = L; ::_thesis: ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A by A8, RLVECT_2:def_6; hence ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A ; ::_thesis: verum end; supposeA28: F = <*v2,v3,v1*> ; ::_thesis: ex L, L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A then A29: F . 3 = v1 by FINSEQ_1:45; A30: ( F . 1 = v2 & F . 2 = v3 ) by A28, FINSEQ_1:45; then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A29, FINSEQ_1:45; then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def_10; then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31 .= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31 .= {(1 / 3)} by FINSEQ_1:38 ; then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4; A31: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) proof let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) ) assume A32: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 ) then n in Seg (len f) by FINSEQ_1:def_3; hence ( f . n = L . (F . n) & f . n >= 0 ) by A4, A6, A9, A12, A10, A11, A30, A29, A32, ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: verum end; f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A30, A29, FINSEQ_1:45; then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78 .= 1 ; then reconsider L = L as Convex_Combination of V by A5, A6, A31, CONVEX1:def_3; take L = L; ::_thesis: ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A by A8, RLVECT_2:def_6; hence ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A ; ::_thesis: verum end; supposeA33: F = <*v3,v1,v2*> ; ::_thesis: ex L, L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A then A34: F . 3 = v2 by FINSEQ_1:45; A35: ( F . 1 = v3 & F . 2 = v1 ) by A33, FINSEQ_1:45; then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A34, FINSEQ_1:45; then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def_10; then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31 .= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31 .= {(1 / 3)} by FINSEQ_1:38 ; then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4; A36: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) proof let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) ) assume A37: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 ) then n in Seg (len f) by FINSEQ_1:def_3; hence ( f . n = L . (F . n) & f . n >= 0 ) by A4, A6, A9, A12, A10, A11, A35, A34, A37, ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: verum end; f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A35, A34, FINSEQ_1:45; then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78 .= 1 ; then reconsider L = L as Convex_Combination of V by A5, A6, A36, CONVEX1:def_3; take L = L; ::_thesis: ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A by A8, RLVECT_2:def_6; hence ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A ; ::_thesis: verum end; supposeA38: F = <*v3,v2,v1*> ; ::_thesis: ex L, L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A then A39: F . 3 = v1 by FINSEQ_1:45; A40: ( F . 1 = v3 & F . 2 = v2 ) by A38, FINSEQ_1:45; then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A39, FINSEQ_1:45; then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def_10; then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31 .= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31 .= {(1 / 3)} by FINSEQ_1:38 ; then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4; A41: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) proof let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) ) assume A42: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 ) then n in Seg (len f) by FINSEQ_1:def_3; hence ( f . n = L . (F . n) & f . n >= 0 ) by A4, A6, A9, A12, A10, A11, A40, A39, A42, ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: verum end; f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A40, A39, FINSEQ_1:45; then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78 .= 1 ; then reconsider L = L as Convex_Combination of V by A5, A6, A41, CONVEX1:def_3; take L = L; ::_thesis: ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A by A8, RLVECT_2:def_6; hence ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A ; ::_thesis: verum end; end; end; hence ex L being Convex_Combination of V st for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A ; ::_thesis: verum end; Lm1: for V being RealLinearSpace for M being non empty Subset of V st { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M holds M is convex proof let V be RealLinearSpace; ::_thesis: for M being non empty Subset of V st { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M holds M is convex let M be non empty Subset of V; ::_thesis: ( { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M implies M is convex ) assume A1: { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M ; ::_thesis: M is convex 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 proof set S = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } ; let u, v be VECTOR of V; ::_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 A2: ( 0 < r & r < 1 ) and A3: u in M and A4: v in M ; ::_thesis: (r * u) + ((1 - r) * v) in M consider Lv being Convex_Combination of V such that A5: Sum Lv = v and A6: for A being non empty Subset of V st v in A holds Lv is Convex_Combination of A by Th1; reconsider Lv = Lv as Convex_Combination of M by A4, A6; consider Lu being Convex_Combination of V such that A7: Sum Lu = u and A8: for A being non empty Subset of V st u in A holds Lu is Convex_Combination of A by Th1; reconsider Lu = Lu as Convex_Combination of M by A3, A8; A9: (r * u) + ((1 - r) * v) = (Sum (r * Lu)) + ((1 - r) * (Sum Lv)) by A7, A5, RLVECT_3:2 .= (Sum (r * Lu)) + (Sum ((1 - r) * Lv)) by RLVECT_3:2 .= Sum ((r * Lu) + ((1 - r) * Lv)) by RLVECT_3:1 ; A10: (r * Lu) + ((1 - r) * Lv) is Convex_Combination of M by A2, CONVEX2:9; then (r * Lu) + ((1 - r) * Lv) in ConvexComb V by Def1; then (r * u) + ((1 - r) * v) in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } by A9, A10; hence (r * u) + ((1 - r) * v) in M by A1; ::_thesis: verum end; hence M is convex by CONVEX1:def_2; ::_thesis: verum end; Lm2: for V being RealLinearSpace for M being non empty Subset of V for L being Convex_Combination of M st card (Carrier L) >= 2 holds ex L1, L2 being Convex_Combination of M ex r being Real st ( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 ) proof let V be RealLinearSpace; ::_thesis: for M being non empty Subset of V for L being Convex_Combination of M st card (Carrier L) >= 2 holds ex L1, L2 being Convex_Combination of M ex r being Real st ( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 ) let M be non empty Subset of V; ::_thesis: for L being Convex_Combination of M st card (Carrier L) >= 2 holds ex L1, L2 being Convex_Combination of M ex r being Real st ( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 ) let L be Convex_Combination of M; ::_thesis: ( card (Carrier L) >= 2 implies ex L1, L2 being Convex_Combination of M ex r being Real st ( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 ) ) consider F being FinSequence of the carrier of V such that A1: F is one-to-one and A2: rng F = Carrier L and A3: 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 CONVEX1:def_3; A4: for n, m being Element of NAT st 1 <= n & n < m & m <= len F holds F . n <> F . m proof let n, m be Element of NAT ; ::_thesis: ( 1 <= n & n < m & m <= len F implies F . n <> F . m ) assume that A5: 1 <= n and A6: n < m and A7: m <= len F ; ::_thesis: F . n <> F . m n <= len F by A6, A7, XXREAL_0:2; then n in Seg (len F) by A5, FINSEQ_1:1; then A8: n in dom F by FINSEQ_1:def_3; 1 <= m by A5, A6, XXREAL_0:2; then m in Seg (len F) by A7, FINSEQ_1:1; then A9: m in dom F by FINSEQ_1:def_3; assume F . n = F . m ; ::_thesis: contradiction hence contradiction by A1, A6, A8, A9, FUNCT_1:def_4; ::_thesis: verum end; assume A10: card (Carrier L) >= 2 ; ::_thesis: ex L1, L2 being Convex_Combination of M ex r being Real st ( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 ) then A11: len F >= 2 by A2, A4, GRAPH_5:7; then consider i being Nat such that A12: len F = i + 1 by NAT_1:6; set v = F . (len F); A13: Carrier L c= M by RLVECT_2:def_6; 1 <= len F by A11, XXREAL_0:2; then A14: len F in dom F by FINSEQ_3:25; then A15: F . (len F) in rng F by FUNCT_1:3; rng F c= the carrier of V by FINSEQ_1:def_4; then reconsider v = F . (len F) as VECTOR of V by A15; A16: F . (len F) in rng F by A14, FUNCT_1:3; reconsider i = i as Element of NAT by ORDINAL1:def_12; consider f being FinSequence of REAL such that A17: len f = len F and A18: Sum f = 1 and A19: for n being Nat st n in dom f holds ( f . n = L . (F . n) & f . n >= 0 ) by A3; 1 <= len f by A17, A11, XXREAL_0:2; then A20: 1 in Seg (len f) by FINSEQ_1:1; then A21: 1 in dom f by FINSEQ_1:def_3; 1 in dom F by A17, A20, FINSEQ_1:def_3; then F . 1 in rng F by FUNCT_1:3; then A22: L . (F . 1) <> 0 by A2, RLVECT_2:19; A23: for k being Nat st k in dom (f | i) holds 0 <= (f | i) . k proof A24: dom (f | i) c= dom f by FINSEQ_5:18; let k be Nat; ::_thesis: ( k in dom (f | i) implies 0 <= (f | i) . k ) assume A25: k in dom (f | i) ; ::_thesis: 0 <= (f | i) . k f | i = f | (Seg i) by FINSEQ_1:def_15; then (f | i) . k = f . k by A25, FUNCT_1:47; hence 0 <= (f | i) . k by A19, A25, A24; ::_thesis: verum end; len F >= 1 + 1 by A10, A2, A4, GRAPH_5:7; then (len F) - 1 >= 1 by XREAL_1:19; then 1 in Seg i by A12, FINSEQ_1:1; then A26: 1 in dom (f | (Seg i)) by A21, RELAT_1:57; f | i = f | (Seg i) by FINSEQ_1:def_15; then A27: (f | i) . 1 = f . 1 by A26, FUNCT_1:47 .= L . (F . 1) by A19, A21 ; A28: 1 in dom (f | i) by A26, FINSEQ_1:def_15; then (f | i) . 1 >= 0 by A23; then A29: Sum (f | i) > 0 by A23, A28, A27, A22, RVSUM_1:85; 1 <= len f by A17, A11, XXREAL_0:2; then len f in Seg (len f) by FINSEQ_1:1; then A30: len f in dom f by FINSEQ_1:def_3; then f . (len f) in rng f by FUNCT_1:3; then reconsider r = f . (len f) as Real ; A31: f = (f | i) ^ (f /^ i) by RFINSEQ:8; for n, m being Element of NAT st n in dom (F | i) & m in dom (F | i) & (F | i) /. n = (F | i) /. m holds n = m proof A32: dom (F | i) c= dom F by FINSEQ_5:18; let n, m be Element of NAT ; ::_thesis: ( n in dom (F | i) & m in dom (F | i) & (F | i) /. n = (F | i) /. m implies n = m ) assume that A33: n in dom (F | i) and A34: m in dom (F | i) and A35: (F | i) /. n = (F | i) /. m ; ::_thesis: n = m F /. n = (F | i) /. n by A33, FINSEQ_4:70 .= F /. m by A34, A35, FINSEQ_4:70 ; hence n = m by A1, A33, A34, A32, PARTFUN2:10; ::_thesis: verum end; then A36: F | i is one-to-one by PARTFUN2:9; reconsider B = {v} as non empty Subset of V ; consider L1 being Convex_Combination of V such that Sum L1 = v and A37: for A being non empty Subset of V st v in A holds L1 is Convex_Combination of A by Th1; A38: f = (f | i) ^ (f /^ i) by RFINSEQ:8; set r9 = 1 / (1 - r); defpred S1[ set , set ] means ( ( $1 in (rng F) \ {v} implies $2 = (1 / (1 - r)) * (L . $1) ) & ( not $1 in (rng F) \ {v} implies $2 = 0 ) ); A39: for x being set st x in the carrier of V holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in the carrier of V implies ex y being set st S1[x,y] ) assume x in the carrier of V ; ::_thesis: ex y being set st S1[x,y] ( x in (rng F) \ {v} or not x in (rng F) \ {v} ) ; hence ex y being set st S1[x,y] ; ::_thesis: verum end; consider L2 being Function such that A40: ( dom L2 = the carrier of V & ( for x being set st x in the carrier of V holds S1[x,L2 . x] ) ) from CLASSES1:sch_1(A39); for y being set st y in rng L2 holds y in REAL proof let y be set ; ::_thesis: ( y in rng L2 implies y in REAL ) assume y in rng L2 ; ::_thesis: y in REAL then consider x being set such that A41: x in dom L2 and A42: y = L2 . x by FUNCT_1:def_3; percases ( x in (rng F) \ {v} or not x in (rng F) \ {v} ) ; supposeA43: x in (rng F) \ {v} ; ::_thesis: y in REAL then x in rng F ; then reconsider x = x as VECTOR of V by A2; y = (1 / (1 - r)) * (L . x) by A40, A42, A43 .= ((1 / (1 - r)) * L) . x by RLVECT_2:def_11 ; hence y in REAL ; ::_thesis: verum end; suppose not x in (rng F) \ {v} ; ::_thesis: y in REAL then y = 0 by A40, A41, A42; hence y in REAL ; ::_thesis: verum end; end; end; then rng L2 c= REAL by TARSKI:def_3; then A44: L2 is Element of Funcs ( the carrier of V,REAL) by A40, FUNCT_2:def_2; ex T being finite Subset of V st for v being Element of V st not v in T holds L2 . v = 0 proof reconsider T = (Carrier L) \ {v} as finite Subset of V ; take T ; ::_thesis: for v being Element of V st not v in T holds L2 . v = 0 thus for v being Element of V st not v in T holds L2 . v = 0 by A2, A40; ::_thesis: verum end; then reconsider L2 = L2 as Linear_Combination of V by A44, RLVECT_2:def_3; for u being set st u in Carrier L2 holds u in (Carrier L) \ {v} proof let u be set ; ::_thesis: ( u in Carrier L2 implies u in (Carrier L) \ {v} ) assume A45: u in Carrier L2 ; ::_thesis: u in (Carrier L) \ {v} then reconsider u = u as Element of V ; L2 . u <> 0 by A45, RLVECT_2:19; hence u in (Carrier L) \ {v} by A2, A40; ::_thesis: verum end; then A46: Carrier L2 c= (Carrier L) \ {v} by TARSKI:def_3; f /^ i = <*(f /. (len f))*> by A17, A12, FINSEQ_5:30 .= <*(f . (len f))*> by A30, PARTFUN1:def_6 ; then A47: Sum f = (Sum (f | i)) + r by A31, RVSUM_1:74; then Sum (f | i) = 1 - r by A18; then A48: 1 > r + 0 by A29, XREAL_1:20; A49: 1 / (1 - r) > 0 by A18, A47, A29, XREAL_1:139; for u being set st u in (Carrier L) \ {v} holds u in Carrier L2 proof let u be set ; ::_thesis: ( u in (Carrier L) \ {v} implies u in Carrier L2 ) assume A50: u in (Carrier L) \ {v} ; ::_thesis: u in Carrier L2 then reconsider u = u as Element of V ; u in Carrier L by A50, XBOOLE_0:def_5; then A51: L . u <> 0 by RLVECT_2:19; L2 . u = (1 / (1 - r)) * (L . u) by A2, A40, A50; then L2 . u <> 0 by A49, A51, XCMPLX_1:6; hence u in Carrier L2 by RLVECT_2:19; ::_thesis: verum end; then (Carrier L) \ {v} c= Carrier L2 by TARSKI:def_3; then A52: Carrier L2 = (Carrier L) \ {v} by A46, XBOOLE_0:def_10; then Carrier L2 c= Carrier L by XBOOLE_1:36; then Carrier L2 c= M by A13, XBOOLE_1:1; then reconsider L2 = L2 as Linear_Combination of M by RLVECT_2:def_6; deffunc H1( set ) -> set = L2 . ((F | i) . $1); consider f2 being FinSequence such that A53: ( len f2 = len (F | i) & ( for k being Nat st k in dom f2 holds f2 . k = H1(k) ) ) from FINSEQ_1:sch_2(); F = (F | i) ^ (F /^ i) by RFINSEQ:8; then Carrier L = (rng (F | i)) \/ (rng (F /^ i)) by A2, FINSEQ_1:31; then A54: (Carrier L) \ (rng (F /^ i)) = rng (F | i) by A1, FINSEQ_5:34, XBOOLE_1:88; for y being set st y in rng f2 holds y in REAL proof let y be set ; ::_thesis: ( y in rng f2 implies y in REAL ) A55: ex L29 being Function st ( L2 = L29 & dom L29 = the carrier of V & rng L29 c= REAL ) by FUNCT_2:def_2; assume y in rng f2 ; ::_thesis: y in REAL then consider x being set such that A56: x in dom f2 and A57: y = f2 . x by FUNCT_1:def_3; A58: x in Seg (len f2) by A56, FINSEQ_1:def_3; reconsider x = x as Element of NAT by A56; x in dom (F | i) by A53, A58, FINSEQ_1:def_3; then (F | i) . x in rng (F | i) by FUNCT_1:3; then L2 . ((F | i) . x) in rng L2 by A54, A55, FUNCT_1:3; then L2 . ((F | i) . x) in REAL ; hence y in REAL by A53, A56, A57; ::_thesis: verum end; then rng f2 c= REAL by TARSKI:def_3; then reconsider f2 = f2 as FinSequence of REAL by FINSEQ_1:def_4; A59: dom f2 = Seg (len (F | i)) by A53, FINSEQ_1:def_3; then A60: dom f2 = Seg i by A12, FINSEQ_1:59, NAT_1:12 .= Seg (len (f | i)) by A17, A12, FINSEQ_1:59, NAT_1:12 .= dom (f | i) by FINSEQ_1:def_3 ; A61: (len F) - 1 = i by A12; A62: for k being Element of NAT st k in dom f2 holds ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 ) proof let k be Element of NAT ; ::_thesis: ( k in dom f2 implies ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 ) ) assume A63: k in dom f2 ; ::_thesis: ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 ) then A64: f2 . k = L2 . ((F | i) . k) by A53; k in dom (f | (Seg i)) by A60, A63, FINSEQ_1:def_15; then k in (dom f) /\ (Seg i) by RELAT_1:61; then A65: k in dom f by XBOOLE_0:def_4; A66: k in dom (F | i) by A59, A63, FINSEQ_1:def_3; then (F | i) . k in rng (F | i) by FUNCT_1:3; then reconsider w = (F | i) . k as Element of V by A54; A67: F | i = F | (Seg i) by FINSEQ_1:def_15; then A68: (F | i) . k = F . k by A66, FUNCT_1:47; A69: not w in {v} proof ( k <= len (F | i) & len (F | i) <= i ) by A59, A63, FINSEQ_1:1, FINSEQ_5:17; then k <= i by XXREAL_0:2; then A70: k + 1 <= len F by A61, XREAL_1:19; assume w in {v} ; ::_thesis: contradiction then A71: F . k = v by A68, TARSKI:def_1; dom (F | (Seg i)) c= dom F by RELAT_1:60; then k = len F by A1, A14, A66, A67, A71, FUNCT_1:def_4; hence contradiction by A70, NAT_1:13; ::_thesis: verum end; f | i = f | (Seg i) by FINSEQ_1:def_15; then A72: (f | i) . k = f . k by A60, A63, FUNCT_1:47; then A73: (f | i) . k = L . (F . k) by A19, A65; then A74: (f | i) . k = L . ((F | i) . k) by A66, A67, FUNCT_1:47; percases ( w in (rng F) \ {v} or not w in (rng F) \ {v} ) ; supposeA75: w in (rng F) \ {v} ; ::_thesis: ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 ) f . k >= 0 by A19, A65; then A76: (1 / (1 - r)) * ((f | i) . k) >= 0 by A18, A47, A29, A72; L2 . w = (1 / (1 - r)) * (L . w) by A40, A75 .= (1 / (1 - r)) * ((f | i) . k) by A73, A66, A67, FUNCT_1:47 .= ((1 / (1 - r)) * (f | i)) . k by RVSUM_1:44 ; hence ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 ) by A64, A76, RVSUM_1:44; ::_thesis: verum end; supposeA77: not w in (rng F) \ {v} ; ::_thesis: ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 ) then not w in rng F by A69, XBOOLE_0:def_5; then L . w = 0 by A2, RLVECT_2:19; then A78: (1 / (1 - r)) * ((f | i) . k) = 0 by A74; f2 . k = 0 by A40, A64, A77; hence ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 ) by A78, RVSUM_1:44; ::_thesis: verum end; end; end; then A79: for n being Nat st n in dom f2 holds ( f2 . n = L2 . ((F | i) . n) & f2 . n >= 0 ) by A53; f /^ i = <*(f /. (len f))*> by A17, A12, FINSEQ_5:30 .= <*(f . (len f))*> by A30, PARTFUN1:def_6 ; then A80: Sum f = (Sum (f | i)) + r by A38, RVSUM_1:74; F /^ i = <*(F /. (len F))*> by A12, FINSEQ_5:30 .= <*(F . (len F))*> by A14, PARTFUN1:def_6 ; then A81: rng (F | i) = Carrier L2 by A52, A54, FINSEQ_1:38; A82: for k being Nat st k in dom f2 holds f2 . k = ((1 / (1 - r)) * (f | i)) . k by A62; dom f2 = dom ((1 / (1 - r)) * (f | i)) by A60, VALUED_1:def_5; then f2 = (1 / (1 - r)) * (f | i) by A82, FINSEQ_1:13; then Sum f2 = (1 / (1 - r)) * (1 - r) by A18, A80, RVSUM_1:87 .= 1 / ((1 - r) / (1 - r)) by XCMPLX_1:81 .= 1 / 1 by A18, A47, A29, XCMPLX_1:60 .= 1 ; then reconsider L2 = L2 as Convex_Combination of M by A36, A81, A53, A79, CONVEX1:def_3; A83: v in Carrier L by A2, A14, FUNCT_1:3; then {v} c= Carrier L by ZFMISC_1:31; then A84: card (Carrier L2) = (card (Carrier L)) - (card {v}) by A52, CARD_2:44; Carrier L c= M by RLVECT_2:def_6; then reconsider L1 = L1 as Convex_Combination of M by A37, A83; v in {v} by TARSKI:def_1; then L1 is Convex_Combination of B by A37; then A85: Carrier L1 c= {v} by RLVECT_2:def_6; then A86: ( Carrier L1 = {} or Carrier L1 = {v} ) by ZFMISC_1:33; A87: for u being Element of V holds L . u = ((r * L1) + ((1 - r) * L2)) . u proof let u be Element of V; ::_thesis: L . u = ((r * L1) + ((1 - r) * L2)) . u A88: ((r * L1) + ((1 - r) * L2)) . u = ((r * L1) . u) + (((1 - r) * L2) . u) by RLVECT_2:def_10; percases ( u in Carrier L or not u in Carrier L ) ; supposeA89: u in Carrier L ; ::_thesis: L . u = ((r * L1) + ((1 - r) * L2)) . u percases ( u = v or u <> v ) ; supposeA90: u = v ; ::_thesis: L . u = ((r * L1) + ((1 - r) * L2)) . u then u in {v} by TARSKI:def_1; then not u in Carrier L2 by A46, XBOOLE_0:def_5; then L2 . u = 0 by RLVECT_2:19; then (1 - r) * (L2 . u) = 0 ; then A91: ((1 - r) * L2) . u = 0 by RLVECT_2:def_11; L1 . u = 1 by A86, A90, CONVEX1:21, CONVEX1:27; then A92: r * (L1 . u) = r ; L . u = r + 0 by A17, A19, A30, A90; hence L . u = ((r * L1) + ((1 - r) * L2)) . u by A88, A92, A91, RLVECT_2:def_11; ::_thesis: verum end; suppose u <> v ; ::_thesis: L . u = ((r * L1) + ((1 - r) * L2)) . u then A93: not u in Carrier L1 by A85, TARSKI:def_1; then L1 . u = 0 by RLVECT_2:19; then r * (L1 . u) = 0 ; then A94: (r * L1) . u = 0 by RLVECT_2:def_11; u in Carrier L2 by A52, A86, A89, A93, CONVEX1:21, XBOOLE_0:def_5; then L2 . u = (1 / (1 - r)) * (L . u) by A2, A40, A46; then (1 - r) * (L2 . u) = ((1 - r) * (1 / (1 - r))) * (L . u) .= (1 / ((1 - r) / (1 - r))) * (L . u) by XCMPLX_1:81 .= 1 * (L . u) by A18, A47, A29, XCMPLX_1:51 .= L . u ; hence L . u = ((r * L1) + ((1 - r) * L2)) . u by A88, A94, RLVECT_2:def_11; ::_thesis: verum end; end; end; supposeA95: not u in Carrier L ; ::_thesis: L . u = ((r * L1) + ((1 - r) * L2)) . u then not u in Carrier L1 by A2, A15, A85, TARSKI:def_1; then L1 . u = 0 by RLVECT_2:19; then r * (L1 . u) = 0 ; then A96: (r * L1) . u = 0 by RLVECT_2:def_11; not u in Carrier L2 by A46, A95, XBOOLE_0:def_5; then L2 . u = 0 by RLVECT_2:19; then A97: (1 - r) * (L2 . u) = 0 ; L . u = 0 + 0 by A95, RLVECT_2:19; hence L . u = ((r * L1) + ((1 - r) * L2)) . u by A88, A96, A97, RLVECT_2:def_11; ::_thesis: verum end; end; end; take L1 ; ::_thesis: ex L2 being Convex_Combination of M ex r being Real st ( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 ) take L2 ; ::_thesis: ex r being Real st ( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 ) take r ; ::_thesis: ( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 ) f . (len f) = L . (F . (len f)) by A19, A30; then r <> 0 by A2, A17, A16, RLVECT_2:19; hence ( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 ) by A19, A30, A48, A86, A87, A84, CARD_1:30, CONVEX1:21, RLVECT_2:def_9; ::_thesis: verum end; Lm3: for V being RealLinearSpace for M being non empty Subset of V st M is convex holds { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M proof let V be RealLinearSpace; ::_thesis: for M being non empty Subset of V st M is convex holds { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M let M be non empty Subset of V; ::_thesis: ( M is convex implies { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M ) set S = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } ; assume A1: M is convex ; ::_thesis: { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M for v being set st v in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } holds v in M proof let v be set ; ::_thesis: ( v in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } implies v in M ) assume v in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } ; ::_thesis: v in M then consider L being Convex_Combination of M such that A2: v = Sum L and L in ConvexComb V ; reconsider v = v as VECTOR of V by A2; percases ( card (Carrier L) < 2 or card (Carrier L) >= 2 ) ; supposeA3: card (Carrier L) < 2 ; ::_thesis: v in M Carrier L <> 0 by CONVEX1:21; then A4: card (Carrier L) >= 0 + 1 by NAT_1:13; card (Carrier L) < 1 + 1 by A3; then card (Carrier L) <= 1 by NAT_1:13; then card (Carrier L) = 1 by A4, XXREAL_0:1; then consider x being set such that A5: Carrier L = {x} by CARD_2:42; x in Carrier L by A5, TARSKI:def_1; then reconsider x = x as VECTOR of V ; A6: {x} c= M by A5, RLVECT_2:def_6; v = (L . x) * x by A2, A5, RLVECT_2:35 .= 1 * x by A5, CONVEX1:27 .= x by RLVECT_1:def_8 ; hence v in M by A6, ZFMISC_1:31; ::_thesis: verum end; supposeA7: card (Carrier L) >= 2 ; ::_thesis: v in M defpred S1[ Nat] means for LL being Convex_Combination of M st card (Carrier LL) = 1 + $1 & ex L1, L2 being Convex_Combination of M ex r being Real st ( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) holds Sum LL in M; A8: S1[1] proof let LL be Convex_Combination of M; ::_thesis: ( card (Carrier LL) = 1 + 1 & ex L1, L2 being Convex_Combination of M ex r being Real st ( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) implies Sum LL in M ) assume that A9: card (Carrier LL) = 1 + 1 and A10: ex L1, L2 being Convex_Combination of M ex r being Real st ( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) ; ::_thesis: Sum LL in M consider L1, L2 being Convex_Combination of M, r being Real such that A11: ( 0 < r & r < 1 ) and A12: LL = (r * L1) + ((1 - r) * L2) and A13: card (Carrier L1) = 1 and A14: card (Carrier L2) = (card (Carrier LL)) - 1 by A10; consider x2 being set such that A15: Carrier L2 = {x2} by A9, A14, CARD_2:42; x2 in Carrier L2 by A15, TARSKI:def_1; then reconsider x2 = x2 as VECTOR of V ; ( Sum L2 = (L2 . x2) * x2 & L2 . x2 = 1 ) by A15, CONVEX1:27, RLVECT_2:35; then A16: Sum L2 = x2 by RLVECT_1:def_8; {x2} c= M by A15, RLVECT_2:def_6; then A17: Sum L2 in M by A16, ZFMISC_1:31; consider x1 being set such that A18: Carrier L1 = {x1} by A13, CARD_2:42; x1 in Carrier L1 by A18, TARSKI:def_1; then reconsider x1 = x1 as VECTOR of V ; ( Sum L1 = (L1 . x1) * x1 & L1 . x1 = 1 ) by A18, CONVEX1:27, RLVECT_2:35; then A19: Sum L1 = x1 by RLVECT_1:def_8; {x1} c= M by A18, RLVECT_2:def_6; then A20: Sum L1 in M by A19, ZFMISC_1:31; Sum LL = (Sum (r * L1)) + (Sum ((1 - r) * L2)) by A12, RLVECT_3:1 .= (r * (Sum L1)) + (Sum ((1 - r) * L2)) by RLVECT_3:2 .= (r * (Sum L1)) + ((1 - r) * (Sum L2)) by RLVECT_3:2 ; hence Sum LL in M by A1, A11, A20, A17, CONVEX1:def_2; ::_thesis: verum end; consider k being Nat such that A21: card (Carrier L) = k + 1 by A7, NAT_1:6; reconsider k = k as non empty Element of NAT by A7, A21, ORDINAL1:def_12; A22: card (Carrier L) = 1 + k by A21; A23: ex L1, L2 being Convex_Combination of M ex r being Real st ( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 ) by A7, Lm2; A24: for k being non empty Nat st S1[k] holds S1[k + 1] proof let k be non empty Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A25: S1[k] ; ::_thesis: S1[k + 1] let LL be Convex_Combination of M; ::_thesis: ( card (Carrier LL) = 1 + (k + 1) & ex L1, L2 being Convex_Combination of M ex r being Real st ( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) implies Sum LL in M ) assume that A26: card (Carrier LL) = 1 + (k + 1) and A27: ex L1, L2 being Convex_Combination of M ex r being Real st ( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) ; ::_thesis: Sum LL in M consider L1, L2 being Convex_Combination of M, r being Real such that A28: ( 0 < r & r < 1 ) and A29: LL = (r * L1) + ((1 - r) * L2) and A30: card (Carrier L1) = 1 and A31: card (Carrier L2) = (card (Carrier LL)) - 1 by A27; k >= 0 + 1 by NAT_1:13; then k + 1 >= 1 + 1 by XREAL_1:6; then ex LL1, LL2 being Convex_Combination of M ex rr being Real st ( 0 < rr & rr < 1 & L2 = (rr * LL1) + ((1 - rr) * LL2) & card (Carrier LL1) = 1 & card (Carrier LL2) = (card (Carrier L2)) - 1 ) by A26, A31, Lm2; then A32: Sum L2 in M by A25, A26, A31; consider x1 being set such that A33: Carrier L1 = {x1} by A30, CARD_2:42; x1 in Carrier L1 by A33, TARSKI:def_1; then reconsider x1 = x1 as VECTOR of V ; ( Sum L1 = (L1 . x1) * x1 & L1 . x1 = 1 ) by A33, CONVEX1:27, RLVECT_2:35; then A34: Sum L1 = x1 by RLVECT_1:def_8; {x1} c= M by A33, RLVECT_2:def_6; then A35: Sum L1 in M by A34, ZFMISC_1:31; Sum LL = (Sum (r * L1)) + (Sum ((1 - r) * L2)) by A29, RLVECT_3:1 .= (r * (Sum L1)) + (Sum ((1 - r) * L2)) by RLVECT_3:2 .= (r * (Sum L1)) + ((1 - r) * (Sum L2)) by RLVECT_3:2 ; hence Sum LL in M by A1, A28, A35, A32, CONVEX1:def_2; ::_thesis: verum end; for k being non empty Nat holds S1[k] from NAT_1:sch_10(A8, A24); hence v in M by A2, A22, A23; ::_thesis: verum end; end; end; hence { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M by TARSKI:def_3; ::_thesis: verum end; theorem :: CONVEX3:4 for V being RealLinearSpace for M being non empty Subset of V holds ( M is convex iff { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M ) by Lm1, Lm3; theorem :: CONVEX3:5 for V being RealLinearSpace for M being non empty Subset of V holds conv M = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } proof let V be RealLinearSpace; ::_thesis: for M being non empty Subset of V holds conv M = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } let M be non empty Subset of V; ::_thesis: conv M = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } consider m being set such that A1: m in M by XBOOLE_0:def_1; reconsider m = m as VECTOR of V by A1; consider LL being Convex_Combination of V such that A2: Sum LL = m and A3: for A being non empty Subset of V st m in A holds LL is Convex_Combination of A by Th1; reconsider LL = LL as Convex_Combination of M by A1, A3; LL in ConvexComb V by Def1; then m in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } by A2; then reconsider N = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } as non empty set ; for x being set st x in N holds x in the carrier of V proof let x be set ; ::_thesis: ( x in N implies x in the carrier of V ) assume x in N ; ::_thesis: x in the carrier of V then ex L being Convex_Combination of M st ( x = Sum L & L in ConvexComb V ) ; hence x in the carrier of V ; ::_thesis: verum end; then reconsider N = N as Subset of V by TARSKI:def_3; for x being set st x in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } holds x in conv M proof let x be set ; ::_thesis: ( x in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } implies x in conv M ) assume x in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } ; ::_thesis: x in conv M then A4: ex L being Convex_Combination of M st ( x = Sum L & L in ConvexComb V ) ; M c= conv M by CONVEX1:41; hence x in conv M by A4, CONVEX2:6; ::_thesis: verum end; then A5: { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= conv M by TARSKI:def_3; for u, v being VECTOR of V for r being Real st 0 < r & r < 1 & u in N & v in N holds (r * u) + ((1 - r) * v) in N proof let u, v be VECTOR of V; ::_thesis: for r being Real st 0 < r & r < 1 & u in N & v in N holds (r * u) + ((1 - r) * v) in N let r be Real; ::_thesis: ( 0 < r & r < 1 & u in N & v in N implies (r * u) + ((1 - r) * v) in N ) assume that A6: ( 0 < r & r < 1 ) and A7: u in N and A8: v in N ; ::_thesis: (r * u) + ((1 - r) * v) in N consider Lv being Convex_Combination of M such that A9: v = Sum Lv and Lv in ConvexComb V by A8; consider Lu being Convex_Combination of M such that A10: u = Sum Lu and Lu in ConvexComb V by A7; reconsider LL = (r * Lu) + ((1 - r) * Lv) as Convex_Combination of M by A6, CONVEX2:9; (r * Lu) + ((1 - r) * Lv) is Convex_Combination of V by A6, CONVEX2:8; then A11: (r * Lu) + ((1 - r) * Lv) in ConvexComb V by Def1; Sum LL = (Sum (r * Lu)) + (Sum ((1 - r) * Lv)) by RLVECT_3:1 .= (r * (Sum Lu)) + (Sum ((1 - r) * Lv)) by RLVECT_3:2 .= (r * (Sum Lu)) + ((1 - r) * (Sum Lv)) by RLVECT_3:2 ; hence (r * u) + ((1 - r) * v) in N by A10, A9, A11; ::_thesis: verum end; then A12: N is convex by CONVEX1:def_2; for v being set st v in M holds v in N proof let v be set ; ::_thesis: ( v in M implies v in N ) assume A13: v in M ; ::_thesis: v in N then reconsider v = v as VECTOR of V ; consider LL being Convex_Combination of V such that A14: Sum LL = v and A15: for A being non empty Subset of V st v in A holds LL is Convex_Combination of A by Th1; reconsider LL = LL as Convex_Combination of M by A13, A15; LL in ConvexComb V by Def1; hence v in N by A14; ::_thesis: verum end; then M c= N by TARSKI:def_3; then conv M c= N by A12, CONVEX1:30; hence conv M = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } by A5, XBOOLE_0:def_10; ::_thesis: verum end; begin definition let V be non empty RLSStruct ; let M be Subset of V; attrM is cone means :Def3: :: CONVEX3:def 3 for r being Real for v being VECTOR of V st r > 0 & v in M holds r * v in M; end; :: deftheorem Def3 defines cone CONVEX3:def_3_:_ for V being non empty RLSStruct for M being Subset of V holds ( M is cone iff for r being Real for v being VECTOR of V st r > 0 & v in M holds r * v in M ); theorem Th6: :: CONVEX3:6 for V being non empty RLSStruct for M being Subset of V st M = {} holds M is cone proof let V be non empty RLSStruct ; ::_thesis: for M being Subset of V st M = {} holds M is cone let M be Subset of V; ::_thesis: ( M = {} implies M is cone ) A1: for r being Real for v being VECTOR of V st r > 0 & v in {} holds r * v in {} ; assume M = {} ; ::_thesis: M is cone hence M is cone by A1, Def3; ::_thesis: verum end; registration let V be non empty RLSStruct ; cluster cone for Element of K32( the carrier of V); existence ex b1 being Subset of V st b1 is cone proof {} V is cone by Th6; hence ex b1 being Subset of V st b1 is cone ; ::_thesis: verum end; end; registration let V be non empty RLSStruct ; cluster empty cone for Element of K32( the carrier of V); existence ex b1 being Subset of V st ( b1 is empty & b1 is cone ) proof set M = {} ; reconsider M = {} as Subset of V by XBOOLE_1:2; reconsider M = M as cone Subset of V by Th6; take M ; ::_thesis: ( M is empty & M is cone ) thus ( M is empty & M is cone ) ; ::_thesis: verum end; end; registration let V be RealLinearSpace; cluster non empty cone for Element of K32( the carrier of V); existence ex b1 being Subset of V st ( not b1 is empty & b1 is cone ) proof set M = {(0. V)}; reconsider M = {(0. V)} as Subset of V ; for r being Real for v being VECTOR of V st r > 0 & v in M holds r * v in M proof let r be Real; ::_thesis: for v being VECTOR of V st r > 0 & v in M holds r * v in M let v be VECTOR of V; ::_thesis: ( r > 0 & v in M implies r * v in M ) assume that r > 0 and A1: v in M ; ::_thesis: r * v in M v = 0. V by A1, TARSKI:def_1; then r * v = 0. V by RLVECT_1:10; hence r * v in M by TARSKI:def_1; ::_thesis: verum end; then reconsider M = M as cone Subset of V by Def3; take M ; ::_thesis: ( not M is empty & M is cone ) thus ( not M is empty & M is cone ) ; ::_thesis: verum end; end; theorem Th7: :: CONVEX3:7 for V being non empty RLSStruct for M being cone Subset of V st V is vector-distributive & V is scalar-distributive & V is scalar-associative & V is scalar-unital holds ( M is convex iff for u, v being VECTOR of V st u in M & v in M holds u + v in M ) proof let V be non empty RLSStruct ; ::_thesis: for M being cone Subset of V st V is vector-distributive & V is scalar-distributive & V is scalar-associative & V is scalar-unital holds ( M is convex iff for u, v being VECTOR of V st u in M & v in M holds u + v in M ) let M be cone Subset of V; ::_thesis: ( V is vector-distributive & V is scalar-distributive & V is scalar-associative & V is scalar-unital implies ( M is convex iff for u, v being VECTOR of V st u in M & v in M holds u + v in M ) ) A1: ( ( for u, v being VECTOR of V st u in M & v in M holds u + v in M ) implies M is convex ) proof assume A2: for u, v being VECTOR of V st u in M & v in M holds u + v in M ; ::_thesis: M is convex 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 proof let u, v be VECTOR of V; ::_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 A3: 0 < r and A4: r < 1 and A5: u in M and A6: v in M ; ::_thesis: (r * u) + ((1 - r) * v) in M r + 0 < 1 by A4; then 1 - r > 0 by XREAL_1:20; then A7: (1 - r) * v in M by A6, Def3; r * u in M by A3, A5, Def3; hence (r * u) + ((1 - r) * v) in M by A2, A7; ::_thesis: verum end; hence M is convex by CONVEX1:def_2; ::_thesis: verum end; assume A8: ( V is vector-distributive & V is scalar-distributive & V is scalar-associative & V is scalar-unital ) ; ::_thesis: ( M is convex iff for u, v being VECTOR of V st u in M & v in M holds u + v in M ) ( M is convex implies for u, v being VECTOR of V st u in M & v in M holds u + v in M ) proof assume A9: M is convex ; ::_thesis: for u, v being VECTOR of V st u in M & v in M holds u + v in M for u, v being VECTOR of V st u in M & v in M holds u + v in M proof let u, v be VECTOR of V; ::_thesis: ( u in M & v in M implies u + v in M ) assume ( u in M & v in M ) ; ::_thesis: u + v in M then ((1 / 2) * u) + ((1 - (1 / 2)) * v) in M by A9, CONVEX1:def_2; then A10: 2 * (((1 / 2) * u) + ((1 / 2) * v)) in M by Def3; 2 * (((1 / 2) * u) + ((1 / 2) * v)) = (2 * ((1 / 2) * u)) + (2 * ((1 / 2) * v)) by A8, RLVECT_1:def_5 .= ((2 * (1 / 2)) * u) + (2 * ((1 / 2) * v)) by A8, RLVECT_1:def_7 .= (1 * u) + ((2 * (1 / 2)) * v) by A8, RLVECT_1:def_7 .= u + (1 * v) by A8, RLVECT_1:def_8 ; hence u + v in M by A8, A10, RLVECT_1:def_8; ::_thesis: verum end; hence for u, v being VECTOR of V st u in M & v in M holds u + v in M ; ::_thesis: verum end; hence ( M is convex iff for u, v being VECTOR of V st u in M & v in M holds u + v in M ) by A1; ::_thesis: verum end; Lm4: for V being RealLinearSpace for M being Subset of V for L being Linear_Combination of M st card (Carrier L) >= 1 holds ex L1, L2 being Linear_Combination of M st ( Sum L = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 & Carrier L1 c= Carrier L & Carrier L2 c= Carrier L & ( for v being VECTOR of V st v in Carrier L1 holds L1 . v = L . v ) & ( for v being VECTOR of V st v in Carrier L2 holds L2 . v = L . v ) ) proof let V be RealLinearSpace; ::_thesis: for M being Subset of V for L being Linear_Combination of M st card (Carrier L) >= 1 holds ex L1, L2 being Linear_Combination of M st ( Sum L = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 & Carrier L1 c= Carrier L & Carrier L2 c= Carrier L & ( for v being VECTOR of V st v in Carrier L1 holds L1 . v = L . v ) & ( for v being VECTOR of V st v in Carrier L2 holds L2 . v = L . v ) ) let M be Subset of V; ::_thesis: for L being Linear_Combination of M st card (Carrier L) >= 1 holds ex L1, L2 being Linear_Combination of M st ( Sum L = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 & Carrier L1 c= Carrier L & Carrier L2 c= Carrier L & ( for v being VECTOR of V st v in Carrier L1 holds L1 . v = L . v ) & ( for v being VECTOR of V st v in Carrier L2 holds L2 . v = L . v ) ) let L be Linear_Combination of M; ::_thesis: ( card (Carrier L) >= 1 implies ex L1, L2 being Linear_Combination of M st ( Sum L = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 & Carrier L1 c= Carrier L & Carrier L2 c= Carrier L & ( for v being VECTOR of V st v in Carrier L1 holds L1 . v = L . v ) & ( for v being VECTOR of V st v in Carrier L2 holds L2 . v = L . v ) ) ) assume card (Carrier L) >= 1 ; ::_thesis: ex L1, L2 being Linear_Combination of M st ( Sum L = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 & Carrier L1 c= Carrier L & Carrier L2 c= Carrier L & ( for v being VECTOR of V st v in Carrier L1 holds L1 . v = L . v ) & ( for v being VECTOR of V st v in Carrier L2 holds L2 . v = L . v ) ) then Carrier L <> {} ; then consider u being set such that A1: u in Carrier L by XBOOLE_0:def_1; reconsider u = u as VECTOR of V by A1; consider L1 being Linear_Combination of {u} such that A2: L1 . u = L . u by RLVECT_4:37; A3: Carrier L1 c= {u} by RLVECT_2:def_6; Carrier L c= M by RLVECT_2:def_6; then {u} c= M by A1, ZFMISC_1:31; then Carrier L1 c= M by A3, XBOOLE_1:1; then reconsider L1 = L1 as Linear_Combination of M by RLVECT_2:def_6; A4: for v being VECTOR of V st v in Carrier L1 holds L1 . v = L . v proof let v be VECTOR of V; ::_thesis: ( v in Carrier L1 implies L1 . v = L . v ) assume v in Carrier L1 ; ::_thesis: L1 . v = L . v then v = u by A3, TARSKI:def_1; hence L1 . v = L . v by A2; ::_thesis: verum end; defpred S1[ set , set ] means ( ( $1 in (Carrier L) \ {u} implies $2 = L . $1 ) & ( not $1 in (Carrier L) \ {u} implies $2 = 0 ) ); A5: for x being set st x in the carrier of V holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in the carrier of V implies ex y being set st S1[x,y] ) assume x in the carrier of V ; ::_thesis: ex y being set st S1[x,y] ( x in (Carrier L) \ {u} or not x in (Carrier L) \ {u} ) ; hence ex y being set st S1[x,y] ; ::_thesis: verum end; consider L2 being Function such that A6: ( dom L2 = the carrier of V & ( for x being set st x in the carrier of V holds S1[x,L2 . x] ) ) from CLASSES1:sch_1(A5); for y being set st y in rng L2 holds y in REAL proof let y be set ; ::_thesis: ( y in rng L2 implies y in REAL ) assume y in rng L2 ; ::_thesis: y in REAL then consider x being set such that A7: x in dom L2 and A8: y = L2 . x by FUNCT_1:def_3; percases ( x in (Carrier L) \ {u} or not x in (Carrier L) \ {u} ) ; supposeA9: x in (Carrier L) \ {u} ; ::_thesis: y in REAL then reconsider x = x as VECTOR of V ; y = L . x by A6, A8, A9; hence y in REAL ; ::_thesis: verum end; suppose not x in (Carrier L) \ {u} ; ::_thesis: y in REAL then y = 0 by A6, A7, A8; hence y in REAL ; ::_thesis: verum end; end; end; then rng L2 c= REAL by TARSKI:def_3; then A10: L2 is Element of Funcs ( the carrier of V,REAL) by A6, FUNCT_2:def_2; ex T being finite Subset of V st for v being Element of V st not v in T holds L2 . v = 0 proof set T = (Carrier L) \ {u}; reconsider T = (Carrier L) \ {u} as finite Subset of V ; take T ; ::_thesis: for v being Element of V st not v in T holds L2 . v = 0 thus for v being Element of V st not v in T holds L2 . v = 0 by A6; ::_thesis: verum end; then reconsider L2 = L2 as Linear_Combination of V by A10, RLVECT_2:def_3; for x being set st x in Carrier L2 holds x in M proof let x be set ; ::_thesis: ( x in Carrier L2 implies x in M ) assume A11: x in Carrier L2 ; ::_thesis: x in M then reconsider x = x as VECTOR of V ; L2 . x <> 0 by A11, RLVECT_2:19; then x in (Carrier L) \ {u} by A6; then A12: x in Carrier L by XBOOLE_0:def_5; Carrier L c= M by RLVECT_2:def_6; hence x in M by A12; ::_thesis: verum end; then Carrier L2 c= M by TARSKI:def_3; then reconsider L2 = L2 as Linear_Combination of M by RLVECT_2:def_6; for x being set st x in Carrier L2 holds x in (Carrier L) \ {u} proof let x be set ; ::_thesis: ( x in Carrier L2 implies x in (Carrier L) \ {u} ) assume A13: x in Carrier L2 ; ::_thesis: x in (Carrier L) \ {u} then reconsider x = x as VECTOR of V ; L2 . x <> 0 by A13, RLVECT_2:19; hence x in (Carrier L) \ {u} by A6; ::_thesis: verum end; then A14: Carrier L2 c= (Carrier L) \ {u} by TARSKI:def_3; for v being VECTOR of V holds L . v = (L1 + L2) . v proof let v be VECTOR of V; ::_thesis: L . v = (L1 + L2) . v percases ( v in Carrier L or not v in Carrier L ) ; supposeA15: v in Carrier L ; ::_thesis: L . v = (L1 + L2) . v percases ( v = u or v <> u ) ; supposeA16: v = u ; ::_thesis: L . v = (L1 + L2) . v then A17: not v in Carrier L2 by A14, ZFMISC_1:56; (L1 + L2) . v = (L1 . v) + (L2 . v) by RLVECT_2:def_10 .= (L . v) + 0 by A2, A16, A17, RLVECT_2:19 ; hence L . v = (L1 + L2) . v ; ::_thesis: verum end; supposeA18: v <> u ; ::_thesis: L . v = (L1 + L2) . v then not v in Carrier L1 by A3, TARSKI:def_1; then A19: L1 . v = 0 by RLVECT_2:19; A20: v in (Carrier L) \ {u} by A15, A18, ZFMISC_1:56; (L1 + L2) . v = (L1 . v) + (L2 . v) by RLVECT_2:def_10 .= 0 + (L . v) by A6, A19, A20 ; hence L . v = (L1 + L2) . v ; ::_thesis: verum end; end; end; supposeA21: not v in Carrier L ; ::_thesis: L . v = (L1 + L2) . v then not v in Carrier L2 by A14, ZFMISC_1:56; then A22: L2 . v = 0 by RLVECT_2:19; A23: not v in Carrier L1 by A1, A3, A21, TARSKI:def_1; (L1 + L2) . v = (L1 . v) + (L2 . v) by RLVECT_2:def_10 .= 0 by A23, A22, RLVECT_2:19 ; hence L . v = (L1 + L2) . v by A21, RLVECT_2:19; ::_thesis: verum end; end; end; then A24: L = L1 + L2 by RLVECT_2:def_9; for x being set st x in (Carrier L) \ {u} holds x in Carrier L2 proof let x be set ; ::_thesis: ( x in (Carrier L) \ {u} implies x in Carrier L2 ) assume A25: x in (Carrier L) \ {u} ; ::_thesis: x in Carrier L2 then reconsider x = x as VECTOR of V ; x in Carrier L by A25, XBOOLE_0:def_5; then A26: L . x <> 0 by RLVECT_2:19; L2 . x = L . x by A6, A25; hence x in Carrier L2 by A26, RLVECT_2:19; ::_thesis: verum end; then (Carrier L) \ {u} c= Carrier L2 by TARSKI:def_3; then A27: Carrier L2 = (Carrier L) \ {u} by A14, XBOOLE_0:def_10; take L1 ; ::_thesis: ex L2 being Linear_Combination of M st ( Sum L = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 & Carrier L1 c= Carrier L & Carrier L2 c= Carrier L & ( for v being VECTOR of V st v in Carrier L1 holds L1 . v = L . v ) & ( for v being VECTOR of V st v in Carrier L2 holds L2 . v = L . v ) ) take L2 ; ::_thesis: ( Sum L = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 & Carrier L1 c= Carrier L & Carrier L2 c= Carrier L & ( for v being VECTOR of V st v in Carrier L1 holds L1 . v = L . v ) & ( for v being VECTOR of V st v in Carrier L2 holds L2 . v = L . v ) ) A28: (Carrier L) \ {u} c= Carrier L by XBOOLE_1:36; Carrier L1 <> {} proof assume Carrier L1 = {} ; ::_thesis: contradiction then L . u = 0 by A2, RLVECT_2:19; hence contradiction by A1, RLVECT_2:19; ::_thesis: verum end; then A29: Carrier L1 = {u} by A3, ZFMISC_1:33; then Carrier L1 c= Carrier L by A1, ZFMISC_1:31; then card (Carrier L2) = (card (Carrier L)) - (card (Carrier L1)) by A29, A27, CARD_2:44 .= (card (Carrier L)) - 1 by A29, CARD_1:30 ; hence ( Sum L = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 & Carrier L1 c= Carrier L & Carrier L2 c= Carrier L & ( for v being VECTOR of V st v in Carrier L1 holds L1 . v = L . v ) & ( for v being VECTOR of V st v in Carrier L2 holds L2 . v = L . v ) ) by A1, A4, A6, A29, A14, A24, A28, CARD_1:30, RLVECT_3:1, XBOOLE_1:1, ZFMISC_1:31; ::_thesis: verum end; theorem :: CONVEX3:8 for V being RealLinearSpace for M being Subset of V holds ( ( M is convex & M is cone ) iff for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds L . v > 0 ) holds Sum L in M ) proof let V be RealLinearSpace; ::_thesis: for M being Subset of V holds ( ( M is convex & M is cone ) iff for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds L . v > 0 ) holds Sum L in M ) let M be Subset of V; ::_thesis: ( ( M is convex & M is cone ) iff for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds L . v > 0 ) holds Sum L in M ) A1: ( ( for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds L . v > 0 ) holds Sum L in M ) implies ( M is convex & M is cone ) ) proof assume A2: for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds L . v > 0 ) holds Sum L in M ; ::_thesis: ( M is convex & M is cone ) A3: for r being Real for v being VECTOR of V st r > 0 & v in M holds r * v in M proof let r be Real; ::_thesis: for v being VECTOR of V st r > 0 & v in M holds r * v in M let v be VECTOR of V; ::_thesis: ( r > 0 & v in M implies r * v in M ) assume that A4: r > 0 and A5: v in M ; ::_thesis: r * v in M consider L being Linear_Combination of {v} such that A6: L . v = r by RLVECT_4:37; A7: for u being VECTOR of V st u in Carrier L holds L . u > 0 proof let u be VECTOR of V; ::_thesis: ( u in Carrier L implies L . u > 0 ) A8: Carrier L c= {v} by RLVECT_2:def_6; assume u in Carrier L ; ::_thesis: L . u > 0 hence L . u > 0 by A4, A6, A8, TARSKI:def_1; ::_thesis: verum end; A9: v in Carrier L by A4, A6, RLVECT_2:19; {v} c= M by A5, ZFMISC_1:31; then reconsider L = L as Linear_Combination of M by RLVECT_2:21; Sum L in M by A2, A9, A7; hence r * v in M by A6, RLVECT_2:32; ::_thesis: verum end; A10: for u, v being VECTOR of V st u in M & v in M holds u + v in M proof let u, v be VECTOR of V; ::_thesis: ( u in M & v in M implies u + v in M ) assume that A11: u in M and A12: v in M ; ::_thesis: u + v in M percases ( u <> v or u = v ) ; supposeA13: u <> v ; ::_thesis: u + v in M consider L being Linear_Combination of {u,v} such that A14: ( L . u = 1 & L . v = 1 ) by A13, RLVECT_4:38; A15: Sum L = (1 * u) + (1 * v) by A13, A14, RLVECT_2:33 .= u + (1 * v) by RLVECT_1:def_8 .= u + v by RLVECT_1:def_8 ; A16: Carrier L <> {} by A14, RLVECT_2:19; A17: for v1 being VECTOR of V st v1 in Carrier L holds L . v1 > 0 proof let v1 be VECTOR of V; ::_thesis: ( v1 in Carrier L implies L . v1 > 0 ) A18: Carrier L c= {u,v} by RLVECT_2:def_6; assume A19: v1 in Carrier L ; ::_thesis: L . v1 > 0 percases ( v1 = u or v1 = v ) by A19, A18, TARSKI:def_2; suppose v1 = u ; ::_thesis: L . v1 > 0 hence L . v1 > 0 by A14; ::_thesis: verum end; suppose v1 = v ; ::_thesis: L . v1 > 0 hence L . v1 > 0 by A14; ::_thesis: verum end; end; end; {u,v} c= M by A11, A12, ZFMISC_1:32; then reconsider L = L as Linear_Combination of M by RLVECT_2:21; Sum L in M by A2, A16, A17; hence u + v in M by A15; ::_thesis: verum end; supposeA20: u = v ; ::_thesis: u + v in M (1 + 1) * u in M by A3, A11; then (1 * u) + (1 * u) in M by RLVECT_1:def_6; then u + (1 * u) in M by RLVECT_1:def_8; hence u + v in M by A20, RLVECT_1:def_8; ::_thesis: verum end; end; end; M is cone by A3, Def3; hence ( M is convex & M is cone ) by A10, Th7; ::_thesis: verum end; ( M is convex & M is cone implies for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds L . v > 0 ) holds Sum L in M ) proof defpred S1[ Nat] means for LL being Linear_Combination of M st card (Carrier LL) = $1 & ( for u being VECTOR of V st u in Carrier LL holds LL . u > 0 ) & ex L1, L2 being Linear_Combination of M st ( Sum LL = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 & Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL & ( for v being VECTOR of V st v in Carrier L1 holds L1 . v = LL . v ) & ( for v being VECTOR of V st v in Carrier L2 holds L2 . v = LL . v ) ) holds Sum LL in M; assume that A21: M is convex and A22: M is cone ; ::_thesis: for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds L . v > 0 ) holds Sum L in M A23: S1[1] proof let LL be Linear_Combination of M; ::_thesis: ( card (Carrier LL) = 1 & ( for u being VECTOR of V st u in Carrier LL holds LL . u > 0 ) & ex L1, L2 being Linear_Combination of M st ( Sum LL = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 & Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL & ( for v being VECTOR of V st v in Carrier L1 holds L1 . v = LL . v ) & ( for v being VECTOR of V st v in Carrier L2 holds L2 . v = LL . v ) ) implies Sum LL in M ) assume that A24: card (Carrier LL) = 1 and A25: for u being VECTOR of V st u in Carrier LL holds LL . u > 0 and ex L1, L2 being Linear_Combination of M st ( Sum LL = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 & Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL & ( for v being VECTOR of V st v in Carrier L1 holds L1 . v = LL . v ) & ( for v being VECTOR of V st v in Carrier L2 holds L2 . v = LL . v ) ) ; ::_thesis: Sum LL in M consider x being set such that A26: Carrier LL = {x} by A24, CARD_2:42; {x} c= M by A26, RLVECT_2:def_6; then A27: x in M by ZFMISC_1:31; then reconsider x = x as VECTOR of V ; x in Carrier LL by A26, TARSKI:def_1; then A28: LL . x > 0 by A25; Sum LL = (LL . x) * x by A26, RLVECT_2:35; hence Sum LL in M by A22, A27, A28, Def3; ::_thesis: verum end; A29: for k being non empty Nat st S1[k] holds S1[k + 1] proof let k be non empty Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A30: S1[k] ; ::_thesis: S1[k + 1] let LL be Linear_Combination of M; ::_thesis: ( card (Carrier LL) = k + 1 & ( for u being VECTOR of V st u in Carrier LL holds LL . u > 0 ) & ex L1, L2 being Linear_Combination of M st ( Sum LL = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 & Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL & ( for v being VECTOR of V st v in Carrier L1 holds L1 . v = LL . v ) & ( for v being VECTOR of V st v in Carrier L2 holds L2 . v = LL . v ) ) implies Sum LL in M ) assume that A31: card (Carrier LL) = k + 1 and A32: for u being VECTOR of V st u in Carrier LL holds LL . u > 0 and A33: ex L1, L2 being Linear_Combination of M st ( Sum LL = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 & Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL & ( for v being VECTOR of V st v in Carrier L1 holds L1 . v = LL . v ) & ( for v being VECTOR of V st v in Carrier L2 holds L2 . v = LL . v ) ) ; ::_thesis: Sum LL in M consider L1, L2 being Linear_Combination of M such that A34: Sum LL = (Sum L1) + (Sum L2) and A35: card (Carrier L1) = 1 and A36: card (Carrier L2) = (card (Carrier LL)) - 1 and A37: Carrier L1 c= Carrier LL and A38: Carrier L2 c= Carrier LL and A39: for v being VECTOR of V st v in Carrier L1 holds L1 . v = LL . v and A40: for v being VECTOR of V st v in Carrier L2 holds L2 . v = LL . v by A33; A41: for u being VECTOR of V st u in Carrier L1 holds L1 . u > 0 proof let u be VECTOR of V; ::_thesis: ( u in Carrier L1 implies L1 . u > 0 ) assume A42: u in Carrier L1 ; ::_thesis: L1 . u > 0 then L1 . u = LL . u by A39; hence L1 . u > 0 by A32, A37, A42; ::_thesis: verum end; A43: for u being VECTOR of V st u in Carrier L2 holds L2 . u > 0 proof let u be VECTOR of V; ::_thesis: ( u in Carrier L2 implies L2 . u > 0 ) assume A44: u in Carrier L2 ; ::_thesis: L2 . u > 0 then L2 . u = LL . u by A40; hence L2 . u > 0 by A32, A38, A44; ::_thesis: verum end; ex LL1, LL2 being Linear_Combination of M st ( Sum L1 = (Sum LL1) + (Sum LL2) & card (Carrier LL1) = 1 & card (Carrier LL2) = (card (Carrier L1)) - 1 & Carrier LL1 c= Carrier L1 & Carrier LL2 c= Carrier L1 & ( for v being VECTOR of V st v in Carrier LL1 holds LL1 . v = L1 . v ) & ( for v being VECTOR of V st v in Carrier LL2 holds LL2 . v = L1 . v ) ) by A35, Lm4; then A45: Sum L1 in M by A23, A35, A41; card (Carrier L2) >= 0 + 1 by A31, A36, NAT_1:13; then ex LL1, LL2 being Linear_Combination of M st ( Sum L2 = (Sum LL1) + (Sum LL2) & card (Carrier LL1) = 1 & card (Carrier LL2) = (card (Carrier L2)) - 1 & Carrier LL1 c= Carrier L2 & Carrier LL2 c= Carrier L2 & ( for v being VECTOR of V st v in Carrier LL1 holds LL1 . v = L2 . v ) & ( for v being VECTOR of V st v in Carrier LL2 holds LL2 . v = L2 . v ) ) by Lm4; then Sum L2 in M by A30, A31, A36, A43; hence Sum LL in M by A21, A22, A34, A45, Th7; ::_thesis: verum end; A46: for k being non empty Nat holds S1[k] from NAT_1:sch_10(A23, A29); let L be Linear_Combination of M; ::_thesis: ( Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds L . v > 0 ) implies Sum L in M ) assume that A47: Carrier L <> {} and A48: for v being VECTOR of V st v in Carrier L holds L . v > 0 ; ::_thesis: Sum L in M card (Carrier L) >= 0 + 1 by A47, NAT_1:13; then ex L1, L2 being Linear_Combination of M st ( Sum L = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 & Carrier L1 c= Carrier L & Carrier L2 c= Carrier L & ( for v being VECTOR of V st v in Carrier L1 holds L1 . v = L . v ) & ( for v being VECTOR of V st v in Carrier L2 holds L2 . v = L . v ) ) by Lm4; hence Sum L in M by A47, A48, A46; ::_thesis: verum end; hence ( ( M is convex & M is cone ) iff for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds L . v > 0 ) holds Sum L in M ) by A1; ::_thesis: verum end; theorem :: CONVEX3:9 for V being non empty RLSStruct for M, N being Subset of V st M is cone & N is cone holds M /\ N is cone proof let V be non empty RLSStruct ; ::_thesis: for M, N being Subset of V st M is cone & N is cone holds M /\ N is cone let M, N be Subset of V; ::_thesis: ( M is cone & N is cone implies M /\ N is cone ) assume that A1: M is cone and A2: N is cone ; ::_thesis: M /\ N is cone let r be Real; :: according to CONVEX3:def_3 ::_thesis: for v being VECTOR of V st r > 0 & v in M /\ N holds r * v in M /\ N let v be VECTOR of V; ::_thesis: ( r > 0 & v in M /\ N implies r * v in M /\ N ) assume that A3: r > 0 and A4: v in M /\ N ; ::_thesis: r * v in M /\ N v in N by A4, XBOOLE_0:def_4; then A5: r * v in N by A2, A3, Def3; v in M by A4, XBOOLE_0:def_4; then r * v in M by A1, A3, Def3; hence r * v in M /\ N by A5, XBOOLE_0:def_4; ::_thesis: verum end;