:: Convex Sets and Convex Combinations on Complex Linear Spaces
:: by Hidenori Matsuzaki , Noboru Endou and Yasunari Shidama
::
:: Received March 3, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

definition
let V be non empty 1-sorted ;
mode C_Linear_Combination of V ->  Element of Funcs ( the carrier of V,COMPLEX) means :Def1: :: CONVEX4:def 1
 ex T being finite Subset of V st
for v being Element of V st not v in T holds
it . v = 0 ;
existence
 ex b1 being Element of Funcs ( the carrier of V,COMPLEX) ex T being finite Subset of V st
for v being Element of V st not v in T holds
b1 . v = 0
proofend;
end;

:: deftheorem Def1 defines C_Linear_Combination CONVEX4:def_1_:_
 for V being non empty 1-sorted
for b2 being Element of Funcs ( the carrier of V,COMPLEX) holds
( b2 is C_Linear_Combination of V iff ex T being finite Subset of V st
for v being Element of V st not v in T holds
b2 . v = 0 );

notation
let V be non empty addLoopStr ;
let L be Element of Funcs ( the carrier of V,COMPLEX);
synonym  Carrier L for  support V;
end;

Lm1: now__::_thesis:_for_V_being_non_empty_addLoopStr_
for_L_being_Element_of_Funcs_(_the_carrier_of_V,COMPLEX)_holds_Carrier_c=_the_carrier_of_V
let V be non empty addLoopStr ; ::_thesis: for L being Element of Funcs ( the carrier of V,COMPLEX) holds Carrier c= the carrier of V
let L be Element of Funcs ( the carrier of V,COMPLEX); ::_thesis: Carrier c= the carrier of V
A1: support L c= dom L by PRE_POLY:37;
thus  Carrier c= the carrier of V ::_thesis: verum
proof
let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in Carrier or x in the carrier of V )
assume  x in support L ; ::_thesis: x in the carrier of V
then  x in dom L by A1;
hence  x in the carrier of V ; ::_thesis: verum
end;
end;

definition
let V be non empty addLoopStr ;
let L be Element of Funcs ( the carrier of V,COMPLEX);
:: original:Carrier
redefine func Carrier L ->  Subset of V equals :: CONVEX4:def 2
 {  v where v is Element of V : L . v <> 0c  }  ;
coherence
 Carrier is Subset of V by Lm1;
compatibility
 for b1 being Subset of V holds
( b1 = Carrier iff b1 =  {  v where v is Element of V : L . v <> 0c  }  )
proofend;
end;

:: deftheorem  defines Carrier CONVEX4:def_2_:_
 for V being non empty addLoopStr
for L being Element of Funcs ( the carrier of V,COMPLEX) holds Carrier L =  {  v where v is Element of V : L . v <> 0c  }  ;

registration
let V be non empty addLoopStr ;
let L be C_Linear_Combination of V;
cluster Carrier  ->  finite ;
coherence
 Carrier L is finite
proofend;
end;

theorem Th1: :: CONVEX4:1
for V being non empty addLoopStr
for L being C_Linear_Combination of V
for v being Element of V holds
( L . v = 0c iff not v in Carrier L )
proofend;

definition
let V be non empty addLoopStr ;
func ZeroCLC V ->  C_Linear_Combination of V means :Def3: :: CONVEX4:def 3
 Carrier it = {} ;
existence
 ex b1 being C_Linear_Combination of V st Carrier b1 = {}
proofend;
uniqueness
 for b1, b2 being C_Linear_Combination of V st Carrier b1 = {} &amp; Carrier b2 = {} holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines ZeroCLC CONVEX4:def_3_:_
 for V being non empty addLoopStr
for b2 being C_Linear_Combination of V holds
( b2 = ZeroCLC V iff Carrier b2 = {} );

registration
let V be non empty addLoopStr ;
cluster Carrier  ->  empty ;
coherence
 Carrier (ZeroCLC V) is empty by Def3;
end;

theorem Th2: :: CONVEX4:2
for V being non empty addLoopStr
for v being Element of V holds (ZeroCLC V) . v = 0c
proofend;

definition
let V be non empty addLoopStr ;
let A be Subset of V;
mode C_Linear_Combination of A ->  C_Linear_Combination of V means :Def4: :: CONVEX4:def 4
 Carrier it c= A;
existence
 ex b1 being C_Linear_Combination of V st Carrier b1 c= A
proofend;
end;

:: deftheorem Def4 defines C_Linear_Combination CONVEX4:def_4_:_
 for V being non empty addLoopStr
for A being Subset of V
for b3 being C_Linear_Combination of V holds
( b3 is C_Linear_Combination of A iff Carrier b3 c= A );

theorem :: CONVEX4:3
for V being non empty addLoopStr
for A, B being Subset of V
for l being C_Linear_Combination of A st A c= B holds
l is C_Linear_Combination of B
proofend;

theorem Th4: :: CONVEX4:4
for V being non empty addLoopStr
for A being Subset of V holds ZeroCLC V is C_Linear_Combination of A
proofend;

