### The Mizar article:

### Convex Hull, Set of Convex Combinations and Convex Cone

**by****Noboru Endou, and****Yasunari Shidama**

- Received June 16, 2003
Copyright (c) 2003 Association of Mizar Users

- MML identifier: CONVEX3
- [ MML identifier index ]

environ vocabulary RLVECT_1, FUNCT_1, ARYTM_1, RELAT_1, FINSEQ_1, BOOLE, JORDAN1, ARYTM_3, CONVEX1, FINSEQ_4, SEQ_1, CARD_1, RLVECT_2, FUNCT_2, RFINSEQ, FINSET_1, CONVEX2, CONVEX3; notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, FINSEQ_1, RELAT_1, FUNCT_1, FINSET_1, CARD_1, NAT_1, STRUCT_0, FUNCT_2, RLVECT_1, FINSEQ_4, RLVECT_2, RVSUM_1, CONVEX1, TOPREAL1, RFINSEQ, CONVEX2; constructors REAL_1, SEQ_1, RUSUB_5, FINSEQ_4, CONVEX1, NAT_1, MONOID_0, TOPREAL1, RFINSEQ, MEMBERED; clusters RELSET_1, ARYTM_3, STRUCT_0, RLVECT_1, SEQ_1, RUSUB_4, BINARITH, XREAL_0, MEMBERED, NUMBERS, ORDINAL2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; theorems RLVECT_1, RVSUM_1, FUNCT_1, FINSEQ_1, TARSKI, ZFMISC_1, REAL_1, XBOOLE_0, REAL_2, AXIOMS, XBOOLE_1, RLVECT_2, CARD_1, FINSEQ_3, FINSEQ_4, ENUMSET1, CONVEX1, FUNCT_2, NAT_1, TOPREAL1, RFINSEQ, SQUARE_1, CONVEX2, RLVECT_3, CARD_2, CARD_4, FINSEQ_5, PARTFUN2, GRAPH_5, RELAT_1, XCMPLX_1; schemes BINARITH, RLVECT_4, XBOOLE_0, FINSEQ_1, FUNCT_1; begin :: Equality of Convex Hull and Set of Convex Combinations definition let V be RealLinearSpace; defpred P[set] means $1 is Convex_Combination of V; func ConvexComb(V) -> set means :Def1: for L being set holds L in it iff L is Convex_Combination of V; existence 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) & P[x] from Separation; take A; let L be set; thus L in A implies L is Convex_Combination of V by A1; assume L is Convex_Combination of V; hence thesis by A1; end; uniqueness proof thus for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq; end; end; definition let V be RealLinearSpace, M be non empty Subset of V; defpred P[set] means $1 is Convex_Combination of M; func ConvexComb(M) -> set means for L being set holds L in it iff L is Convex_Combination of M; existence 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) & P[x] from Separation; take A; let L be set; thus L in A implies L is Convex_Combination of M by A1; assume L is Convex_Combination of M; hence thesis by A1; end; uniqueness proof thus for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq; end; end; theorem Th1: for V being RealLinearSpace, v being VECTOR of V holds 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; let v be VECTOR of V; consider L being Linear_Combination of {v} such that A1:L.v = 1 from LinCEx1; A2:Carrier(L) c= {v} by RLVECT_2:def 8; v in Carrier(L) by A1,RLVECT_2:28; then {v} c= Carrier(L) by ZFMISC_1:37; then A3:{v} = Carrier(L) by A2,XBOOLE_0:def 10; consider F being FinSequence of the carrier of V such that A4:F is one-to-one & rng F = Carrier(L) & Sum(L) = Sum(L (#) F) by RLVECT_2:def 10; deffunc F(set) = L.(F.$1); consider f being FinSequence such that A5:len f = len F & for n being Nat st n in Seg(len F) holds f.n = F(n) from SeqLambda; A6:len F = 1 by A3,A4,FINSEQ_3:105; then 1 in Seg len F by FINSEQ_1:4,TARSKI:def 1; then A7:f.1 = L.(F.1) by A5; F = <*v*> by A3,A4,FINSEQ_3:106; then A8:F.1 = v by FINSEQ_1:def 8; rng f c= REAL proof f = <*1*> by A1,A5,A6,A7,A8,FINSEQ_1:57; then rng f = {1} by FINSEQ_1:55; hence thesis by ZFMISC_1:37; end; then reconsider f as FinSequence of REAL by FINSEQ_1:def 4; A9:f.1 >= 0 by A1,A7,A8; f = <*1*> by A1,A5,A6,A7,A8,FINSEQ_1:57; then A10:Sum(f) = 1 by RVSUM_1:103; for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 proof let n be Nat; assume n in dom f; then n in Seg len f by FINSEQ_1:def 3; hence thesis by A5,A6,A9,FINSEQ_1:4,TARSKI:def 1; end; then reconsider L as Convex_Combination of V by A4,A5,A10,CONVEX1:def 3; A11: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; assume v in A; then {v} c= A by ZFMISC_1:37; hence thesis by A3,RLVECT_2:def 8; end; take L; Sum(L) = 1 * v by A1,A3,RLVECT_2:53; hence thesis by A11,RLVECT_1:def 9; end; theorem for V being RealLinearSpace, 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; let v1,v2 be VECTOR of V; assume A1:v1 <> v2; consider L being Linear_Combination of {v1,v2} such that A2:L.v1 = 1/2 & L.v2 = 1/2 from LinCEx2(A1); A3:Carrier(L) c= {v1,v2} by RLVECT_2:def 8; v1 in Carrier(L) & v2 in Carrier(L) by A2,RLVECT_2:28; then {v1,v2} c= Carrier(L) by ZFMISC_1:38; then A4:{v1,v2} = Carrier(L) by A3,XBOOLE_0:def 10; consider F being FinSequence of the carrier of V such that A5:F is one-to-one & rng F = Carrier(L) & Sum(L) = Sum(L (#) F) by RLVECT_2:def 10; deffunc F(set) = L.(F.$1); consider f being FinSequence such that A6:len f = len F & for n being Nat st n in Seg(len F) holds f.n = F(n) from SeqLambda; A7:len F = 2 by A1,A4,A5,FINSEQ_3:107; then 1 in Seg len F & 2 in Seg len F by FINSEQ_1:3; then A8:f.1 = L.(F.1) & f.2 = L.(F.2) by A6; now per cases by A1,A4,A5,FINSEQ_3:108; suppose F = <*v1,v2*>; then A9: F.1 = v1 & F.2 = v2 by FINSEQ_1:61; rng f c= REAL proof f = <*1/2,1/2*> by A2,A6,A7,A8,A9,FINSEQ_1:61; then f = <*1/2*>^<*1/2*> by FINSEQ_1:def 9; then rng f = rng <*1/2*> \/ rng <*1/2*> by FINSEQ_1:44 .= {1/2} by FINSEQ_1:55; hence thesis by ZFMISC_1:37; end; then reconsider f as FinSequence of REAL by FINSEQ_1:def 4; A10: f.1 >= 0 & f.2 >= 0 by A2,A8,A9; f = <*1/2,1/2*> by A2,A6,A7,A8,A9,FINSEQ_1:61; then A11: Sum(f) = 1/2 + 1/2 by RVSUM_1:107 .= 1; for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 proof let n be Nat; assume n in dom f; then n in Seg len f by FINSEQ_1:def 3; hence thesis by A6,A7,A10,FINSEQ_1:4,TARSKI:def 2; end; then reconsider L as Convex_Combination of V by A5,A6,A11,CONVEX1:def 3; A12: for A being non empty Subset of V st {v1,v2} c= A holds L is Convex_Combination of A by A4,RLVECT_2:def 8; take L; thus thesis by A12; suppose F = <*v2,v1*>; then A13: F.1 = v2 & F.2 = v1 by FINSEQ_1:61; rng f c= REAL proof f = <*1/2,1/2*> by A2,A6,A7,A8,A13,FINSEQ_1:61; then f = <*1/2*>^<*1/2*> by FINSEQ_1:def 9; then rng f = rng <*1/2*> \/ rng <*1/2*> by FINSEQ_1:44 .= {1/2} by FINSEQ_1:55; hence thesis by ZFMISC_1:37; end; then reconsider f as FinSequence of REAL by FINSEQ_1:def 4; A14: f.1 >= 0 & f.2 >= 0 by A2,A8,A13; f = <*1/2,1/2*> by A2,A6,A7,A8,A13,FINSEQ_1:61; then A15: Sum(f) = 1/2 + 1/2 by RVSUM_1:107 .= 1; for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 proof let n be Nat; assume n in dom f; then n in Seg len f by FINSEQ_1:def 3; hence thesis by A6,A7,A14,FINSEQ_1:4,TARSKI:def 2; end; then reconsider L as Convex_Combination of V by A5,A6,A15,CONVEX1:def 3; A16: for A being non empty Subset of V st {v1,v2} c= A holds L is Convex_Combination of A by A4,RLVECT_2:def 8; take L; thus thesis by A16; end; hence thesis; end; theorem for V being RealLinearSpace, 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; let v1,v2,v3 be VECTOR of V; assume that A1:v1 <> v2 and A2:v1 <> v3 and A3:v2 <> v3; consider L being Linear_Combination of {v1,v2,v3} such that A4:L.v1 = 1/3 & L.v2 = 1/3 & L.v3 = 1/3 from LinCEx3(A1,A2,A3); A5:Carrier(L) c= {v1,v2,v3} by RLVECT_2:def 8; for x being set st x in {v1,v2,v3} holds x in Carrier(L) proof let x be set; assume A6:x in {v1,v2,v3}; then reconsider x as VECTOR of V; x = v1 or x = v2 or x = v3 by A6,ENUMSET1:13; hence thesis by A4,RLVECT_2:28; end; then {v1,v2,v3} c= Carrier(L) by TARSKI:def 3; then A7:{v1,v2,v3} = Carrier(L) by A5,XBOOLE_0:def 10; consider F being FinSequence of the carrier of V such that A8:F is one-to-one & rng F = Carrier(L) & Sum(L) = Sum(L (#) F) by RLVECT_2:def 10; deffunc F(set) = L.(F.$1); consider f being FinSequence such that A9:len f = len F & for n being Nat st n in Seg(len F) holds f.n = F(n) from SeqLambda; A10:len F = 3 by A1,A2,A3,A7,A8,FINSEQ_3:110; then 1 in Seg len F & 2 in Seg len F & 3 in Seg len F by FINSEQ_1:3; then A11:f.1 = L.(F.1) & f.2 = L.(F.2) & f.3 = L.(F.3) by A9; now per cases by A1,A2,A3,A7,A8,CONVEX1:31; suppose F = <*v1,v2,v3*>; then A12: F.1 = v1 & F.2 = v2 & F.3 = v3 by FINSEQ_1:62; rng f c= REAL proof f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A12,FINSEQ_1:62; 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:44 .= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44 .= {1/3} by FINSEQ_1:55; hence thesis by ZFMISC_1:37; end; then reconsider f as FinSequence of REAL by FINSEQ_1:def 4; A13: f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A12; f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A12,FINSEQ_1:62; then A14: Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1; for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 proof let n be Nat; assume n in dom f; then n in Seg len f by FINSEQ_1:def 3; hence thesis by A9,A10,A13,ENUMSET1:13,FINSEQ_3:1; end; then reconsider L as Convex_Combination of V by A8,A9,A14,CONVEX1:def 3; A15: for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A by A7,RLVECT_2:def 8; take L; thus thesis by A15; suppose F = <* v1,v3,v2*>; then A16: F.1 = v1 & F.2 = v3 & F.3 = v2 by FINSEQ_1:62; rng f c= REAL proof f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A16,FINSEQ_1:62; 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:44 .= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44 .= {1/3} by FINSEQ_1:55; hence thesis by ZFMISC_1:37; end; then reconsider f as FinSequence of REAL by FINSEQ_1:def 4; A17: f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A16; f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A16,FINSEQ_1:62; then A18: Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1; for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 proof let n be Nat; assume n in dom f; then n in Seg len f by FINSEQ_1:def 3; hence thesis by A9,A10,A17,ENUMSET1:13,FINSEQ_3:1; end; then reconsider L as Convex_Combination of V by A8,A9,A18,CONVEX1:def 3; A19: for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A by A7,RLVECT_2:def 8; take L; thus thesis by A19; suppose F = <*v2,v1,v3*>; then A20: F.1 = v2 & F.2 = v1 & F.3 = v3 by FINSEQ_1:62; rng f c= REAL proof f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A20,FINSEQ_1:62; 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:44 .= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44 .= {1/3} by FINSEQ_1:55; hence thesis by ZFMISC_1:37; end; then reconsider f as FinSequence of REAL by FINSEQ_1:def 4; A21: f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A20; f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A20,FINSEQ_1:62; then A22: Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1; for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 proof let n be Nat; assume n in dom f; then n in Seg len f by FINSEQ_1:def 3; hence thesis by A9,A10,A21,ENUMSET1:13,FINSEQ_3:1; end; then reconsider L as Convex_Combination of V by A8,A9,A22,CONVEX1:def 3; A23: for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A by A7,RLVECT_2:def 8; take L; thus thesis by A23; suppose F = <* v2,v3,v1*>; then A24: F.1 = v2 & F.2 = v3 & F.3 = v1 by FINSEQ_1:62; rng f c= REAL proof f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A24,FINSEQ_1:62; 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:44 .= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44 .= {1/3} by FINSEQ_1:55; hence thesis by ZFMISC_1:37; end; then reconsider f as FinSequence of REAL by FINSEQ_1:def 4; A25: f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A24; f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A24,FINSEQ_1:62; then A26: Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1; for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 proof let n be Nat; assume n in dom f; then n in Seg len f by FINSEQ_1:def 3; hence thesis by A9,A10,A25,ENUMSET1:13,FINSEQ_3:1; end; then reconsider L as Convex_Combination of V by A8,A9,A26,CONVEX1:def 3; A27: for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A by A7,RLVECT_2:def 8; take L; thus thesis by A27; suppose F = <* v3,v1,v2*>; then A28: F.1 = v3 & F.2 = v1 & F.3 = v2 by FINSEQ_1:62; rng f c= REAL proof f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A28,FINSEQ_1:62; 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:44 .= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44 .= {1/3} by FINSEQ_1:55; hence thesis by ZFMISC_1:37; end; then reconsider f as FinSequence of REAL by FINSEQ_1:def 4; A29: f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A28; f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A28,FINSEQ_1:62; then A30: Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1; for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 proof let n be Nat; assume n in dom f; then n in Seg len f by FINSEQ_1:def 3; hence thesis by A9,A10,A29,ENUMSET1:13,FINSEQ_3:1; end; then reconsider L as Convex_Combination of V by A8,A9,A30,CONVEX1:def 3; A31: for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A by A7,RLVECT_2:def 8; take L; thus thesis by A31; suppose F = <* v3,v2,v1*>; then A32: F.1 = v3 & F.2 = v2 & F.3 = v1 by FINSEQ_1:62; rng f c= REAL proof f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A32,FINSEQ_1:62; 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:44 .= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44 .= {1/3} by FINSEQ_1:55; hence thesis by ZFMISC_1:37; end; then reconsider f as FinSequence of REAL by FINSEQ_1:def 4; A33: f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A32; f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A32,FINSEQ_1:62; then A34: Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1; for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 proof let n be Nat; assume n in dom f; then n in Seg len f by FINSEQ_1:def 3; hence thesis by A9,A10,A33,ENUMSET1:13,FINSEQ_3:1; end; then reconsider L as Convex_Combination of V by A8,A9,A34,CONVEX1:def 3; A35: for A being non empty Subset of V st {v1,v2,v3} c= A holds L is Convex_Combination of A by A7,RLVECT_2:def 8; take L; thus thesis by A35; end; hence thesis; end; Lm1: for V being RealLinearSpace, 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; let M be non empty Subset of V; assume A1:{Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)} c= M; for u,v being VECTOR of V, 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; let r be Real; set S = {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)}; assume A2: 0 < r & r < 1 & u in M & v in M; consider Lu being Convex_Combination of V such that A3: Sum(Lu) = u & (for A being non empty Subset of V st u in A holds Lu is Convex_Combination of A) by Th1; reconsider Lu as Convex_Combination of M by A2,A3; consider Lv being Convex_Combination of V such that A4: Sum(Lv) = v & (for A being non empty Subset of V st v in A holds Lv is Convex_Combination of A) by Th1; reconsider Lv as Convex_Combination of M by A2,A4; A5: r*u + (1-r)*v = Sum(r*Lu) + (1-r)*Sum(Lv) by A3,A4,RLVECT_3:2 .= Sum(r*Lu) + Sum((1-r)*Lv) by RLVECT_3:2 .= Sum(r*Lu + (1-r)*Lv) by RLVECT_3:1; A6: r*Lu + (1-r)*Lv is Convex_Combination of M by A2,CONVEX2:10; then r*Lu + (1-r)*Lv in ConvexComb(V) by Def1; then r*u + (1-r)*v in S by A5,A6; hence thesis by A1; end; hence thesis by CONVEX1:def 2; end; Lm2: for V being RealLinearSpace, M being non empty Subset of V, L being Convex_Combination of M st card Carrier(L) >= 2 holds ex L1,L2 being Convex_Combination of M, 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; let M be non empty Subset of V; let L be Convex_Combination of M; assume A1:card Carrier(L) >= 2; consider F being FinSequence of the carrier of V such that A2: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)) by CONVEX1:def 3; 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; A4: for n,m being Nat st 1 <= n & n < m & m <= len F holds F.n <> F.m proof let n,m be Nat; assume A5: 1 <= n & n < m & m <= len F; assume A6: F.n = F.m; n <= len F & 1 <= m by A5,AXIOMS:22; then n in Seg len F & m in Seg len F by A5,FINSEQ_1:3; then n in dom F & m in dom F by FINSEQ_1:def 3; hence contradiction by A2,A5,A6,FUNCT_1:def 8; end; then A7:len F >= 2 by A1,A2,GRAPH_5:10; len F >= 1 + 1 by A1,A2,A4,GRAPH_5:10; then A8:len F - 1 >= 1 by REAL_1:84; len F <> 0 by A7; then consider i being Nat such that A9:len F = i + 1 by NAT_1:22; A10:len F - 1 = i by A9,XCMPLX_1:26; set v = F.len F; 1 <= len F by A7,AXIOMS:22; then A11:len F in dom F by FINSEQ_3:27; then A12:F.(len F) in rng F & rng F c= the carrier of V by FINSEQ_1:def 4, FUNCT_1:12; then reconsider v as VECTOR of V; consider L1 being Convex_Combination of V such that A13:Sum(L1) = v & (for A being non empty Subset of V st v in A holds L1 is Convex_Combination of A) by Th1; A14:v in Carrier L & Carrier L c= M by A2,A11,FUNCT_1:12,RLVECT_2:def 8; then reconsider L1 as Convex_Combination of M by A13; 1 <= len f by A3,A7,AXIOMS:22; then len f in Seg len f by FINSEQ_1:3; then A15:len f in dom f by FINSEQ_1:def 3; then f.(len f) in rng f & rng f c= REAL by FINSEQ_1:def 4,FUNCT_1:12; then reconsider r = f.len f as Real; A16:0 < r & r < 1 proof A17: f.(len f) = L.(F.(len f)) & f.(len f) >= 0 by A3,A15; F.(len F) in rng F by A11,FUNCT_1:12; then A18: r <> 0 & r >= 0 by A2,A3,A17,RLVECT_2:28; A19: f = (f|i)^(f/^i) by RFINSEQ:21; f/^i = <*f/.(len f)*> by A3,A9,FINSEQ_5:33 .= <*f.(len f)*> by A15,FINSEQ_4:def 4; then Sum(f) = Sum(f|i) + r by A19,RVSUM_1:104; then A20: Sum(f|i) = 1 - r by A3,XCMPLX_1:26; Sum(f|i) > 0 proof A21: for k being Nat st k in dom(f|i) holds 0 <= (f|i).k proof let k be Nat; assume A22: k in dom(f|i); f|i = f|Seg i by TOPREAL1:def 1; then A23: (f|i).k = f.k by A22,FUNCT_1:68; dom(f|i) c= dom f by FINSEQ_5:20; hence thesis by A3,A22,A23; end; ex k being Nat st k in dom(f|i) & 0 < (f|i).k proof A24: 1 in Seg i by A8,A10,FINSEQ_1:3; 1 <= len f by A3,A7,AXIOMS:22; then A25: 1 in Seg len f by FINSEQ_1:3; then A26: 1 in dom f by FINSEQ_1:def 3; then A27: 1 in dom(f|(Seg i)) by A24,RELAT_1:86; then A28: 1 in dom(f|i) by TOPREAL1:def 1; f|i = f|Seg i by TOPREAL1:def 1; then A29: (f|i).1 = f.1 by A27,FUNCT_1:68 .= L.(F.1) by A3,A26; 1 in dom F by A3,A25,FINSEQ_1:def 3; then F.1 in rng F by FUNCT_1:12; then A30: L.(F.1) <> 0 by A2,RLVECT_2:28; (f|i).1 >= 0 by A21,A28; hence thesis by A28,A29,A30; end; hence thesis by A21,RVSUM_1:115; end; then 1 > r + 0 by A20,REAL_1:86; hence thesis by A18; end; set r' = 1/(1 - r); 1 > r + 0 by A16; then A31:1 - r > 0 by REAL_1:86; then A32:r' > 0 by REAL_2:127; defpred P[set,set] means ($1 in (rng F \ {v}) implies $2 = r'*(L.$1)) & (not ($1 in (rng F \ {v})) implies $2 = 0); A33:for x,y1,y2 being set st x in the carrier of V & P[x,y1] & P[x,y2] holds y1 = y2; A34:for x being set st x in the carrier of V ex y being set st P[x,y] proof let x be set; assume x in the carrier of V; x in (rng F \ {v}) or not (x in (rng F \ {v})); hence thesis; end; consider L2 being Function such that A35:dom L2 = the carrier of V & for x being set st x in the carrier of V holds P[x,L2.x] from FuncEx(A33,A34); for y being set st y in rng L2 holds y in REAL proof let y be set; assume y in rng L2; then consider x being set such that A36: x in dom L2 & y = L2.x by FUNCT_1:def 5; now per cases; suppose A37: x in (rng F \ {v}); then x in rng F by XBOOLE_0:def 4; then reconsider x as VECTOR of V by A2; y = r'*L.x by A35,A36,A37 .= (r'*L).x by RLVECT_2:def 13; hence thesis; suppose not (x in (rng F \ {v})); then y = 0 by A35,A36; hence thesis; end; hence thesis; end; then rng L2 c= REAL by TARSKI:def 3; then A38:L2 is Element of Funcs(the carrier of V, REAL) by A35,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; thus thesis by A2,A35; end; then reconsider L2 as Linear_Combination of V by A38,RLVECT_2:def 5; for n,m being Nat st n in dom (F|i) & m in dom (F|i) & (F|i)/.n = (F|i)/.m holds n = m proof let n,m be Nat; assume that A39: n in dom(F|i) and A40: m in dom(F|i) and A41: (F|i)/.n = (F|i)/.m; A42: dom(F|i) c= dom F by FINSEQ_5:20; F/.n = (F|i)/.n by A39,TOPREAL1:1 .= F/.m by A40,A41,TOPREAL1:1; hence thesis by A2,A39,A40,A42,PARTFUN2:17; end; then A43:F|i is one-to-one by PARTFUN2:16; A44:Carrier(L2) = Carrier(L) \ {v} proof for u being set st u in Carrier(L2) holds u in Carrier(L) \ {v} proof let u be set; assume A45: u in Carrier(L2); then reconsider u as Element of V; L2.u <> 0 by A45,RLVECT_2:28; hence thesis by A2,A35; end; then A46: Carrier(L2) c= Carrier(L) \ {v} by TARSKI:def 3; for u being set st u in Carrier(L) \ {v} holds u in Carrier(L2) proof let u be set; assume A47: u in Carrier(L) \ {v}; then reconsider u as Element of V; A48: u in Carrier(L) by A47,XBOOLE_0:def 4; A49: L2.u = r'*L.u by A2,A35,A47; L.u <> 0 by A48,RLVECT_2:28; then L2.u <> 0 by A32,A49,XCMPLX_1:6; hence thesis by RLVECT_2:28; end; then Carrier(L) \ {v} c= Carrier(L2) by TARSKI:def 3; hence thesis by A46,XBOOLE_0:def 10; end; then Carrier(L2) c= Carrier(L) & Carrier(L) c= M by RLVECT_2:def 8,XBOOLE_1:36; then Carrier(L2) c= M by XBOOLE_1:1; then reconsider L2 as Linear_Combination of M by RLVECT_2:def 8; A50:rng(F|i) = Carrier(L2) proof F = (F|i)^(F/^i) by RFINSEQ:21; then A51: Carrier(L) = rng(F|i) \/ rng(F/^i) by A2,FINSEQ_1:44; rng(F|i) misses rng(F/^i) by A2,FINSEQ_5:37; then A52: Carrier(L) \ rng(F/^i) = rng(F|i) by A51,XBOOLE_1:88; F/^i = <*F/.(len F)*> by A9,FINSEQ_5:33 .= <*F.(len F)*> by A11,FINSEQ_4:def 4; hence thesis by A44,A52,FINSEQ_1:55; end; deffunc F(set) = L2.((F|i).$1); consider f2 being FinSequence such that A53:len f2 = len(F|i) & for k being Nat st k in Seg len(F|i) holds f2.k = F(k) from SeqLambda; for y being set st y in rng f2 holds y in REAL proof let y be set; assume y in rng f2; then consider x being set such that A54: x in dom f2 & y = f2.x by FUNCT_1:def 5; A55: x in Seg len f2 by A54,FINSEQ_1:def 3; then reconsider x as Nat; x in dom (F|i) by A53,A55,FINSEQ_1:def 3; then A56: (F|i).x in rng (F|i) by FUNCT_1:12; consider L2' being Function such that A57: L2 = L2' & dom L2' = the carrier of V & rng L2' c= REAL by FUNCT_2:def 2; L2.((F|i).x) in rng L2 by A50,A56,A57,FUNCT_1:12; then L2.((F|i).x) in REAL by A57; hence thesis by A53,A54,A55; end; then rng f2 c= REAL by TARSKI:def 3; then reconsider f2 as FinSequence of REAL by FINSEQ_1:def 4; Sum(f2) = 1 & (for n being Nat st n in dom(f2) holds f2.n = L2.((F|i).n) & f2.n >= 0) proof A58: i <= len F by A9,NAT_1:37; A59: dom f2 = Seg len (F|i) by A53,FINSEQ_1:def 3; then A60: dom f2 = Seg i by A58,TOPREAL1:3 .= Seg len (f|i) by A3,A58,TOPREAL1:3 .= dom (f|i) by FINSEQ_1:def 3; then A61: dom f2 = dom (r'*(f|i)) by RVSUM_1:65; A62: for k being Nat st k in dom f2 holds f2.k = (r'*(f|i)).k & f2.k >= 0 proof let k be Nat; assume A63: k in dom f2; then A64: f2.k = L2.((F|i).k) by A53,A59; k in dom (f|Seg i) & f|i = f|(Seg i) by A60,A63,TOPREAL1:def 1; then A65: k in dom f /\ Seg i & (f|i).k = f.k by FUNCT_1:68; then A66: k in dom f by XBOOLE_0:def 3; then A67: (f|i).k = L.(F.k) by A3,A65; A68: k in dom (F|i) by A59,A63,FINSEQ_1:def 3; A69: F|i = F|Seg i by TOPREAL1:def 1; then A70: (F|i).k = F.k by A68,FUNCT_1:68; A71: (f|i).k = L.((F|i).k) by A67,A68,A69,FUNCT_1:68; (F|i).k in rng(F|i) by A68,FUNCT_1:12; then reconsider w = (F|i).k as Element of V by A50; A72: not w in {v} proof assume w in {v}; then A73: F.k = v by A70,TARSKI:def 1; dom (F|Seg i) c= dom F by FUNCT_1:76; then A74: k = len F by A2,A11,A68,A69,A73,FUNCT_1:def 8; k <= len(F|i) & len(F|i) <= i by A59,A63,FINSEQ_1:3,FINSEQ_5:19; then k <= i by AXIOMS:22; then k + 1 <= len F by A10,REAL_1:84; hence contradiction by A74,NAT_1:38; end; now per cases; suppose w in (rng F \ {v}); then A75: L2.w = r'*(L.w) by A35 .= r'*(f|i).k by A67,A68,A69,FUNCT_1:68 .= (r'*(f|i)).k by RVSUM_1:66; f.k >= 0 by A3,A66; then r'*(f|i).k >= 0 by A32,A65,SQUARE_1:19; hence thesis by A64,A75,RVSUM_1:66; suppose A76: not w in (rng F \ {v}); then A77: not w in rng F by A72,XBOOLE_0:def 4; A78: f2.k = 0 by A35,A64,A76; L.w = 0 by A2,A77,RLVECT_2:28; then r'*(f|i).k = 0 by A71; hence thesis by A78,RVSUM_1:66; end; hence thesis; end; then for k being Nat st k in dom f2 holds f2.k = (r'*(f|i)).k; then A79: f2 = r'*(f|i) by A61,FINSEQ_1:17; A80: f = (f|i)^(f/^i) by RFINSEQ:21; f/^i = <*f/.(len f)*> by A3,A9,FINSEQ_5:33 .= <*f.(len f)*> by A15,FINSEQ_4:def 4; then Sum(f) = Sum(f|i) + r by A80,RVSUM_1:104; then Sum(f|i) = 1 - r by A3,XCMPLX_1:26; hence Sum(f2) = 1/(1-r)*(1-r) by A79,RVSUM_1:117 .= 1/((1-r)/(1-r)) by XCMPLX_1:82 .= 1/1 by A31,XCMPLX_1:60 .= 1; thus thesis by A53,A59,A62; end; then reconsider L2 as Convex_Combination of M by A43,A50,A53,CONVEX1:def 3; A81:v in {v} by TARSKI:def 1; reconsider B = {v} as non empty Subset of V by TARSKI:def 1; L1 is Convex_Combination of B by A13,A81; then A82:Carrier L1 c= {v} by RLVECT_2:def 8; then A83:Carrier L1 = {} or Carrier L1 = {v} by ZFMISC_1:39; A84:for u being Element of V holds L.u = (r*L1 + (1-r)*L2).u proof let u be Element of V; A85: (r*L1 +(1-r)*L2).u = (r*L1).u +((1-r)*L2).u by RLVECT_2:def 12; now per cases; suppose A86: u in Carrier L; now per cases; suppose A87:u = v; then L1.u = 1 by A83,CONVEX1:21,27; then A88: r*L1.u = r; u in {v} by A87,TARSKI:def 1; then not u in Carrier L2 by A44,XBOOLE_0:def 4; then L2.u = 0 by RLVECT_2:28; then (1-r)*L2.u = 0; then A89: ((1-r)*L2).u = 0 by RLVECT_2:def 13; L.u = r + 0 by A3,A15,A87; hence thesis by A85,A88,A89,RLVECT_2:def 13; suppose u <> v; then A90: not u in Carrier L1 by A82,TARSKI:def 1; then L1.u = 0 by RLVECT_2:28; then r*L1.u = 0; then A91: (r*L1).u = 0 by RLVECT_2:def 13; u in Carrier L2 by A44,A83,A86,A90,CONVEX1:21,XBOOLE_0:def 4; then L2.u = r'*(L.u) by A2,A35,A44; then (1-r)*L2.u = ((1-r)*r')*L.u by XCMPLX_1:4 .= 1/((1-r)/(1-r))*L.u by XCMPLX_1:82 .= 1*L.u by A31,XCMPLX_1:51 .= L.u; hence thesis by A85,A91,RLVECT_2:def 13; end; hence thesis; suppose A92:not u in Carrier L; then A93: L.u = 0 + 0 by RLVECT_2:28; not u in Carrier L1 by A2,A12,A82,A92,TARSKI:def 1; then L1.u = 0 by RLVECT_2:28; then r*L1.u = 0; then A94: (r*L1).u = 0 by RLVECT_2:def 13; not u in Carrier L2 by A44,A92,XBOOLE_0:def 4; then L2.u = 0 by RLVECT_2:28; then (1-r)*L2.u = 0; hence thesis by A85,A93,A94,RLVECT_2:def 13; end; hence thesis; end; take L1,L2,r; {v} c= Carrier L by A14,ZFMISC_1:37; then card Carrier L2 = card Carrier L - card {v} by A44,CARD_2:63; hence thesis by A16,A83,A84,CARD_1:79,CONVEX1:21,RLVECT_2:def 11; end; Lm3: for V being RealLinearSpace, 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; let M be non empty Subset of V; assume A1:M is convex; set S = {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)}; for v being set st v in S holds v in M proof let v being set; assume v in S; then consider L being Convex_Combination of M such that A2: v = Sum(L) & L in ConvexComb(V); reconsider v as VECTOR of V by A2; now per cases; suppose card Carrier(L) < 2; then card Carrier(L) < 1 + 1; then A3: card Carrier(L) <= 1 by NAT_1:38; card Carrier(L) <> 0 proof assume card Carrier(L) = 0; then Carrier(L) = {} by CARD_2:59; hence contradiction by CONVEX1:21; end; then card Carrier(L) > 0 by NAT_1:19; then card Carrier(L) >= 0 + 1 by NAT_1:38; then card Carrier(L) = 1 by A3,AXIOMS:21; then consider x being set such that A4: Carrier(L) = {x} by CARD_2:60; x in Carrier(L) by A4,TARSKI:def 1; then reconsider x as VECTOR of V; A5: v = L.x*x by A2,A4,RLVECT_2:53 .= 1*x by A4,CONVEX1:27 .= x by RLVECT_1:def 9; {x} c= M by A4,RLVECT_2:def 8; hence thesis by A5,ZFMISC_1:37; suppose A6: card Carrier(L) >= 2; defpred P[Nat] means for LL being Convex_Combination of M st card Carrier LL = 1 + $1 & (ex L1,L2 being Convex_Combination of M, 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; A7: P[1] proof let LL be Convex_Combination of M; assume that A8: card Carrier LL = 1 + 1 and A9: ex L1,L2 being Convex_Combination of M, 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; consider L1,L2 be Convex_Combination of M, r be Real such that A10: 0 < r & r < 1 & LL = r*L1 + (1-r)*L2 & card Carrier(L1) = 1 & card Carrier(L2) = card Carrier(LL) - 1 by A9; consider x1 being set such that A11: Carrier(L1) = {x1} by A10,CARD_2:60; x1 in Carrier(L1) by A11,TARSKI:def 1; then reconsider x1 as VECTOR of V; Sum L1 = L1.x1 * x1 & L1.x1 = 1 by A11,CONVEX1:27,RLVECT_2:53; then A12: Sum L1 = x1 by RLVECT_1:def 9; A13: {x1} c= M by A11,RLVECT_2:def 8; consider x2 being set such that A14: Carrier(L2) = {x2} by A8,A10,CARD_2:60; x2 in Carrier(L2) by A14,TARSKI:def 1; then reconsider x2 as VECTOR of V; Sum L2 = L2.x2 * x2 & L2.x2 = 1 by A14,CONVEX1:27,RLVECT_2:53; then A15: Sum L2 = x2 by RLVECT_1:def 9; {x2} c= M by A14,RLVECT_2:def 8; then A16: Sum L1 in M & Sum L2 in M by A12,A13,A15,ZFMISC_1:37; Sum LL = Sum(r*L1) + Sum((1-r)*L2) by A10,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,A10,A16,CONVEX1:def 2; end; A17: for k being non empty Nat st P[k] holds P[k+1] proof let k being non empty Nat; assume A18: P[k]; let LL be Convex_Combination of M; assume that A19: card Carrier LL = 1 + (k+1) and A20: ex L1,L2 being Convex_Combination of M, 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; consider L1,L2 be Convex_Combination of M, r be Real such that A21: 0 < r & r < 1 & LL = r*L1 + (1-r)*L2 & card Carrier(L1) = 1 & card Carrier(L2) = card Carrier(LL) - 1 by A20; consider x1 being set such that A22: Carrier(L1) = {x1} by A21,CARD_2:60; x1 in Carrier(L1) by A22,TARSKI:def 1; then reconsider x1 as VECTOR of V; Sum L1 = L1.x1 * x1 & L1.x1 = 1 by A22,CONVEX1:27,RLVECT_2:53; then A23: Sum L1 = x1 by RLVECT_1:def 9; {x1} c= M by A22,RLVECT_2:def 8; then A24: Sum L1 in M by A23,ZFMISC_1:37; A25: card Carrier(L2) = (k+1) + (1-1) by A19,A21,XCMPLX_1:29 .= k + 1; k > 0 by NAT_1:19; then k >= 0 + 1 by NAT_1:38; then k + 1 >= 1 + 1 by AXIOMS:24; then consider LL1,LL2 be Convex_Combination of M, rr be Real such that A26: 0 < rr & rr < 1 & L2 = rr*LL1 + (1-rr)*LL2 & card Carrier(LL1) = 1 & card Carrier(LL2) = card Carrier(L2) - 1 by A25,Lm2; A27: Sum L2 in M by A18,A25,A26; Sum LL = Sum(r*L1) + Sum((1-r)*L2) by A21,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,A21,A24,A27,CONVEX1:def 2; end; A28: for k being non empty Nat holds P[k] from Ind_from_1(A7,A17); card Carrier(L) <> 0 by A6; then ex k being Nat st card Carrier L = k + 1 by NAT_1:22; then consider k being Nat such that A29: card Carrier L = 1 + k; k <> 0 by A6,A29; then reconsider k as non empty Nat; A30: card Carrier L = 1 + k by A29; ex L1,L2 being Convex_Combination of M, 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 A6,Lm2; hence thesis by A2,A28,A30; end; hence thesis; end; hence thesis by TARSKI:def 3; end; theorem for V being RealLinearSpace, 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 for V being RealLinearSpace, 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; let M be non empty Subset of V; 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; assume x in {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)}; then consider L being Convex_Combination of M such that A1: x = Sum(L) & L in ConvexComb(V); M c= conv(M) by CONVEX2:8; hence thesis by A1,CONVEX2:6; end; then A2:{Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)} c= conv(M) by TARSKI:def 3; consider m being set such that A3:m in M by XBOOLE_0:def 1; reconsider m as VECTOR of V by A3; consider LL being Convex_Combination of V such that A4:Sum LL = m & for A being non empty Subset of V st m in A holds LL is Convex_Combination of A by Th1; reconsider LL as Convex_Combination of M by A3,A4; LL in ConvexComb(V) by Def1; then m in {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)} by A4; 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; assume x in N; then consider L being Convex_Combination of M such that A5: x = Sum L & L in ConvexComb(V); thus thesis by A5; end; then N c= the carrier of V by TARSKI:def 3; then reconsider N as Subset of V; for u,v being VECTOR of V, r be 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; let r be Real; assume A6: 0 < r & r < 1 & u in N & v in N; then consider Lu being Convex_Combination of M such that A7: u = Sum Lu & Lu in ConvexComb(V); consider Lv being Convex_Combination of M such that A8: v = Sum Lv & Lv in ConvexComb(V) by A6; r*Lu + (1-r)*Lv is Convex_Combination of V by A6,CONVEX2:9; then A9: r*Lu + (1-r)*Lv in ConvexComb(V) by Def1; reconsider LL = r*Lu + (1-r)*Lv as Convex_Combination of M by A6,CONVEX2:10; 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 A7,A8,A9; end; then A10:N is convex by CONVEX1:def 2; for v being set st v in M holds v in N proof let v be set; assume A11: v in M; then reconsider v as VECTOR of V; consider LL being Convex_Combination of V such that A12: Sum LL = v & for A being non empty Subset of V st v in A holds LL is Convex_Combination of A by Th1; reconsider LL as Convex_Combination of M by A11,A12; LL in ConvexComb(V) by Def1; hence thesis by A12; end; then M c= N by TARSKI:def 3; then conv(M) c= N by A10,CONVEX1:30; hence thesis by A2,XBOOLE_0:def 10; end; begin :: Cone and Convex Cone definition let V be non empty RLSStruct, M be Subset of V; attr M is cone means :Def3: for r being Real, v being VECTOR of V st r > 0 & v in M holds r*v in M; end; theorem Th6: for V being non empty RLSStruct, M being Subset of V st M = {} holds M is cone proof let V be non empty RLSStruct; let M be Subset of V; assume A1:M = {}; for r being Real, v being VECTOR of V st r > 0 & v in {} holds r*v in {}; hence thesis by A1,Def3; end; definition let V be non empty RLSStruct; cluster cone Subset of V; existence proof consider M being empty Subset of V; M is cone by Th6; hence thesis; end; end; definition let V be non empty RLSStruct; cluster empty cone Subset of V; existence proof set M = {}; M c= the carrier of V by XBOOLE_1:2; then reconsider M as Subset of V; reconsider M as cone Subset of V by Th6; take M; thus thesis; end; end; definition let V be RealLinearSpace; cluster non empty cone Subset of V; existence proof set M = {0.V}; reconsider M as Subset of V; for r being Real, v being VECTOR of V st r > 0 & v in M holds r*v in M proof let r be Real; let v be VECTOR of V; assume r > 0 & v in M; then v = 0.V by TARSKI:def 1; then r*v = 0.V by RLVECT_1:23; hence thesis by TARSKI:def 1; end; then reconsider M as cone Subset of V by Def3; take M; thus thesis by TARSKI:def 1; end; end; theorem Th7: for V being non empty RLSStruct, M being cone Subset of V st V is RealLinearSpace-like 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; let M be cone Subset of V; assume A1:V is RealLinearSpace-like; A2: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 A3: M is convex; for u,v being VECTOR of V st u in M & v in M holds u + v in M proof let u,v being VECTOR of V; assume u in M & v in M; then (1/2)*u + (1-(1/2))*v in M by A3,CONVEX1:def 2; then A4: 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 A1,RLVECT_1:def 9 .= (2*(1/2))*u + 2*((1/2)*v) by A1,RLVECT_1:def 9 .= 1*u + (2*(1/2))*v by A1,RLVECT_1:def 9 .= u + 1*v by A1,RLVECT_1:def 9; hence thesis by A1,A4,RLVECT_1:def 9; end; hence thesis; end; (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 A5: 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, r be 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; let r be Real; assume that A6: 0 < r & r < 1 and A7: u in M & v in M; r + 0 < 1 by A6; then 1 - r > 0 by REAL_1:86; then r*u in M & (1-r)*v in M by A6,A7,Def3; hence thesis by A5; end; hence thesis by CONVEX1:def 2; end; hence thesis by A2; end; Lm4: for V being RealLinearSpace, M being Subset of V, 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; let M be Subset of V; let L be Linear_Combination of M; assume card Carrier(L) >= 1; then card Carrier L <> 0; then Carrier L <> {} by CARD_4:17; then consider u being set such that A1:u in Carrier L by XBOOLE_0:def 1; reconsider u as VECTOR of V by A1; consider L1 be Linear_Combination of {u} such that A2:L1.u = L.u from LinCEx1; Carrier L c= M by RLVECT_2:def 8; then A3:{u} c= M by A1,ZFMISC_1:37; A4:Carrier L1 c= {u} by RLVECT_2:def 8; then Carrier L1 c= M by A3,XBOOLE_1:1; then reconsider L1 as Linear_Combination of M by RLVECT_2:def 8; A5:for v being VECTOR of V st v in Carrier L1 holds L1.v = L.v proof let v be VECTOR of V; assume v in Carrier L1; then v = u by A4,TARSKI:def 1; hence thesis by A2; end; defpred P[set,set] means ($1 in (Carrier L \ {u}) implies $2 = L.$1) & (not ($1 in (Carrier L \ {u})) implies $2 = 0); A6:for x,y1,y2 being set st x in the carrier of V & P[x,y1] & P[x,y2] holds y1 = y2; A7:for x being set st x in the carrier of V ex y being set st P[x,y] proof let x be set; assume x in the carrier of V; x in (Carrier L \ {u}) or not (x in (Carrier L \ {u})); hence thesis; end; consider L2 being Function such that A8:dom L2 = the carrier of V & for x being set st x in the carrier of V holds P[x,L2.x] from FuncEx(A6,A7); for y being set st y in rng L2 holds y in REAL proof let y be set; assume y in rng L2; then consider x being set such that A9: x in dom L2 & y = L2.x by FUNCT_1:def 5; now per cases; suppose A10: x in (Carrier L \ {u}); then reconsider x as VECTOR of V; y = L.x by A8,A9,A10; hence thesis; suppose not (x in (Carrier L \ {u})); then y = 0 by A8,A9; hence thesis; end; hence thesis; end; then rng L2 c= REAL by TARSKI:def 3; then A11:L2 is Element of Funcs(the carrier of V, REAL) by A8,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 as finite Subset of V; take T; thus thesis by A8; end; then reconsider L2 as Linear_Combination of V by A11,RLVECT_2:def 5; for x being set st x in Carrier L2 holds x in M proof let x be set; assume A12: x in Carrier L2; then reconsider x as VECTOR of V; L2.x <> 0 by A12,RLVECT_2:28; then x in Carrier L \ {u} by A8; then A13: x in Carrier L by XBOOLE_0:def 4; Carrier L c= M by RLVECT_2:def 8; hence thesis by A13; end; then Carrier L2 c= M by TARSKI:def 3; then reconsider L2 as Linear_Combination of M by RLVECT_2:def 8; Carrier L1 <> {} proof assume Carrier L1 = {}; then L.u = 0 by A2,RLVECT_2:28; hence contradiction by A1,RLVECT_2:28; end; then A14:Carrier L1 = {u} by A4,ZFMISC_1:39; for x being set st x in Carrier L2 holds x in Carrier L \ {u} proof let x be set; assume A15: x in Carrier L2; then reconsider x as VECTOR of V; L2.x <> 0 by A15,RLVECT_2:28; hence thesis by A8; end; then A16:Carrier L2 c= Carrier L \ {u} by TARSKI:def 3; for x being set st x in Carrier L \ {u} holds x in Carrier L2 proof let x be set; assume A17: x in Carrier L \ {u}; then reconsider x as VECTOR of V; A18: L2.x = L.x by A8,A17; x in Carrier L by A17,XBOOLE_0:def 4; then L.x <> 0 by RLVECT_2:28; hence thesis by A18,RLVECT_2:28; end; then Carrier L \ {u} c= Carrier L2 by TARSKI:def 3; then A19:Carrier L2 = Carrier L \ {u} by A16,XBOOLE_0:def 10; for v being VECTOR of V holds L.v = (L1 + L2).v proof let v be VECTOR of V; now per cases; suppose A20: v in Carrier L; now per cases; suppose A21: v = u; then A22: not v in Carrier L2 by A16,ZFMISC_1:64; (L1 + L2).v = L1.v + L2.v by RLVECT_2:def 12 .= L.v + 0 by A2,A21,A22,RLVECT_2:28; hence thesis; suppose A23: v <> u; then not v in Carrier L1 by A4,TARSKI:def 1; then A24: L1.v = 0 by RLVECT_2:28; A25: v in Carrier L \ {u} by A20,A23,ZFMISC_1:64; (L1 + L2).v = L1.v + L2.v by RLVECT_2:def 12 .= 0 + L.v by A8,A24,A25; hence thesis; end; hence thesis; suppose A26: not v in Carrier L; then A27: not v in Carrier L1 by A1,A4,TARSKI:def 1; not v in Carrier L2 by A16,A26,ZFMISC_1:64; then A28: L2.v = 0 by RLVECT_2:28; (L1 + L2).v = L1.v + L2.v by RLVECT_2:def 12 .= 0 by A27,A28,RLVECT_2:28; hence thesis by A26,RLVECT_2:28; end; hence thesis; end; then A29:L = L1 + L2 by RLVECT_2:def 11; Carrier L1 c= Carrier L by A1,A14,ZFMISC_1:37; then A30:card Carrier L2 = card Carrier L - card Carrier L1 by A14,A19,CARD_2:63 .= card Carrier L - 1 by A14,CARD_1:79; take L1,L2; Carrier L \ {u} c= Carrier L by XBOOLE_1:36; hence thesis by A1,A5,A8,A14,A16,A29,A30,CARD_1:79,RLVECT_3:1,XBOOLE_1:1, ZFMISC_1:37; end; theorem for V being RealLinearSpace, 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; let M be Subset of V; A1: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 assume A2: M is convex & M is cone; let L be Linear_Combination of M; assume A3: Carrier L <> {} & for v being VECTOR of V st v in Carrier L holds L.v > 0; defpred P[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; A4: P[1] proof let LL be Linear_Combination of M; assume that A5: card Carrier LL = 1 and A6: 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); consider x being set such that A7: Carrier LL = {x} by A5,CARD_2:60; {x} c= M by A7,RLVECT_2:def 8; then A8: x in M by ZFMISC_1:37; then reconsider x as VECTOR of V; A9: Sum LL = LL.x * x by A7,RLVECT_2:53; x in Carrier LL by A7,TARSKI:def 1; then LL.x > 0 by A6; hence thesis by A2,A8,A9,Def3; end; A10: for k being non empty Nat st P[k] holds P[k+1] proof let k be non empty Nat; assume A11: P[k]; let LL be Linear_Combination of M; assume that A12: card Carrier LL = k + 1 and A13: for u being VECTOR of V st u in Carrier LL holds LL.u > 0 and A14: 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); consider L1,L2 be Linear_Combination of M such that A15: 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) by A14; A16: card Carrier L2 = k by A12,A15,XCMPLX_1:26; then card Carrier L2 > 0 by NAT_1:19; then card Carrier L2 >= 0 + 1 by NAT_1:38; then A17: 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; for u being VECTOR of V st u in Carrier L2 holds L2.u > 0 proof let u be VECTOR of V; assume u in Carrier L2; then u in Carrier LL & L2.u = LL.u by A15; hence thesis by A13; end; then A18: Sum L2 in M by A11,A16,A17; A19: 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 A15,Lm4; for u being VECTOR of V st u in Carrier L1 holds L1.u > 0 proof let u be VECTOR of V; assume u in Carrier L1; then u in Carrier LL & L1.u = LL.u by A15; hence thesis by A13; end; then Sum L1 in M by A4,A15,A19; hence thesis by A2,A15,A18,Th7; end; A20: for k being non empty Nat holds P[k] from Ind_from_1(A4,A10); A21: card Carrier L <> 0 by A3,CARD_2:59; then card Carrier L > 0 by NAT_1:19; then card Carrier L >= 0 + 1 by NAT_1:38; then A22: 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; consider k being non empty Nat such that A23: card Carrier L = k by A21; thus thesis by A3,A20,A22,A23; end; (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 A24: (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); A25: for r being Real, v being VECTOR of V st r > 0 & v in M holds r*v in M proof let r be Real; let v be VECTOR of V; assume A26: r > 0 & v in M; consider L being Linear_Combination of {v} such that A27: L.v = r from LinCEx1; A28: v in Carrier L by A26,A27,RLVECT_2:28; A29: for u being VECTOR of V st u in Carrier L holds L.u > 0 proof let u be VECTOR of V; assume A30: u in Carrier L; Carrier L c= {v} by RLVECT_2:def 8; hence thesis by A26,A27,A30,TARSKI:def 1; end; {v} c= M by A26,ZFMISC_1:37; then reconsider L as Linear_Combination of M by RLVECT_2:33; Sum L in M by A24,A28,A29; hence thesis by A27,RLVECT_2:50; end; then A31: M is cone by Def3; 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; assume A32: u in M & v in M; now per cases; suppose A33: u <> v; consider L being Linear_Combination of {u,v} such that A34: L.u = 1 & L.v = 1 from LinCEx2(A33); A35: Carrier L <> {} by A34,RLVECT_2:28; A36: for v1 being VECTOR of V st v1 in Carrier L holds L.v1 > 0 proof let v1 be VECTOR of V; assume A37: v1 in Carrier L; A38: Carrier L c= {u,v} by RLVECT_2:def 8; now per cases by A37,A38,TARSKI:def 2; suppose v1 = u; hence thesis by A34; suppose v1 = v; hence thesis by A34; end; hence thesis; end; A39: Sum L = 1 * u + 1 * v by A33,A34,RLVECT_2:51 .= u + 1 * v by RLVECT_1:def 9 .= u + v by RLVECT_1:def 9; {u,v} c= M by A32,ZFMISC_1:38; then reconsider L as Linear_Combination of M by RLVECT_2:33; Sum L in M by A24,A35,A36; hence thesis by A39; suppose A40: u = v; (1+1)*u in M by A25,A32; then 1*u + 1*u in M by RLVECT_1:def 9; then u + 1*u in M by RLVECT_1:def 9; hence thesis by A40,RLVECT_1:def 9; end; hence thesis; end; hence thesis by A31,Th7; end; hence thesis by A1; end; theorem for V being non empty RLSStruct, 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; let M,N be Subset of V; assume that A1:M is cone and A2:N is cone; let r be Real; let v be VECTOR of V; assume A3:r > 0 & v in M /\ N; then A4:v in M & v in N by XBOOLE_0:def 3; then A5:r*v in M by A1,A3,Def3; r*v in N by A2,A3,A4,Def3; hence thesis by A5,XBOOLE_0:def 3; end;

Back to top