Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

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

by
Noboru Endou, and
Yasunari Shidama

MML identifier: CONVEX3
[ Mizar article, 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;

begin :: Equality of Convex Hull and Set of Convex Combinations

definition let V be RealLinearSpace;
func ConvexComb(V) -> set means
:: CONVEX3:def 1
for L being set holds
L in it iff L is Convex_Combination of V;
end;

definition let V be RealLinearSpace, M be non empty Subset of V;
func ConvexComb(M) -> set means
:: CONVEX3:def 2
for L being set holds
L in it iff L is Convex_Combination of M;
end;

theorem :: CONVEX3:1
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);

theorem :: CONVEX3:2
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;

theorem :: CONVEX3:3
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;

theorem :: CONVEX3:4
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;

theorem :: CONVEX3:5
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)};

begin :: Cone and Convex Cone

definition let V be non empty RLSStruct, M be Subset of V;
attr M is cone means
:: CONVEX3:def 3
for r being Real, v being VECTOR of V st r > 0 & v in M holds
r*v in M;
end;

theorem :: CONVEX3:6
for V being non empty RLSStruct, M being Subset of V st
M = {} holds M is cone;

definition let V be non empty RLSStruct;
cluster cone Subset of V;
end;

definition let V be non empty RLSStruct;
cluster empty cone Subset of V;
end;

definition let V be RealLinearSpace;
cluster non empty cone Subset of V;
end;

theorem :: CONVEX3:7
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;

theorem :: CONVEX3:8
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);

theorem :: CONVEX3:9
for V being non empty RLSStruct, M,N being Subset of V st
M is cone & N is cone holds M /\ N is cone;
```