theorem Th5: :: CONVEX4:5
for V being non empty addLoopStr
for l being C_Linear_Combination of {} the carrier of V holds l = ZeroCLC V
proofend;

definition
let V be non empty CLSStruct ;
let F be FinSequence of the carrier of V;
let f be Function of the carrier of V,COMPLEX;
funcf (#) F ->  FinSequence of the carrier of V means :Def5: :: CONVEX4:def 5
( len it = len F &amp; ( for i being Nat st i in dom it holds
it . i = (f . (F /. i)) * (F /. i) ) );
existence
 ex b1 being FinSequence of the carrier of V st
( len b1 = len F &amp; ( for i being Nat st i in dom b1 holds
b1 . i = (f . (F /. i)) * (F /. i) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of the carrier of V st len b1 = len F &amp; ( for i being Nat st i in dom b1 holds
b1 . i = (f . (F /. i)) * (F /. i) ) &amp; len b2 = len F &amp; ( for i being Nat st i in dom b2 holds
b2 . i = (f . (F /. i)) * (F /. i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines (#) CONVEX4:def_5_:_
 for V being non empty CLSStruct
for F being FinSequence of the carrier of V
for f being Function of the carrier of V,COMPLEX
for b4 being FinSequence of the carrier of V holds
( b4 = f (#) F iff ( len b4 = len F &amp; ( for i being Nat st i in dom b4 holds
b4 . i = (f . (F /. i)) * (F /. i) ) ) );

theorem Th6: :: CONVEX4:6
for V being non empty CLSStruct
for v being VECTOR of V
for x being set
for F being FinSequence of the carrier of V
for f being Function of the carrier of V,COMPLEX st x in dom F &amp; v = F . x holds
(f (#) F) . x = (f . v) * v
proofend;

theorem :: CONVEX4:7
for V being non empty CLSStruct
for f being Function of the carrier of V,COMPLEX holds f (#) (<*> the carrier of V) = <*> the carrier of V
proofend;

theorem Th8: :: CONVEX4:8
for V being non empty CLSStruct
for v being VECTOR of V
for f being Function of the carrier of V,COMPLEX holds f (#) <*v*> = <*((f . v) * v)*>
proofend;

theorem Th9: :: CONVEX4:9
for V being non empty CLSStruct
for v1, v2 being VECTOR of V
for f being Function of the carrier of V,COMPLEX holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>
proofend;

theorem Th10: :: CONVEX4:10
for V being non empty CLSStruct
for v1, v2, v3 being VECTOR of V
for f being Function of the carrier of V,COMPLEX holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>
proofend;

definition
let V be non empty right_complementable Abelian add-associative right_zeroed CLSStruct ;
let L be C_Linear_Combination of V;
func Sum L ->  Element of V means :Def6: :: CONVEX4:def 6
 ex F being FinSequence of the carrier of V st
( F is one-to-one &amp; rng F = Carrier L &amp; it = Sum (L (#) F) );
existence
 ex b1 being Element of V ex F being FinSequence of the carrier of V st
( F is one-to-one &amp; rng F = Carrier L &amp; b1 = Sum (L (#) F) )
proofend;
uniqueness
 for b1, b2 being Element of V st ex F being FinSequence of the carrier of V st
( F is one-to-one &amp; rng F = Carrier L &amp; b1 = Sum (L (#) F) ) &amp; ex F being FinSequence of the carrier of V st
( F is one-to-one &amp; rng F = Carrier L &amp; b2 = Sum (L (#) F) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines Sum CONVEX4:def_6_:_
 for V being non empty right_complementable Abelian add-associative right_zeroed CLSStruct
for L being C_Linear_Combination of V
for b3 being Element of V holds
( b3 = Sum L iff ex F being FinSequence of the carrier of V st
( F is one-to-one &amp; rng F = Carrier L &amp; b3 = Sum (L (#) F) ) );

theorem Th11: :: CONVEX4:11
for V being non empty right_complementable Abelian add-associative right_zeroed CLSStruct holds Sum (ZeroCLC V) = 0. V
proofend;

theorem :: CONVEX4:12
for V being ComplexLinearSpace
for A being Subset of V st A <> {} holds
( A is linearly-closed iff for l being C_Linear_Combination of A holds Sum l in A )
proofend;

theorem :: CONVEX4:13
for V being non empty right_complementable Abelian add-associative right_zeroed CLSStruct
for l being C_Linear_Combination of {} the carrier of V holds Sum l = 0. V
proofend;

theorem Th14: :: CONVEX4:14
for V being ComplexLinearSpace
for v being VECTOR of V
for l being C_Linear_Combination of {v} holds Sum l = (l . v) * v
proofend;

theorem Th15: :: CONVEX4:15
for V being ComplexLinearSpace
for v1, v2 being VECTOR of V st v1 <> v2 holds
for l being C_Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2)
proofend;

theorem :: CONVEX4:16
for V being non empty right_complementable Abelian add-associative right_zeroed CLSStruct
for L being C_Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V
proofend;

theorem :: CONVEX4:17
for V being ComplexLinearSpace
for L being C_Linear_Combination of V
for v being VECTOR of V st Carrier L = {v} holds
Sum L = (L . v) * v
proofend;

theorem Th18: :: CONVEX4:18
for V being ComplexLinearSpace
for L being C_Linear_Combination of V
for v1, v2 being VECTOR of V st Carrier L = {v1,v2} &amp; v1 <> v2 holds
Sum L = ((L . v1) * v1) + ((L . v2) * v2)
proofend;

definition
let V be non empty addLoopStr ;
let L1, L2 be C_Linear_Combination of V;
:: original:=
redefine predL1 = L2 means :: CONVEX4:def 7
 for v being Element of V holds L1 . v = L2 . v;
compatibility
 ( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v ) by FUNCT_2:63;
end;

:: deftheorem  defines = CONVEX4:def_7_:_
 for V being non empty addLoopStr
for L1, L2 being C_Linear_Combination of V holds
( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v );

definition
let V be non empty addLoopStr ;
let L1, L2 be C_Linear_Combination of V;
:: original:+
redefine funcL1 + L2 ->  C_Linear_Combination of V means :Def8: :: CONVEX4:def 8
 for v being Element of V holds it . v = (L1 . v) + (L2 . v);
coherence
 L1 + L2 is C_Linear_Combination of V
proofend;
compatibility
 for b1 being C_Linear_Combination of V holds
( b1 = L1 + L2 iff for v being Element of V holds b1 . v = (L1 . v) + (L2 . v) )
proofend;
end;

:: deftheorem Def8 defines + CONVEX4:def_8_:_
 for V being non empty addLoopStr
for L1, L2, b4 being C_Linear_Combination of V holds
( b4 = L1 + L2 iff for v being Element of V holds b4 . v = (L1 . v) + (L2 . v) );

theorem Th19: :: CONVEX4:19
for V being non empty CLSStruct
for L1, L2 being C_Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)
proofend;

theorem Th20: :: CONVEX4:20
for V being non empty CLSStruct
for A being Subset of V
for L1, L2 being C_Linear_Combination of V st L1 is C_Linear_Combination of A &amp; L2 is C_Linear_Combination of A holds
L1 + L2 is C_Linear_Combination of A
proofend;

definition
let V be non empty CLSStruct ;
let A be Subset of V;
let L1, L2 be C_Linear_Combination of A;
:: original:+
redefine funcL1 + L2 ->  C_Linear_Combination of A;
coherence
 L1 + L2 is C_Linear_Combination of A by Th20;
end;

theorem :: CONVEX4:21
for V being non empty addLoopStr
for L1, L2 being C_Linear_Combination of V holds L1 + L2 = L2 + L1 ;

theorem Th22: :: CONVEX4:22
for V being non empty CLSStruct
for L1, L2, L3 being C_Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3
proofend;

theorem Th23: :: CONVEX4:23
for V being non empty CLSStruct
for L being C_Linear_Combination of V holds L + (ZeroCLC V) = L
proofend;

definition
let V be non empty CLSStruct ;
let a be Complex;
let L be C_Linear_Combination of V;
funca * L ->  C_Linear_Combination of V means :Def9: :: CONVEX4:def 9
 for v being VECTOR of V holds it . v = a * (L . v);
existence
 ex b1 being C_Linear_Combination of V st
for v being VECTOR of V holds b1 . v = a * (L . v)
proofend;
uniqueness
 for b1, b2 being C_Linear_Combination of V st ( for v being VECTOR of V holds b1 . v = a * (L . v) ) &amp; ( for v being VECTOR of V holds b2 . v = a * (L . v) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines * CONVEX4:def_9_:_
 for V being non empty CLSStruct
for a being Complex
for L, b4 being C_Linear_Combination of V holds
( b4 = a * L iff for v being VECTOR of V holds b4 . v = a * (L . v) );

theorem Th24: :: CONVEX4:24
for V being non empty CLSStruct
for a being Complex
for L being C_Linear_Combination of V st a <> 0c holds
Carrier (a * L) = Carrier L
proofend;

theorem Th25: :: CONVEX4:25
for V being non empty CLSStruct
for L being C_Linear_Combination of V holds 0c * L = ZeroCLC V
proofend;

theorem Th26: :: CONVEX4:26
for V being non empty CLSStruct
for A being Subset of V
for a being Complex
for L being C_Linear_Combination of V st L is C_Linear_Combination of A holds
a * L is C_Linear_Combination of A
proofend;

theorem Th27: :: CONVEX4:27
for V being non empty CLSStruct
for a, b being Complex
for L being C_Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)
proofend;

theorem Th28: :: CONVEX4:28
for V being non empty CLSStruct
for a being Complex
for L1, L2 being C_Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)
proofend;

theorem Th29: :: CONVEX4:29
for V being non empty CLSStruct
for a, b being Complex
for L being C_Linear_Combination of V holds a * (b * L) = (a * b) * L
proofend;

theorem Th30: :: CONVEX4:30
for V being non empty CLSStruct
for L being C_Linear_Combination of V holds 1r * L = L
proofend;

definition
let V be non empty CLSStruct ;
let L be C_Linear_Combination of V;
func - L ->  C_Linear_Combination of V equals :: CONVEX4:def 10
(- 1r) * L;
correctness
coherence
(- 1r) * L is C_Linear_Combination of V;
;
end;

:: deftheorem  defines - CONVEX4:def_10_:_
 for V being non empty CLSStruct
for L being C_Linear_Combination of V holds - L = (- 1r) * L;

theorem Th31: :: CONVEX4:31
for V being non empty CLSStruct
for v being VECTOR of V
for L being C_Linear_Combination of V holds (- L) . v = - (L . v)
proofend;

theorem :: CONVEX4:32
for V being non empty CLSStruct
for L1, L2 being C_Linear_Combination of V st L1 + L2 = ZeroCLC V holds
L2 = - L1
proofend;

theorem :: CONVEX4:33
for V being non empty CLSStruct
for L being C_Linear_Combination of V holds - (- L) = L
proofend;

definition
let V be non empty CLSStruct ;
let L1, L2 be C_Linear_Combination of V;
funcL1 - L2 ->  C_Linear_Combination of V equals :: CONVEX4:def 11
L1 + (- L2);
correctness
coherence
L1 + (- L2) is C_Linear_Combination of V;
;
end;

:: deftheorem  defines - CONVEX4:def_11_:_
 for V being non empty CLSStruct
for L1, L2 being C_Linear_Combination of V holds L1 - L2 = L1 + (- L2);

theorem Th34: :: CONVEX4:34
for V being non empty CLSStruct
for v being VECTOR of V
for L1, L2 being C_Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)
proofend;

theorem :: CONVEX4:35
for V being non empty CLSStruct
for L1, L2 being C_Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)
proofend;

theorem :: CONVEX4:36
for V being non empty CLSStruct
for A being Subset of V
for L1, L2 being C_Linear_Combination of V st L1 is C_Linear_Combination of A &amp; L2 is C_Linear_Combination of A holds
L1 - L2 is C_Linear_Combination of A
proofend;

theorem Th37: :: CONVEX4:37
for V being non empty CLSStruct
for L being C_Linear_Combination of V holds L - L = ZeroCLC V
proofend;

definition
let V be non empty CLSStruct ;
func C_LinComb V ->  set  means :Def12: :: CONVEX4:def 12
 for x being set holds
( x in it iff x is C_Linear_Combination of V );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is C_Linear_Combination of V )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is C_Linear_Combination of V ) ) &amp; ( for x being set holds
( x in b2 iff x is C_Linear_Combination of V ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines C_LinComb CONVEX4:def_12_:_
 for V being non empty CLSStruct
for b2 being set holds
( b2 = C_LinComb V iff for x being set holds
( x in b2 iff x is C_Linear_Combination of V ) );

registration
let V be non empty CLSStruct ;
cluster C_LinComb V ->  non empty ;
coherence
 not C_LinComb V is empty
proofend;
end;

definition
let V be non empty CLSStruct ;
let e be Element of C_LinComb V;
func @ e ->  C_Linear_Combination of V equals :: CONVEX4:def 13
e;
coherence
 e is C_Linear_Combination of V by Def12;
end;

:: deftheorem  defines @ CONVEX4:def_13_:_
 for V being non empty CLSStruct
for e being Element of C_LinComb V holds @ e = e;

definition
let V be non empty CLSStruct ;
let L be C_Linear_Combination of V;
func @ L ->  Element of C_LinComb V equals :: CONVEX4:def 14
L;
coherence
 L is Element of C_LinComb V by Def12;
end;

:: deftheorem  defines @ CONVEX4:def_14_:_
 for V being non empty CLSStruct
for L being C_Linear_Combination of V holds @ L = L;

definition
let V be non empty CLSStruct ;
func C_LCAdd V ->  BinOp of (C_LinComb V) means :Def15: :: CONVEX4:def 15
 for e1, e2 being Element of C_LinComb V holds it . (e1,e2) = (@ e1) + (@ e2);
existence
 ex b1 being BinOp of (C_LinComb V) st
for e1, e2 being Element of C_LinComb V holds b1 . (e1,e2) = (@ e1) + (@ e2)
proofend;
uniqueness
 for b1, b2 being BinOp of (C_LinComb V) st ( for e1, e2 being Element of C_LinComb V holds b1 . (e1,e2) = (@ e1) + (@ e2) ) &amp; ( for e1, e2 being Element of C_LinComb V holds b2 . (e1,e2) = (@ e1) + (@ e2) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def15 defines C_LCAdd CONVEX4:def_15_:_
 for V being non empty CLSStruct
for b2 being BinOp of (C_LinComb V) holds
( b2 = C_LCAdd V iff for e1, e2 being Element of C_LinComb V holds b2 . (e1,e2) = (@ e1) + (@ e2) );

definition
let V be non empty CLSStruct ;
func C_LCMult V ->  Function of [:COMPLEX,(C_LinComb V):],(C_LinComb V) means :Def16: :: CONVEX4:def 16
 for a being Complex
for e being Element of C_LinComb V holds it . [a,e] = a * (@ e);
existence
 ex b1 being Function of [:COMPLEX,(C_LinComb V):],(C_LinComb V) st
for a being Complex
for e being Element of C_LinComb V holds b1 . [a,e] = a * (@ e)
proofend;
uniqueness
 for b1, b2 being Function of [:COMPLEX,(C_LinComb V):],(C_LinComb V) st ( for a being Complex
for e being Element of C_LinComb V holds b1 . [a,e] = a * (@ e) ) &amp; ( for a being Complex
for e being Element of C_LinComb V holds b2 . [a,e] = a * (@ e) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines C_LCMult CONVEX4:def_16_:_
 for V being non empty CLSStruct
for b2 being Function of [:COMPLEX,(C_LinComb V):],(C_LinComb V) holds
( b2 = C_LCMult V iff for a being Complex
for e being Element of C_LinComb V holds b2 . [a,e] = a * (@ e) );

definition
let V be non empty CLSStruct ;
func LC_CLSpace V ->  ComplexLinearSpace equals :: CONVEX4:def 17
 CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #);
coherence
 CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) is ComplexLinearSpace
proofend;
end;

:: deftheorem  defines LC_CLSpace CONVEX4:def_17_:_
 for V being non empty CLSStruct holds LC_CLSpace V = CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #);

registration
let V be non empty CLSStruct ;
cluster LC_CLSpace V ->  strict ;
coherence
 ( LC_CLSpace V is strict &amp; not LC_CLSpace V is empty ) ;
end;

theorem Th38: :: CONVEX4:38
for V being non empty CLSStruct
for L1, L2 being C_Linear_Combination of V holds (vector ((LC_CLSpace V),L1)) + (vector ((LC_CLSpace V),L2)) = L1 + L2
proofend;

theorem Th39: :: CONVEX4:39
for V being non empty CLSStruct
for a being Complex
for L being C_Linear_Combination of V holds a * (vector ((LC_CLSpace V),L)) = a * L
proofend;

theorem Th40: :: CONVEX4:40
for V being non empty CLSStruct
for L being C_Linear_Combination of V holds - (vector ((LC_CLSpace V),L)) = - L
proofend;

theorem :: CONVEX4:41
for V being non empty CLSStruct
for L1, L2 being C_Linear_Combination of V holds (vector ((LC_CLSpace V),L1)) - (vector ((LC_CLSpace V),L2)) = L1 - L2
proofend;

definition
let V be non empty CLSStruct ;
let A be Subset of V;
func LC_CLSpace A ->  strict Subspace of LC_CLSpace V means :: CONVEX4:def 18
 the carrier of it =  {  l where l is C_Linear_Combination of A : verum  }  ;
existence
 ex b1 being strict Subspace of LC_CLSpace V st the carrier of b1 =  {  l where l is C_Linear_Combination of A : verum  }
proofend;
uniqueness
 for b1, b2 being strict Subspace of LC_CLSpace V st the carrier of b1 =  {  l where l is C_Linear_Combination of A : verum  }  &amp; the carrier of b2 =  {  l where l is C_Linear_Combination of A : verum  }  holds
b1 = b2 by CLVECT_1:49;
end;

:: deftheorem  defines LC_CLSpace CONVEX4:def_18_:_
 for V being non empty CLSStruct
for A being Subset of V
for b3 being strict Subspace of LC_CLSpace V holds
( b3 = LC_CLSpace A iff the carrier of b3 =  {  l where l is C_Linear_Combination of A : verum  }  );

begin

definition
let V be ComplexLinearSpace;
let W be Subspace of V;
func Up W ->  Subset of V equals :: CONVEX4:def 19
 the carrier of W;
coherence
 the carrier of W is Subset of V by CLVECT_1:def_8;
end;

:: deftheorem  defines Up CONVEX4:def_19_:_
 for V being ComplexLinearSpace
for W being Subspace of V holds Up W = the carrier of W;

registration
let V be ComplexLinearSpace;
let W be Subspace of V;
cluster Up W ->  non empty ;
coherence
 not Up W is empty ;
end;

definition
let V be non empty CLSStruct ;
let S be Subset of V;
attrS is Affine  means :Def20: :: CONVEX4:def 20
 for x, y being VECTOR of V
for z being Complex st z is Real &amp; x in S &amp; y in S holds
((1r - z) * x) + (z * y) in S;
end;

:: deftheorem Def20 defines Affine CONVEX4:def_20_:_
 for V being non empty CLSStruct
for S being Subset of V holds
( S is Affine iff for x, y being VECTOR of V
for z being Complex st z is Real &amp; x in S &amp; y in S holds
((1r - z) * x) + (z * y) in S );

definition
let V be ComplexLinearSpace;
func (Omega). V ->  strict Subspace of V equals :: CONVEX4:def 21
 CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);
coherence
 CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V
proofend;
end;

:: deftheorem  defines (Omega). CONVEX4:def_21_:_
 for V being ComplexLinearSpace holds (Omega). V = CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);

registration
let V be non empty CLSStruct ;
cluster [#] V ->  Affine ;
coherence
 [#] V is Affine
proofend;
cluster empty  ->  Affine for Element of bool the carrier of V;
coherence
 for b1 being Subset of V st b1 is empty holds
b1 is Affine
proofend;
end;

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

theorem Th42: :: CONVEX4:42
for a being real number
for z being complex number holds Re (a * z) = a * (Re z)
proofend;

theorem Th43: :: CONVEX4:43
for a being real number
for z being complex number holds Im (a * z) = a * (Im z)
proofend;

theorem Th44: :: CONVEX4:44
for a being real number
for z being complex number st 0 <= a &amp; a <= 1 holds
( |.(a * z).| = a * |.z.| &amp; |.((1r - a) * z).| = (1r - a) * |.z.| )
proofend;

begin

definition
let V be non empty CLSStruct ;
let M be Subset of V;
let r be Complex;
funcr * M ->  Subset of V equals :: CONVEX4:def 22
 {  (r * v) where v is Element of V : v in M  }  ;
coherence
  {  (r * v) where v is Element of V : v in M  }  is Subset of V
proofend;
end;

:: deftheorem  defines * CONVEX4:def_22_:_
 for V being non empty CLSStruct
for M being Subset of V
for r being Complex holds r * M =  {  (r * v) where v is Element of V : v in M  }  ;

definition
let V be non empty CLSStruct ;
let M be Subset of V;
attrM is convex  means :Def23: :: CONVEX4:def 23
 for u, v being VECTOR of V
for z being Complex st ex r being Real st
( z = r &amp; 0 < r &amp; r < 1 ) &amp; u in M &amp; v in M holds
(z * u) + ((1r - z) * v) in M;
end;

:: deftheorem Def23 defines convex CONVEX4:def_23_:_
 for V being non empty CLSStruct
for M being Subset of V holds
( M is convex iff for u, v being VECTOR of V
for z being Complex st ex r being Real st
( z = r &amp; 0 < r &amp; r < 1 ) &amp; u in M &amp; v in M holds
(z * u) + ((1r - z) * v) in M );

theorem :: CONVEX4:45
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
for M being Subset of V
for z being Complex st M is convex holds
z * M is convex
proofend;

theorem :: CONVEX4:46
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
for M, N being Subset of V st M is convex &amp; N is convex holds
M + N is convex
proofend;

theorem :: CONVEX4:47
for V being ComplexLinearSpace
for M, N being Subset of V st M is convex &amp; N is convex holds
M - N is convex
proofend;

theorem Th48: :: CONVEX4:48
for V being non empty CLSStruct
for M being Subset of V holds
( M is convex iff for z being Complex st ex r being Real st
( z = r &amp; 0 < r &amp; r < 1 ) holds
(z * M) + ((1r - z) * M) c= M )
proofend;

theorem :: CONVEX4:49
for V being non empty Abelian CLSStruct
for M being Subset of V st M is convex holds
for z being Complex st ex r being Real st
( z = r &amp; 0 < r &amp; r < 1 ) holds
((1r - z) * M) + (z * M) c= M
proofend;

theorem :: CONVEX4:50
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
for M, N being Subset of V st M is convex &amp; N is convex holds
for z being Complex holds (z * M) + ((1r - z) * N) is convex
proofend;

theorem Th51: :: CONVEX4:51
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
for M being Subset of V holds 1r * M = M
proofend;

theorem Th52: :: CONVEX4:52
for V being ComplexLinearSpace
for M being non empty Subset of V holds 0c * M = {(0. V)}
proofend;

theorem :: CONVEX4:53
for V being non empty add-associative addLoopStr
for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3)
proofend;

theorem Th54: :: CONVEX4:54
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
for M being Subset of V
for z1, z2 being Complex holds z1 * (z2 * M) = (z1 * z2) * M
proofend;

theorem Th55: :: CONVEX4:55
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
for M1, M2 being Subset of V
for z being Complex holds z * (M1 + M2) = (z * M1) + (z * M2)
proofend;

theorem :: CONVEX4:56
for V being ComplexLinearSpace
for M being Subset of V
for v being VECTOR of V holds
( M is convex iff v + M is convex )
proofend;

theorem :: CONVEX4:57
for V being ComplexLinearSpace holds Up ((0). V) is convex
proofend;

theorem :: CONVEX4:58
for V being ComplexLinearSpace holds Up ((Omega). V) is convex
proofend;

theorem Th59: :: CONVEX4:59
for V being non empty CLSStruct
for M being Subset of V st M = {} holds
M is convex
proofend;

theorem Th60: :: CONVEX4:60
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
for M1, M2 being Subset of V
for z1, z2 being Complex st M1 is convex &amp; M2 is convex holds
(z1 * M1) + (z2 * M2) is convex
proofend;

theorem Th61: :: CONVEX4:61
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
for M being Subset of V
for z1, z2 being Complex holds (z1 + z2) * M c= (z1 * M) + (z2 * M)
proofend;

theorem Th62: :: CONVEX4:62
for V being non empty CLSStruct
for M, N being Subset of V
for z being Complex st M c= N holds
z * M c= z * N
proofend;

theorem Th63: :: CONVEX4:63
for V being non empty CLSStruct
for M being empty Subset of V
for z being Complex holds z * M = {}
proofend;

theorem Th64: :: CONVEX4:64
for V being non empty addLoopStr
for M being empty Subset of V
for N being Subset of V holds M + N = {}
proofend;

theorem Th65: :: CONVEX4:65
for V being non empty right_zeroed addLoopStr
for M being Subset of V holds M + {(0. V)} = M
proofend;

Lm2:  for V being ComplexLinearSpace
for M being Subset of V
for z1, z2 being Complex st ex r1, r2 being Real st
( z1 = r1 &amp; z2 = r2 &amp; r1 >= 0 &amp; r2 >= 0 ) &amp; M is convex holds
(z1 * M) + (z2 * M) c= (z1 + z2) * M
proofend;

theorem :: CONVEX4:66
for V being ComplexLinearSpace
for M being Subset of V
for z1, z2 being Complex st ex r1, r2 being Real st
( z1 = r1 &amp; z2 = r2 &amp; r1 >= 0 &amp; r2 >= 0 ) &amp; M is convex holds
(z1 * M) + (z2 * M) = (z1 + z2) * M
proofend;

theorem :: CONVEX4:67
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
for M1, M2, M3 being Subset of V
for z1, z2, z3 being Complex st M1 is convex &amp; M2 is convex &amp; M3 is convex holds
((z1 * M1) + (z2 * M2)) + (z3 * M3) is convex
proofend;

theorem Th68: :: CONVEX4:68
for V being non empty CLSStruct
for F being Subset-Family of V st ( for M being Subset of V st M in F holds
M is convex ) holds
meet F is convex
proofend;

theorem Th69: :: CONVEX4:69
for V being non empty CLSStruct
for M being Subset of V st M is Affine holds
M is convex
proofend;

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

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

theorem :: CONVEX4:70
for V being non empty ComplexUnitarySpace-like CUNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M =  {  u where u is VECTOR of V : Re (u .|. v) >= r  }  holds
M is convex
proofend;

theorem :: CONVEX4:71
for V being non empty ComplexUnitarySpace-like CUNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M =  {  u where u is VECTOR of V : Re (u .|. v) > r  }  holds
M is convex
proofend;

theorem :: CONVEX4:72
for V being non empty ComplexUnitarySpace-like CUNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M =  {  u where u is VECTOR of V : Re (u .|. v) <= r  }  holds
M is convex
proofend;

theorem :: CONVEX4:73
for V being non empty ComplexUnitarySpace-like CUNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M =  {  u where u is VECTOR of V : Re (u .|. v) < r  }  holds
M is convex
proofend;

theorem :: CONVEX4:74
for V being non empty ComplexUnitarySpace-like CUNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M =  {  u where u is VECTOR of V : Im (u .|. v) >= r  }  holds
M is convex
proofend;

theorem :: CONVEX4:75
for V being non empty ComplexUnitarySpace-like CUNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M =  {  u where u is VECTOR of V : Im (u .|. v) > r  }  holds
M is convex
proofend;

theorem :: CONVEX4:76
for V being non empty ComplexUnitarySpace-like CUNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M =  {  u where u is VECTOR of V : Im (u .|. v) <= r  }  holds
M is convex
proofend;

theorem :: CONVEX4:77
for V being non empty ComplexUnitarySpace-like CUNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M =  {  u where u is VECTOR of V : Im (u .|. v) < r  }  holds
M is convex
proofend;

theorem :: CONVEX4:78
for V being non empty ComplexUnitarySpace-like CUNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M =  {  u where u is VECTOR of V : |.(u .|. v).| <= r  }  holds
M is convex
proofend;

theorem :: CONVEX4:79
for V being non empty ComplexUnitarySpace-like CUNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M =  {  u where u is VECTOR of V : |.(u .|. v).| < r  }  holds
M is convex
proofend;

begin

definition
let V be ComplexLinearSpace;
let L be C_Linear_Combination of V;
attrL is convex  means :Def24: :: CONVEX4:def 24
 ex F being FinSequence of the carrier of V st
( F is one-to-one &amp; rng F = Carrier L &amp; ex f being FinSequence of REAL st
( len f = len F &amp; Sum f = 1 &amp; ( for n being Nat st n in dom f holds
( f . n = L . (F . n) &amp; f . n >= 0 ) ) ) );
end;

:: deftheorem Def24 defines convex CONVEX4:def_24_:_
 for V being ComplexLinearSpace
for L being C_Linear_Combination of V holds
( L is convex iff ex F being FinSequence of the carrier of V st
( F is one-to-one &amp; rng F = Carrier L &amp; ex f being FinSequence of REAL st
( len f = len F &amp; Sum f = 1 &amp; ( for n being Nat st n in dom f holds
( f . n = L . (F . n) &amp; f . n >= 0 ) ) ) ) );

theorem Th80: :: CONVEX4:80
for V being ComplexLinearSpace
for L being C_Linear_Combination of V st L is convex holds
Carrier L <> {}
proofend;

theorem :: CONVEX4:81
for V being ComplexLinearSpace
for L being C_Linear_Combination of V
for v being VECTOR of V st L is convex &amp; ex r being Real st
( r = L . v &amp; r <= 0 ) holds
not v in Carrier L
proofend;

theorem :: CONVEX4:82
for V being ComplexLinearSpace
for L being C_Linear_Combination of V st L is convex holds
L <> ZeroCLC V
proofend;

theorem Th83: :: CONVEX4:83
for V being ComplexLinearSpace
for v being VECTOR of V
for L being C_Linear_Combination of V st L is convex &amp; Carrier L = {v} holds
( ex r being Real st
( r = L . v &amp; r = 1 ) &amp; Sum L = (L . v) * v )
proofend;

theorem Th84: :: CONVEX4:84
for V being ComplexLinearSpace
for v1, v2 being VECTOR of V
for L being C_Linear_Combination of V st L is convex &amp; Carrier L = {v1,v2} &amp; v1 <> v2 holds
( ex r1, r2 being Real st
( r1 = L . v1 &amp; r2 = L . v2 &amp; r1 + r2 = 1 &amp; r1 >= 0 &amp; r2 >= 0 ) &amp; Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
proofend;

Lm3:  for V being ComplexLinearSpace
for v1, v2, v3 being VECTOR of V
for L being C_Linear_Combination of {v1,v2,v3} st v1 <> v2 &amp; v2 <> v3 &amp; v3 <> v1 holds
Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
proofend;

theorem Th85: :: CONVEX4:85
for V being ComplexLinearSpace
for v1, v2, v3 being VECTOR of V
for L being C_Linear_Combination of V st L is convex &amp; Carrier L = {v1,v2,v3} &amp; v1 <> v2 &amp; v2 <> v3 &amp; v3 <> v1 holds
( ex r1, r2, r3 being real number st
( r1 = L . v1 &amp; r2 = L . v2 &amp; r3 = L . v3 &amp; (r1 + r2) + r3 = 1 &amp; r1 >= 0 &amp; r2 >= 0 &amp; r3 >= 0 ) &amp; Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )
proofend;

theorem :: CONVEX4:86
for V being ComplexLinearSpace
for v being VECTOR of V
for L being C_Linear_Combination of {v} st L is convex holds
( ex r being Real st
( r = L . v &amp; r = 1 ) &amp; Sum L = (L . v) * v )
proofend;

theorem :: CONVEX4:87
for V being ComplexLinearSpace
for v1, v2 being VECTOR of V
for L being C_Linear_Combination of {v1,v2} st v1 <> v2 &amp; L is convex holds
( ex r1, r2 being real number st
( r1 = L . v1 &amp; r2 = L . v2 &amp; r1 >= 0 &amp; r2 >= 0 ) &amp; Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
proofend;

theorem :: CONVEX4:88
for V being ComplexLinearSpace
for v1, v2, v3 being VECTOR of V
for L being C_Linear_Combination of {v1,v2,v3} st v1 <> v2 &amp; v2 <> v3 &amp; v3 <> v1 &amp; L is convex holds
( ex r1, r2, r3 being real number st
( r1 = L . v1 &amp; r2 = L . v2 &amp; r3 = L . v3 &amp; (r1 + r2) + r3 = 1 &amp; r1 >= 0 &amp; r2 >= 0 &amp; r3 >= 0 ) &amp; Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )
proofend;

begin

definition
let V be non empty CLSStruct ;
let M be Subset of V;
func Convex-Family M ->  Subset-Family of V means :Def25: :: CONVEX4:def 25
 for N being Subset of V holds
( N in it iff ( N is convex &amp; M c= N ) );
existence
 ex b1 being Subset-Family of V st
for N being Subset of V holds
( N in b1 iff ( N is convex &amp; M c= N ) )
proofend;
uniqueness
 for b1, b2 being Subset-Family of V st ( for N being Subset of V holds
( N in b1 iff ( N is convex &amp; M c= N ) ) ) &amp; ( for N being Subset of V holds
( N in b2 iff ( N is convex &amp; M c= N ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def25 defines Convex-Family CONVEX4:def_25_:_
 for V being non empty CLSStruct
for M being Subset of V
for b3 being Subset-Family of V holds
( b3 = Convex-Family M iff for N being Subset of V holds
( N in b3 iff ( N is convex &amp; M c= N ) ) );

definition
let V be non empty CLSStruct ;
let M be Subset of V;
func conv M ->  convex Subset of V equals :: CONVEX4:def 26
 meet (Convex-Family M);
coherence
 meet (Convex-Family M) is convex Subset of V
proofend;
end;

:: deftheorem  defines conv CONVEX4:def_26_:_
 for V being non empty CLSStruct
for M being Subset of V holds conv M = meet (Convex-Family M);

theorem :: CONVEX4:89
for V being non empty CLSStruct
for M being Subset of V
for N being convex Subset of V st M c= N holds
conv M c= N
proofend;