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

Received June 16, 2003

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;
```