:: Some Properties for Convex Combinations
:: by Noboru Endou , Yasumasa Suzuki and Yasunari Shidama
::
:: Received April 3, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

reconsider rr = 1 as Real ;

set ff = <*rr*>;

theorem :: CONVEX2:1
for V being non empty RLSStruct
for M, N being convex Subset of V holds M /\ N is convex ;

theorem :: CONVEX2:2
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M =  {  u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i &amp; u .|. v <= B . i )  }  holds
M is convex
proofend;

theorem :: CONVEX2:3
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M =  {  u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i &amp; u .|. v < B . i )  }  holds
M is convex
proofend;

theorem :: CONVEX2:4
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M =  {  u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i &amp; u .|. v >= B . i )  }  holds
M is convex
proofend;

theorem :: CONVEX2:5
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M =  {  u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i &amp; u .|. v > B . i )  }  holds
M is convex
proofend;

Lm1:  for V being RealLinearSpace
for M being convex Subset of V
for N being Subset of V
for L being Linear_Combination of N st L is convex &amp; N c= M holds
Sum L in M
proofend;

Lm2:  for V being RealLinearSpace
for M being Subset of V st ( for N being Subset of V
for L being Linear_Combination of N st L is convex &amp; N c= M holds
Sum L in M ) holds
M is convex
proofend;

theorem :: CONVEX2:6
for V being RealLinearSpace
for M being Subset of V holds
( ( for N being Subset of V
for L being Linear_Combination of N st L is convex &amp; N c= M holds
Sum L in M ) iff M is convex ) by Lm1, Lm2;

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

:: deftheorem  defines LinComb CONVEX2:def_1_:_
 for V being RealLinearSpace
for M being Subset of V
for b3 being set holds
( b3 = LinComb M iff for L being set holds
( L in b3 iff L is Linear_Combination of M ) );

registration
let V be RealLinearSpace;
cluster Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() convex for Linear_Combination of V;
existence
 ex b1 being Linear_Combination of V st b1 is convex
proofend;
end;

definition
let V be RealLinearSpace;
mode Convex_Combination of V is convex Linear_Combination of V;
end;

registration
let V be RealLinearSpace;
let M be non empty Subset of V;
cluster Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() convex for Linear_Combination of M;
existence
 ex b1 being Linear_Combination of M st b1 is convex
proofend;
end;

definition
let V be RealLinearSpace;
let M be non empty Subset of V;
mode Convex_Combination of M is convex Linear_Combination of M;
end;

Lm3:  for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 + W2) = (Up W1) + (Up W2)
proofend;

Lm4:  for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 /\ W2) = (Up W1) /\ (Up W2)
proofend;

theorem :: CONVEX2:7
for V being RealLinearSpace
for M being Subset of V holds Convex-Family M <> {} ;

Lm5:  for V being RealLinearSpace
for L1, L2 being Convex_Combination of V
for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
proofend;

Lm6:  for F, G being Function st F,G are_fiberwise_equipotent holds
for x1, x2 being set st x1 in dom F &amp; x2 in dom F &amp; x1 <> x2 holds
ex z1, z2 being set st
( z1 in dom G &amp; z2 in dom G &amp; z1 <> z2 &amp; F . x1 = G . z1 &amp; F . x2 = G . z2 )
proofend;

Lm7:  for V being RealLinearSpace
for L being Linear_Combination of V
for A being Subset of V st A c= Carrier L holds
ex L1 being Linear_Combination of V st Carrier L1 = A
proofend;

theorem Th8: :: CONVEX2:8
for V being RealLinearSpace
for L1, L2 being Convex_Combination of V
for r being Real st 0 < r &amp; r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of V
proofend;

theorem :: CONVEX2:9
for V being RealLinearSpace
for M being non empty Subset of V
for L1, L2 being Convex_Combination of M
for r being Real st 0 < r &amp; r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of M
proofend;

begin

theorem :: CONVEX2:10
for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 + W2) = (Up W1) + (Up W2) by Lm3;

theorem :: CONVEX2:11
for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 /\ W2) = (Up W1) /\ (Up W2) by Lm4;

theorem :: CONVEX2:12
for V being RealLinearSpace
for L1, L2 being Convex_Combination of V
for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) by Lm5;

theorem :: CONVEX2:13
for F, G being Function st F,G are_fiberwise_equipotent holds
for x1, x2 being set st x1 in dom F &amp; x2 in dom F &amp; x1 <> x2 holds
ex z1, z2 being set st
( z1 in dom G &amp; z2 in dom G &amp; z1 <> z2 &amp; F . x1 = G . z1 &amp; F . x2 = G . z2 ) by Lm6;

theorem :: CONVEX2:14
for V being RealLinearSpace
for L being Linear_Combination of V
for A being Subset of V st A c= Carrier L holds
ex L1 being Linear_Combination of V st Carrier L1 = A by Lm7;