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

begin

definition

let V be RealLinearSpace;
defpred S₁[ 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 b₁ being set st
for L being set holds
( L in b₁ iff L is Convex_Combination of V )

proof end;

uniqueness
for b₁, b₂ being set st ( for L being set holds
( L in b₁ iff L is Convex_Combination of V ) ) & ( for L being set holds
( L in b₂ iff L is Convex_Combination of V ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines ConvexComb CONVEX3:def 1 :
for V being RealLinearSpace
for b₂ being set holds
( b₂ = ConvexComb V iff for L being set holds
( L in b₂ iff L is Convex_Combination of V ) );

definition

let V be RealLinearSpace;
let M be non empty Subset of V;
defpred S₁[ 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 b₁ being set st
for L being set holds
( L in b₁ iff L is Convex_Combination of M )

proof end;

uniqueness
for b₁, b₂ being set st ( for L being set holds
( L in b₁ iff L is Convex_Combination of M ) ) & ( for L being set holds
( L in b₂ iff L is Convex_Combination of M ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines ConvexComb CONVEX3:def 2 :
for V being RealLinearSpace
for M being non empty Subset of V
for b₃ being set holds
( b₃ = ConvexComb M iff for L being set holds
( L in b₃ 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 ) )

proof end;

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;

begin

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

proof end;

registration

let V be non empty RLSStruct ;
cluster cone Element of K18( the carrier of V);
existence
ex b₁ being Subset of V st b₁ is cone

proof end;

end;

registration

let V be non empty RLSStruct ;
cluster empty cone Element of K18( the carrier of V);
existence
ex b₁ being Subset of V st
( b₁ is empty & b₁ is cone )

proof end;

end;

registration

let V be RealLinearSpace;
cluster non empty cone Element of K18( the carrier of V);
existence
ex b₁ being Subset of V st
( not b₁ is empty & b₁ 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;