The abstract of the Mizar article:

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;