:: Convex Sets and Convex Combinations on Complex Linear Spaces
:: by Hidenori Matsuzaki , Noboru Endou and Yasunari Shidama
::
:: Received March 3, 2008
:: Copyright (c) 2008-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, STRUCT_0, SUBSET_1, FUNCT_2, FINSET_1,
FUNCT_1, CARD_1, FUNCOP_1, COMPLEX1, ALGSTR_0, RLVECT_2, TARSKI, NAT_1,
CLVECT_1, FINSEQ_1, VALUED_1, RELAT_1, PARTFUN1, XXREAL_0, RLVECT_1,
CARD_3, SUPINF_2, RLSUB_1, ARYTM_3, ARYTM_1, QC_LANG1, BINOP_1, ZFMISC_1,
RUSUB_4, REAL_1, REALSET1, XCMPLX_0, CONVEX1, SETFAM_1, CSSPACE, PROB_2,
CONVEX4, PRE_POLY, FUNCT_7;
notations TARSKI, XBOOLE_0, ENUMSET1, DOMAIN_1, ZFMISC_1, SUBSET_1, RELAT_1,
FUNCT_1, PRE_POLY, RELSET_1, FUNCT_2, FINSEQ_1, FINSEQ_4, ALGSTR_0,
RLVECT_1, SETFAM_1, STRUCT_0, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0,
FINSET_1, PARTFUN1, FUNCOP_1, CARD_1, VALUED_1, XCMPLX_0, COMPLEX1,
RVSUM_1, RUSUB_4, RUSUB_5, BINOP_1, REAL_1, RLVECT_2, CLVECT_1, CSSPACE,
REALSET1;
constructors SETFAM_1, BINOP_1, FUNCOP_1, REAL_1, FINSEQ_4, COMPLEX1,
REALSET1, BINOP_2, FINSOP_1, RVSUM_1, RLVECT_2, RUSUB_5, CSSPACE,
RELSET_1;
registrations STRUCT_0, MEMBERED, XXREAL_0, CSSPACE, RLVECT_1, RELSET_1,
FINSET_1, XREAL_0, SUBSET_1, XCMPLX_0, CLVECT_1, NUMBERS, NAT_1, FUNCT_2,
VALUED_1, VALUED_0, CARD_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Complex Linear Combinations
definition
let V be non empty 1-sorted;
mode C_Linear_Combination of V -> Element of Funcs(the carrier of V, COMPLEX)
means
:: 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;
end;
notation
let V be non empty addLoopStr,
L be Element of Funcs(the carrier of V,COMPLEX);
synonym Carrier L for support L;
end;
definition
let V be non empty addLoopStr,
L be Element of Funcs(the carrier of V,COMPLEX);
redefine func Carrier L -> Subset of V equals
:: CONVEX4:def 2
{v where v is Element of V : L.v <> 0c};
end;
registration
let V be non empty addLoopStr, L be C_Linear_Combination of V;
cluster Carrier L -> finite;
end;
theorem :: CONVEX4:1
for V be non empty addLoopStr, L be C_Linear_Combination of V, v
be Element of V holds L.v = 0c iff not v in Carrier L;
definition
let V be non empty addLoopStr;
func ZeroCLC V -> C_Linear_Combination of V means
:: CONVEX4:def 3
Carrier it = {};
end;
registration
let V be non empty addLoopStr;
cluster Carrier ZeroCLC V -> empty;
end;
theorem :: CONVEX4:2
for V be non empty addLoopStr, v be Element of V holds (ZeroCLC V ).v = 0c;
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
:: CONVEX4:def 4
Carrier it c= A;
end;
theorem :: CONVEX4:3
for V be non empty addLoopStr, A,B be Subset of V, l be
C_Linear_Combination of A st A c= B holds l is C_Linear_Combination of B;
theorem :: CONVEX4:4
for V be non empty addLoopStr, A be Subset of V holds ZeroCLC V
is C_Linear_Combination of A;
theorem :: CONVEX4:5
for V being non empty addLoopStr, l being C_Linear_Combination of
{}the carrier of V holds l = ZeroCLC V;
reserve x,y for set,
i for Nat;
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;
func f (#) F -> FinSequence of the carrier of V means
:: CONVEX4:def 5
len it = len F & for i st i in dom it holds it.i = f.(F/.i) * F/.i;
end;
reserve V for non empty CLSStruct,
u,v,v1,v2,v3 for VECTOR of V,
A for Subset of V,
l, l1, l2 for C_Linear_Combination of A,
x,y,y1,y2 for set,
a,b for Complex,
F for FinSequence of the carrier of V,
f for Function of the carrier of V, COMPLEX;
theorem :: CONVEX4:6
x in dom F & v = F.x implies (f (#) F).x = f.v * v;
theorem :: CONVEX4:7
f (#) <*>(the carrier of V) = <*>(the carrier of V);
theorem :: CONVEX4:8
f (#) <* v *> = <* f.v * v *>;
theorem :: CONVEX4:9
f (#) <* v1,v2 *> = <* f.v1 * v1, f.v2 * v2 *>;
theorem :: CONVEX4:10
f (#) <* v1,v2,v3 *> = <* f.v1 * v1, f.v2 * v2, f.v3 * v3 *>;
reserve K,L,L1,L2,L3 for C_Linear_Combination of V;
definition
let V be Abelian add-associative right_zeroed right_complementable non empty
CLSStruct;
let L be C_Linear_Combination of V;
func Sum L -> Element of V means
:: CONVEX4:def 6
ex F being FinSequence of the
carrier of V st F is one-to-one & rng F = Carrier L & it = Sum(L (#) F);
end;
theorem :: CONVEX4:11
for V being Abelian add-associative right_zeroed
right_complementable non empty CLSStruct holds Sum(ZeroCLC V) = 0.V;
theorem :: CONVEX4:12
for V being ComplexLinearSpace, A being Subset of V holds A <> {}
implies ( A is linearly-closed iff for l being C_Linear_Combination of A holds
Sum l in A );
theorem :: CONVEX4:13
for V being Abelian add-associative right_zeroed right_complementable
non empty CLSStruct, l being C_Linear_Combination of {}(the carrier of V) holds
Sum l = 0.V;
theorem :: CONVEX4:14
for V being ComplexLinearSpace, v being VECTOR of V, l being
C_Linear_Combination of {v} holds Sum l = l.v * v;
theorem :: CONVEX4:15
for V being ComplexLinearSpace, v1, v2 being VECTOR of V holds
v1 <> v2 implies for l being C_Linear_Combination of {v1,v2} holds Sum l = l.v1
* v1 + l.v2 * v2;
theorem :: CONVEX4:16
for V being Abelian add-associative right_zeroed right_complementable
non empty CLSStruct, L being C_Linear_Combination of V holds Carrier L = {}
implies Sum L = 0.V;
theorem :: CONVEX4:17
for V being ComplexLinearSpace, L being C_Linear_Combination of V, v
being VECTOR of V holds Carrier L = {v} implies Sum L = L.v * v;
theorem :: CONVEX4:18
for V being ComplexLinearSpace, L being C_Linear_Combination of
V, v1, v2 being VECTOR of V holds Carrier L = {v1,v2} & v1 <> v2 implies Sum L
= L.v1 * v1 + L.v2 * v2;
definition
let V be non empty addLoopStr;
let L1,L2 be C_Linear_Combination of V;
redefine pred L1 = L2 means
:: CONVEX4:def 7
for v being Element of V holds L1.v = L2.v;
end;
definition
let V be non empty addLoopStr;
let L1,L2 be C_Linear_Combination of V;
redefine func L1 + L2 -> C_Linear_Combination of V means
:: CONVEX4:def 8
for v being Element of V holds it.v = L1.v + L2.v;
end;
theorem :: CONVEX4:19
Carrier(L1 + L2) c= Carrier L1 \/ Carrier L2;
theorem :: CONVEX4:20
L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of
A implies L1 + L2 is C_Linear_Combination of A;
definition
let V,A;
let L1,L2 be C_Linear_Combination of A;
redefine func L1 + L2 -> C_Linear_Combination of A;
end;
theorem :: CONVEX4:21
for V be non empty addLoopStr, L1,L2 be C_Linear_Combination of V
holds L1 + L2 = L2 + L1;
theorem :: CONVEX4:22
L1 + (L2 + L3) = L1 + L2 + L3;
theorem :: CONVEX4:23
L + ZeroCLC V = L;
definition
let V; let a be Complex;
let L;
func a * L -> C_Linear_Combination of V means
:: CONVEX4:def 9
for v holds it.v = a * L.v;
end;
theorem :: CONVEX4:24
a <> 0c implies Carrier (a * L) = Carrier L;
theorem :: CONVEX4:25
0c * L = ZeroCLC V;
theorem :: CONVEX4:26
L is C_Linear_Combination of A implies a * L is C_Linear_Combination of A;
theorem :: CONVEX4:27
(a + b) * L = a * L + b * L;
theorem :: CONVEX4:28
a * (L1 + L2) = a * L1 + a * L2;
theorem :: CONVEX4:29
a * (b * L) = (a * b) * L;
theorem :: CONVEX4:30
1r * L = L;
definition
let V,L;
func - L -> C_Linear_Combination of V equals
:: CONVEX4:def 10
(- 1r) * L;
end;
theorem :: CONVEX4:31
(- L).v = - L.v;
theorem :: CONVEX4:32
L1 + L2 = ZeroCLC V implies L2 = - L1;
theorem :: CONVEX4:33
- (- L) = L;
definition
let V;
let L1,L2;
func L1 - L2 -> C_Linear_Combination of V equals
:: CONVEX4:def 11
L1 + (- L2);
end;
theorem :: CONVEX4:34
(L1 - L2).v = L1.v - L2.v;
theorem :: CONVEX4:35
Carrier(L1 - L2) c= Carrier L1 \/ Carrier L2;
theorem :: CONVEX4:36
L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A
implies L1 - L2 is C_Linear_Combination of A;
theorem :: CONVEX4:37
L - L = ZeroCLC V;
definition
let V;
func C_LinComb V -> set means
:: CONVEX4:def 12
x in it iff x is C_Linear_Combination of V;
end;
registration
let V;
cluster C_LinComb V -> non empty;
end;
reserve e,e1,e2 for Element of C_LinComb V;
definition
let V;
let e;
func @e -> C_Linear_Combination of V equals
:: CONVEX4:def 13
e;
end;
definition
let V;
let L;
func @L -> Element of C_LinComb V equals
:: CONVEX4:def 14
L;
end;
definition
let V;
func C_LCAdd V -> BinOp of C_LinComb V means
:: CONVEX4:def 15
for e1,e2 holds it.(e1, e2) = @e1 + @e2;
end;
definition
let V;
func C_LCMult V -> Function of [:COMPLEX,C_LinComb V:], C_LinComb V means
:: CONVEX4:def 16
for a,e holds it.[a,e] = a * @e;
end;
definition
let V;
func LC_CLSpace V -> ComplexLinearSpace equals
:: CONVEX4:def 17
CLSStruct (# C_LinComb V, @
ZeroCLC V, C_LCAdd V, C_LCMult V #);
end;
registration
let V;
cluster LC_CLSpace V -> strict non empty;
end;
theorem :: CONVEX4:38
vector(LC_CLSpace V,L1) + vector(LC_CLSpace V,L2) = L1 + L2;
theorem :: CONVEX4:39
a * vector(LC_CLSpace V,L) = a * L;
theorem :: CONVEX4:40
- vector(LC_CLSpace V,L) = - L;
theorem :: CONVEX4:41
vector(LC_CLSpace V,L1) - vector(LC_CLSpace V,L2) = L1 - L2;
definition
let V;
let A;
func LC_CLSpace A -> strict Subspace of LC_CLSpace V means
:: CONVEX4:def 18
the carrier of it = the set of all l ;
end;
begin :: Preliminaries for Complex Convex Sets
definition
let V be ComplexLinearSpace, W be Subspace of V;
func Up W -> Subset of V equals
:: CONVEX4:def 19
the carrier of W;
end;
registration
let V be ComplexLinearSpace, W be Subspace of V;
cluster Up W -> non empty;
end;
definition
let V be non empty CLSStruct, S be Subset of V;
attr S is Affine means
:: CONVEX4:def 20
for x,y being VECTOR of V, z being Complex st
z is Real & x in S & y in S holds (1r - z) * x + z * y in S;
end;
definition
let V be ComplexLinearSpace;
func (Omega).V -> strict Subspace of V equals
:: CONVEX4:def 21
the CLSStruct of V;
end;
registration
let V be non empty CLSStruct;
cluster [#]V -> Affine;
cluster empty -> Affine for Subset of V;
end;
registration
let V be non empty CLSStruct;
cluster non empty Affine for Subset of V;
cluster empty Affine for Subset of V;
end;
theorem :: CONVEX4:42
for a being Real, z being Complex holds Re(a*z)=a* Re(z);
theorem :: CONVEX4:43
for a being Real, z being Complex holds Im(a*z) = a*Im(z);
theorem :: CONVEX4:44
for a being Real , z being Complex st 0<=a & a<=1
holds |.a*z.| = a*|.z.| & |.(1r-a)*z.| = (1r-a)*|.z.|;
begin :: Complex Convex Sets
definition
let V be non empty CLSStruct;
let M be Subset of V;
let r be Complex;
func r*M -> Subset of V equals
:: CONVEX4:def 22
{r * v where v is Element of V: v in M};
end;
definition
let V be non empty CLSStruct;
let M be Subset of V;
attr M is convex means
:: CONVEX4:def 23
for u,v being VECTOR of V, z be Complex st
(ex r be Real st z=r & 0 < r & r < 1 ) & u in M & v in M holds
z*u + (1r-z)*v in M;
end;
theorem :: CONVEX4:45
for V being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty CLSStruct, M being
Subset of V, z being Complex st M is convex holds z*M is convex;
theorem :: CONVEX4:46
for V being Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty
CLSStruct, M,N being Subset of V st M is convex & N is convex holds M + N is
convex;
theorem :: CONVEX4:47
for V being ComplexLinearSpace, M,N being Subset of V st M is convex &
N is convex holds M - N is convex;
theorem :: CONVEX4:48
for V being non empty CLSStruct, M being Subset of V holds M is
convex iff for z being Complex st (ex r being Real st z=r & 0 < r & r < 1)
holds z*M + (1r-z)*M c= M;
theorem :: CONVEX4:49
for V being Abelian non empty CLSStruct, M being Subset of V st M is
convex holds for z being Complex st (ex r being Real st z=r & 0 < r & r < 1)
holds (1r-z)*M + z*M c= M;
theorem :: CONVEX4:50
for V being Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty
CLSStruct, M,N being Subset of V st M is convex & N is convex holds for z
being Complex holds z*M + (1r-z)*N is convex;
theorem :: CONVEX4:51
for V being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty CLSStruct, M be
Subset of V holds 1r*M = M;
theorem :: CONVEX4:52
for V being ComplexLinearSpace, M be non empty Subset of V holds
0c * M = {0.V};
::$CT
theorem :: CONVEX4:54
for V being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty CLSStruct, M
being Subset of V, z1,z2 being Complex holds z1*(z2*M) = (z1*z2)*M;
theorem :: CONVEX4:55
for V being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty CLSStruct, M1,M2
being Subset of V, z being Complex holds z*(M1 + M2) = z*M1 + z*M2;
theorem :: CONVEX4:56
for V being ComplexLinearSpace, M being Subset of V, v being VECTOR of
V holds M is convex iff v + M is convex;
theorem :: CONVEX4:57
for V being ComplexLinearSpace holds Up((0).V) is convex;
theorem :: CONVEX4:58
for V being ComplexLinearSpace holds Up((Omega).V) is convex;
theorem :: CONVEX4:59
for V being non empty CLSStruct, M being Subset of V st M = {}
holds M is convex;
theorem :: CONVEX4:60
for V being Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non
empty CLSStruct, M1,M2 being Subset of V, z1,z2 being Complex st M1 is convex
& M2 is convex holds z1*M1 + z2*M2 is convex;
theorem :: CONVEX4:61
for V being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty CLSStruct, M
being Subset of V, z1,z2 being Complex holds (z1 + z2)*M c= z1*M + z2*M;
theorem :: CONVEX4:62
for V being non empty CLSStruct, M,N being Subset of V, z being
Complex st M c= N holds z*M c= z*N;
theorem :: CONVEX4:63
for V being non empty CLSStruct, M being empty Subset of V, z
being Complex holds z * M = {};
::$CT 2
theorem :: CONVEX4:66
for V being ComplexLinearSpace, M being Subset of V, z1,z2 being
Complex st (ex r1,r2 being Real st z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0) & M
is convex holds z1*M + z2*M = (z1 + z2)*M;
theorem :: CONVEX4:67
for V being Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty
CLSStruct, M1,M2,M3 being Subset of V, z1,z2,z3 being Complex st M1 is convex
& M2 is convex & M3 is convex holds z1*M1 + z2*M2 + z3*M3 is convex;
theorem :: CONVEX4:68
for V being non empty CLSStruct, 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;
theorem :: CONVEX4:69
for V being non empty CLSStruct, M being Subset of V st M is
Affine holds M is convex;
registration
let V be non empty CLSStruct;
cluster non empty convex for Subset of V;
end;
registration
let V be non empty CLSStruct;
cluster empty convex for Subset of V;
end;
theorem :: CONVEX4:70
for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
: Re(u .|. v) >= r } holds M is convex;
theorem :: CONVEX4:71
for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
: Re(u .|. v) > r } holds M is convex;
theorem :: CONVEX4:72
for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
: Re(u .|. v) <= r } holds M is convex;
theorem :: CONVEX4:73
for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
: Re(u .|. v) < r } holds M is convex;
theorem :: CONVEX4:74
for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
: Im(u .|. v) >= r } holds M is convex;
theorem :: CONVEX4:75
for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
: Im(u .|. v) > r } holds M is convex;
theorem :: CONVEX4:76
for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
: Im(u .|. v) <= r } holds M is convex;
theorem :: CONVEX4:77
for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
: Im(u .|. v) < r } holds M is convex;
theorem :: CONVEX4:78
for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
: |.u .|. v .| <= r } holds M is convex;
theorem :: CONVEX4:79
for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
: |.u .|. v .| < r } holds M is convex;
begin :: Complex Convex Combinations
definition
let V be ComplexLinearSpace, L be C_Linear_Combination of V;
attr L is convex means
:: CONVEX4:def 24
ex F being FinSequence of the carrier of V st
F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st len f =
len F & Sum f = 1 & for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >=
0;
end;
theorem :: CONVEX4:80
for V being ComplexLinearSpace, L being C_Linear_Combination of
V st L is convex holds Carrier L <> {};
theorem :: CONVEX4:81
for V being ComplexLinearSpace, L being C_Linear_Combination of V, v
being VECTOR of V st L is convex & ( ex r being Real st r = L.v & r <= 0 )
holds not v in Carrier L;
theorem :: CONVEX4:82
for V being ComplexLinearSpace, L being C_Linear_Combination of V st L
is convex holds L <> ZeroCLC V;
theorem :: CONVEX4:83
for V being ComplexLinearSpace, v being VECTOR of V, L being
C_Linear_Combination of V st L is convex & Carrier L = {v} holds ( ex r being
Real st r = L.v & r = 1 ) & Sum L = L.v * v;
theorem :: CONVEX4:84
for V being ComplexLinearSpace, v1,v2 being VECTOR of V, L being
C_Linear_Combination of V st L is convex & Carrier L = {v1,v2} & v1 <> v2 holds
( ex r1, r2 being Real st r1 = L.v1 & r2 = L.v2 & r1 + r2 = 1 & r1 >= 0 & r2 >=
0 ) & Sum L = L.v1 * v1 + L.v2 * v2;
theorem :: CONVEX4:85
for V being ComplexLinearSpace, v1,v2,v3 being VECTOR of V, L
being C_Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <>
v2 & v2 <> v3 & v3 <> v1 holds ( ex r1, r2, r3 being Real st r1 = L.v1 &
r2 = L.v2 & r3 = L.v3 & r1 + r2 + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & Sum
L = L.v1 * v1 + L.v2 * v2 + L.v3 * v3;
theorem :: CONVEX4:86
for V being ComplexLinearSpace, v being VECTOR of V, L being
C_Linear_Combination of {v} st L is convex holds ( ex r being Real st r = L.v &
r = 1 ) & Sum L = L.v * v;
theorem :: CONVEX4:87
for V being ComplexLinearSpace, v1,v2 being VECTOR of V, L being
C_Linear_Combination of {v1,v2} st v1 <> v2 & L is convex holds ( ex r1, r2
being Real st r1 = L.v1 & r2 = L.v2 &r1 >= 0 & r2 >= 0 )& Sum L = L.v1 *
v1 + L.v2 * v2;
theorem :: CONVEX4:88
for V being ComplexLinearSpace, v1,v2,v3 being VECTOR of V, L being
C_Linear_Combination of {v1,v2,v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 & L is
convex holds ( ex r1, r2, r3 being Real st r1 = L.v1 & r2 = L.v2 & r3 =
L.v3 & r1 + r2 + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & Sum L = L.v1 * v1 + L
.v2 * v2 + L.v3 * v3;
begin :: Complex Convex Hull
definition
let V be non empty CLSStruct, M be Subset of V;
func Convex-Family M -> Subset-Family of V means
:: CONVEX4:def 25
for N being Subset of V holds N in it iff N is convex & M c= N;
end;
definition
let V be non empty CLSStruct, M be Subset of V;
func conv M -> convex Subset of V equals
:: CONVEX4:def 26
meet (Convex-Family M);
end;
theorem :: CONVEX4:89
for V being non empty CLSStruct, M being Subset of V, N being convex
Subset of V st M c= N holds conv M c= N;