Volume 14, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

### The abstract of the Mizar article:

### Convex Sets and Convex Combinations

**by****Noboru Endou,****Takashi Mitsuishi, and****Yasunari Shidama**- Received November 5, 2002
- MML identifier: CONVEX1

- [ Mizar article, MML identifier index ]

environ vocabulary RLVECT_1, FUNCT_1, PROB_2, ARYTM_1, RELAT_1, BHSP_1, FINSEQ_1, BOOLE, JORDAN1, SETFAM_1, CONNSP_3, ARYTM_3, RUSUB_4, RLSUB_1, CONVEX1, FINSEQ_4, SEQ_1, CARD_1, RLVECT_2; notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, PRE_TOPC, STRUCT_0, NUMBERS, XCMPLX_0, XREAL_0, FUNCT_1, CARD_1, NAT_1, REAL_1, FUNCT_2, FINSEQ_1, RLVECT_1, RLSUB_1, FINSEQ_4, RLVECT_2, RVSUM_1, BHSP_1, RUSUB_4, RUSUB_5; constructors REAL_1, EUCLID, SEQ_1, RUSUB_5, FINSEQ_4, RLVECT_2, MEMBERED; clusters STRUCT_0, XREAL_0, RELSET_1, ARYTM_3, RLVECT_1, SEQ_1, RUSUB_4, MEMBERED; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin :: Convex Sets definition let V be non empty RLSStruct, M be Subset of V, r be Real; func r*M -> Subset of V equals :: CONVEX1:def 1 {r * v where v is Element of V: v in M}; end; definition let V be non empty RLSStruct, M be Subset of V; attr M is convex means :: CONVEX1:def 2 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; end; theorem :: CONVEX1:1 for V being RealLinearSpace-like (non empty RLSStruct), M being Subset of V, r being Real st M is convex holds r*M is convex; theorem :: CONVEX1:2 for V being Abelian add-associative RealLinearSpace-like (non empty RLSStruct), M,N being Subset of V st M is convex & N is convex holds M + N is convex; theorem :: CONVEX1:3 for V being RealLinearSpace, M,N being Subset of V st M is convex & N is convex holds M - N is convex; theorem :: CONVEX1:4 for V being non empty RLSStruct, M being Subset of V holds M is convex iff (for r being Real st 0 < r & r < 1 holds r*M + (1-r)*M c= M); theorem :: CONVEX1:5 for V being Abelian (non empty RLSStruct), M being Subset of V st M is convex holds (for r being Real st 0 < r & r < 1 holds (1-r)*M + r*M c= M); theorem :: CONVEX1:6 for V being Abelian add-associative RealLinearSpace-like (non empty RLSStruct ) , M,N being Subset of V st M is convex & N is convex holds for r being Real holds r*M + (1-r)*N is convex; theorem :: CONVEX1:7 for V being RealLinearSpace, M being Subset of V, v being VECTOR of V holds M is convex iff v + M is convex; theorem :: CONVEX1:8 for V being RealLinearSpace holds Up((0).V) is convex; theorem :: CONVEX1:9 for V being RealLinearSpace holds Up((Omega).V) is convex; theorem :: CONVEX1:10 for V being non empty RLSStruct, M being Subset of V st M = {} holds M is convex; theorem :: CONVEX1:11 for V being Abelian add-associative RealLinearSpace-like (non empty RLSStruct), M1,M2 being Subset of V, r1,r2 being Real st M1 is convex & M2 is convex holds r1*M1 + r2*M2 is convex; theorem :: CONVEX1:12 for V being RealLinearSpace-like (non empty RLSStruct), M being Subset of V, r1,r2 being Real holds (r1 + r2)*M c= r1*M + r2*M; theorem :: CONVEX1:13 for V being RealLinearSpace, M being Subset of V, r1,r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds r1*M + r2*M c= (r1 + r2)*M; theorem :: CONVEX1:14 for V being Abelian add-associative RealLinearSpace-like (non empty RLSStruct ) , M1,M2,M3 being Subset of V, r1,r2,r3 being Real st M1 is convex & M2 is convex & M3 is convex holds r1*M1 + r2*M2 + r3*M3 is convex; theorem :: CONVEX1:15 for V being non empty RLSStruct, F being Subset-Family of V st (for M being Subset of V st M in F holds M is convex) holds meet F is convex; theorem :: CONVEX1:16 for V being non empty RLSStruct, M being Subset of V st M is Affine holds M is convex; definition let V be non empty RLSStruct; cluster convex Subset of V; end; definition let V be non empty RLSStruct; cluster empty convex Subset of V; end; definition let V be non empty RLSStruct; cluster non empty convex Subset of V; end; theorem :: CONVEX1:17 for V being RealUnitarySpace-like (non empty UNITSTR), M being Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V : u .|. v >= r} holds M is convex; theorem :: CONVEX1:18 for V being RealUnitarySpace-like (non empty UNITSTR), M being Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V : u .|. v > r} holds M is convex; theorem :: CONVEX1:19 for V being RealUnitarySpace-like (non empty UNITSTR), M being Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V : u .|. v <= r} holds M is convex; theorem :: CONVEX1:20 for V being RealUnitarySpace-like (non empty UNITSTR), M being Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V : u .|. v < r} holds M is convex; begin :: Convex Combinations definition let V be RealLinearSpace, L be Linear_Combination of V; attr L is convex means :: CONVEX1:def 3 ex F being FinSequence of the carrier of V st (F is one-to-one & rng F = Carrier L & (ex f being FinSequence of REAL st len f = len F & Sum(f) = 1 & (for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0))); end; theorem :: CONVEX1:21 for V being RealLinearSpace, L being Linear_Combination of V st L is convex holds Carrier(L) <> {}; theorem :: CONVEX1:22 for V being RealLinearSpace, L being Linear_Combination of V, v being VECTOR of V st L is convex & L.v <= 0 holds not v in Carrier(L); theorem :: CONVEX1:23 for V being RealLinearSpace, L being Linear_Combination of V st L is convex holds L <> ZeroLC(V); theorem :: CONVEX1:24 for V being RealLinearSpace, v being VECTOR of V, L being Linear_Combination of {v} st L is convex holds L.v = 1 & Sum(L) = L.v * v; theorem :: CONVEX1:25 for V being RealLinearSpace, v1,v2 being VECTOR of V, L being Linear_Combination of {v1,v2} st v1 <> v2 & L is convex holds L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 & Sum(L) = L.v1 * v1 + L.v2 * v2; theorem :: CONVEX1:26 for V being RealLinearSpace, v1,v2,v3 being VECTOR of V, L being Linear_Combination of {v1,v2,v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 & L is convex holds L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 & Sum(L) = L.v1 * v1 + L.v2 * v2 + L.v3 * v3; theorem :: CONVEX1:27 for V being RealLinearSpace, v being VECTOR of V, L being Linear_Combination of V st L is convex & Carrier(L) = {v} holds L.v = 1; theorem :: CONVEX1:28 for V being RealLinearSpace, v1,v2 being VECTOR of V, L being Linear_Combination of V st L is convex & Carrier(L) = {v1,v2} & v1 <> v2 holds L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0; theorem :: CONVEX1:29 for V being RealLinearSpace, v1,v2,v3 being VECTOR of V, L being Linear_Combination of V st L is convex & Carrier(L) = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 & Sum(L) = L.v1 * v1 + L.v2 * v2 + L.v3 * v3; begin :: Convex Hull scheme SubFamExRLS {A() -> RLSStruct, P[Subset of A()]}: ex F being Subset-Family of A() st for B being Subset of A() holds B in F iff P[B]; scheme SubFamExRLS2 {A() -> RLSStruct, P[Subset of A()]}: ex F being Subset-Family of A() st for B being Subset of A() holds B in F iff P[B]; definition let V be non empty RLSStruct, M be Subset of V; func Convex-Family M -> Subset-Family of V means :: CONVEX1:def 4 for N being Subset of V holds N in it iff (N is convex & M c= N); end; definition let V be non empty RLSStruct, M being Subset of V; func conv(M) -> convex Subset of V equals :: CONVEX1:def 5 meet (Convex-Family M); end; theorem :: CONVEX1:30 for V being non empty RLSStruct, M being Subset of V, N being convex Subset of V st M c= N holds conv(M) c= N; begin :: Miscellaneous theorem :: CONVEX1:31 for p being FinSequence, x,y,z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x holds p = <* x,y,z *> or p = <* x,z,y *> or p = <* y,x,z *> or p = <* y,z,x *> or p = <* z,x,y *> or p = <* z,y,x *>; theorem :: CONVEX1:32 for V being RealLinearSpace-like (non empty RLSStruct), M be Subset of V holds 1*M = M; theorem :: CONVEX1:33 for V being non empty RLSStruct, M being empty Subset of V, r be Real holds r * M = {}; theorem :: CONVEX1:34 for V being RealLinearSpace, M be non empty Subset of V holds 0 * M = {0.V}; theorem :: CONVEX1:35 for V being right_zeroed (non empty LoopStr), M being Subset of V holds M + {0.V} = M; theorem :: CONVEX1:36 for V be add-associative (non empty LoopStr), M1,M2,M3 be Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3); theorem :: CONVEX1:37 for V being RealLinearSpace-like (non empty RLSStruct), M being Subset of V, r1,r2 being Real holds r1*(r2*M) = (r1*r2)*M; theorem :: CONVEX1:38 for V being RealLinearSpace-like (non empty RLSStruct), M1,M2 being Subset of V, r being Real holds r*(M1 + M2) = r*M1 + r*M2; theorem :: CONVEX1:39 for V being non empty RLSStruct, M,N being Subset of V, r being Real st M c= N holds r*M c= r*N; theorem :: CONVEX1:40 for V being non empty LoopStr, M being empty Subset of V, N being Subset of V holds M + N = {};

Back to top