:: Convex Hull, Set of Convex Combinations and Convex Cone
:: by Noboru Endou and Yasunari Shidama
::
:: Received June 16, 2003
:: 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 (Carrier L) >= 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 (Carrier L)) - 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 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 }
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 (Carrier L) >= 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 (Carrier L)) - 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;