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

definition
let V be RealLinearSpace;
defpred S1[ object ] means $1 is Convex_Combination of V; func ConvexComb V -> set means :Def1: :: CONVEX3:def 1 for L being object holds ( L in it iff L is Convex_Combination of V ); existence ex b1 being set st for L being object holds ( L in b1 iff L is Convex_Combination of V ) proof end; uniqueness for b1, b2 being set st ( for L being object holds ( L in b1 iff L is Convex_Combination of V ) ) & ( for L being object holds ( L in b2 iff L is Convex_Combination of V ) ) holds b1 = b2 proof end; end; :: deftheorem Def1 defines ConvexComb CONVEX3:def 1 : for V being RealLinearSpace for b2 being set holds ( b2 = ConvexComb V iff for L being object 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[ object ] means$1 is Convex_Combination of M;
func ConvexComb M -> set means :: CONVEX3:def 2
for L being object holds
( L in it iff L is Convex_Combination of M );
existence
ex b1 being set st
for L being object holds
( L in b1 iff L is Convex_Combination of M )
proof end;
uniqueness
for b1, b2 being set st ( for L being object holds
( L in b1 iff L is Convex_Combination of M ) ) & ( for L being object holds
( L in b2 iff L is Convex_Combination of M ) ) holds
b1 = b2
proof end;
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 object holds
( L in b3 iff L is Convex_Combination of M ) );

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

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 ) )
proof end;

reconsider jd = 1 / 2, jt = 1 / 3 as Element of REAL by XREAL_0:def 1;

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
proof end;

theorem :: CONVEX3:3
for V being RealLinearSpace
for 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
proof end;

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

proof end;

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

proof end;

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

proof end;

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 ;

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 }
proof end;

definition
let V be non empty RLSStruct ;
let M be Subset of V;
attr M is cone means :Def3: :: CONVEX3:def 3
for r being Real
for v being VECTOR of V st r > 0 & 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 & 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 ;

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
proof end;
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 & b1 is cone )
proof end;
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 & b1 is cone )
proof end;
end;

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

Lm4: for V being RealLinearSpace
for M being Subset of V
for L being Linear_Combination of M st card () >= 1 holds
ex L1, L2 being Linear_Combination of M st
( Sum L = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card ()) - 1 & Carrier L1 c= Carrier L & Carrier L2 c= Carrier L & ( for v being VECTOR of V st v in Carrier L1 holds
L1 . v = L . v ) & ( for v being VECTOR of V st v in Carrier L2 holds
L2 . v = L . v ) )

proof end;

theorem :: CONVEX3:8
for V being RealLinearSpace
for 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 )
proof end;

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