:: Convex Hull, Set of Convex Combinations and Convex Cone
:: by Noboru Endou and Yasunari Shidama
::
:: Received June 16, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

definition
let V be RealLinearSpace;
defpred S1[ set ] means $1 is Convex_Combination of V;
func ConvexComb V ->  set  means :Def1: :: CONVEX3:def 1
 for L being set holds
( L in it iff L is Convex_Combination of V );
existence
 ex b1 being set st
for L being set holds
( L in b1 iff L is Convex_Combination of V )
proofend;
uniqueness
 for b1, b2 being set st ( for L being set holds
( L in b1 iff L is Convex_Combination of V ) ) & ( for L being set holds
( L in b2 iff L is Convex_Combination of V ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines ConvexComb CONVEX3:def_1_:_
 for V being RealLinearSpace
for b2 being set holds
( b2 = ConvexComb V iff for L being set holds
( L in b2 iff L is Convex_Combination of V ) );

definition
let V be RealLinearSpace;
let M be non empty Subset of V;
defpred S1[ set ] means $1 is Convex_Combination of M;
func ConvexComb M ->  set  means :: CONVEX3:def 2
 for L being set holds
( L in it iff L is Convex_Combination of M );
existence
 ex b1 being set st
for L being set holds
( L in b1 iff L is Convex_Combination of M )
proofend;
uniqueness
 for b1, b2 being set st ( for L being set holds
( L in b1 iff L is Convex_Combination of M ) ) & ( for L being set holds
( L in b2 iff L is Convex_Combination of M ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines ConvexComb CONVEX3:def_2_:_
 for V being RealLinearSpace
for M being non empty Subset of V
for b3 being set holds
( b3 = ConvexComb M iff for L being set holds
( L in b3 iff L is Convex_Combination of M ) );

theorem Th1: :: CONVEX3:1
for V being RealLinearSpace
for v being VECTOR of V 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 ) )
proofend;

theorem :: CONVEX3:2
for V being RealLinearSpace
for 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
proofend;

theorem :: CONVEX3:3
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V st v1 <> v2 &amp; v1 <> v3 &amp; 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
proofend;

Lm1:  for V being RealLinearSpace
for 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
proofend;

Lm2:  for V being RealLinearSpace
for M being non empty Subset of V
for L being Convex_Combination of M st card (Carrier L) >= 2 holds
ex L1, L2 being Convex_Combination of M ex r being Real st
( 0 < r &amp; r < 1 &amp; L = (r * L1) + ((1 - r) * L2) &amp; card (Carrier L1) = 1 &amp; card (Carrier L2) = (card (Carrier L)) - 1 )
proofend;

Lm3:  for V being RealLinearSpace
for 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
proofend;

theorem :: CONVEX3:4
for V being RealLinearSpace
for 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 :: CONVEX3:5
for V being RealLinearSpace
for M being non empty Subset of V holds conv M =  {  (Sum L) where L is Convex_Combination of M : L in ConvexComb V  }
proofend;

begin

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

:: deftheorem Def3 defines cone CONVEX3:def_3_:_
 for V being non empty RLSStruct
for M being Subset of V holds
( M is cone iff for r being Real
for v being VECTOR of V st r > 0 &amp; v in M holds
r * v in M );

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

registration
let V be non empty RLSStruct ;
cluster cone for Element of K32( the carrier of V);
existence
 ex b1 being Subset of V st b1 is cone
proofend;
end;

registration
let V be non empty RLSStruct ;
cluster empty cone for Element of K32( the carrier of V);
existence
 ex b1 being Subset of V st
( b1 is empty &amp; b1 is cone )
proofend;
end;

registration
let V be RealLinearSpace;
cluster non empty cone for Element of K32( the carrier of V);
existence
 ex b1 being Subset of V st
( not b1 is empty &amp; b1 is cone )
proofend;
end;

theorem Th7: :: CONVEX3:7
for V being non empty RLSStruct
for M being cone Subset of V st V is vector-distributive &amp; V is scalar-distributive &amp; V is scalar-associative &amp; V is scalar-unital holds
( M is convex iff for u, v being VECTOR of V st u in M &amp; v in M holds
u + v in M )
proofend;

Lm4:  for V being RealLinearSpace
for M being Subset of V
for 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) &amp; card (Carrier L1) = 1 &amp; card (Carrier L2) = (card (Carrier L)) - 1 &amp; Carrier L1 c= Carrier L &amp; Carrier L2 c= Carrier L &amp; ( for v being VECTOR of V st v in Carrier L1 holds
L1 . v = L . v ) &amp; ( for v being VECTOR of V st v in Carrier L2 holds
L2 . v = L . v ) )
proofend;

theorem :: CONVEX3:8
for V being RealLinearSpace
for M being Subset of V holds
( ( M is convex &amp; M is cone ) iff for L being Linear_Combination of M st Carrier L <> {} &amp; ( for v being VECTOR of V st v in Carrier L holds
L . v > 0 ) holds
Sum L in M )
proofend;

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