begin
:: deftheorem Def1 defines C_Linear_Combination CONVEX4:def 1 :
:: deftheorem defines Carrier CONVEX4:def 2 :
theorem Th1:
:: deftheorem Def3 defines ZeroCLC CONVEX4:def 3 :
theorem Th2:
:: deftheorem Def4 defines C_Linear_Combination CONVEX4:def 4 :
theorem
theorem Th4:
theorem Th5:
:: deftheorem Def5 defines (#) CONVEX4:def 5 :
theorem Th6:
theorem
theorem Th8:
theorem Th9:
theorem Th10:
:: deftheorem Def6 defines Sum CONVEX4:def 6 :
theorem Th11:
theorem
theorem
theorem Th14:
theorem Th15:
theorem
theorem
theorem Th18:
:: deftheorem defines = CONVEX4:def 7 :
:: deftheorem Def8 defines + CONVEX4:def 8 :
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem Th23:
:: deftheorem Def9 defines * CONVEX4:def 9 :
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
:: deftheorem defines - CONVEX4:def 10 :
theorem Th31:
theorem
theorem
:: deftheorem defines - CONVEX4:def 11 :
theorem Th34:
theorem
theorem
theorem Th37:
:: deftheorem Def12 defines C_LinComb CONVEX4:def 12 :
:: deftheorem defines @ CONVEX4:def 13 :
:: deftheorem defines @ CONVEX4:def 14 :
:: deftheorem Def15 defines C_LCAdd CONVEX4:def 15 :
definition
let V be non
empty CLSStruct ;
func C_LCMult V -> Function of
[:COMPLEX ,(C_LinComb V):],
(C_LinComb V) means :
Def16:
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)
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) ) & ( for a being Complex
for e being Element of C_LinComb V holds b2 . [a,e] = a * (@ e) ) holds
b1 = b2
end;
:: deftheorem Def16 defines C_LCMult CONVEX4:def 16 :
:: deftheorem defines LC_CLSpace CONVEX4:def 17 :
theorem Th38:
theorem Th39:
theorem Th40:
theorem
:: deftheorem defines LC_CLSpace CONVEX4:def 18 :
begin
:: deftheorem defines Up CONVEX4:def 19 :
:: deftheorem Def20 defines Affine CONVEX4:def 20 :
:: deftheorem defines (Omega). CONVEX4:def 21 :
theorem Th42:
theorem Th43:
theorem Th44:
begin
:: deftheorem defines * CONVEX4:def 22 :
:: deftheorem Def23 defines convex CONVEX4:def 23 :
theorem
theorem
theorem
theorem Th48:
theorem
theorem
theorem Th51:
theorem Th52:
theorem
theorem Th54:
theorem Th55:
theorem
theorem
theorem
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
Lm1:
for V being ComplexLinearSpace
for M being Subset of V
for 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) c= (z1 + z2) * M
theorem
theorem
theorem Th68:
theorem Th69:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem Def24 defines convex CONVEX4:def 24 :
theorem Th80:
theorem
theorem
theorem Th83:
theorem Th84:
Lm2:
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 & v2 <> v3 & v3 <> v1 holds
Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
theorem Th85:
theorem
theorem
theorem
begin
:: deftheorem Def25 defines Convex-Family CONVEX4:def 25 :
:: deftheorem defines conv CONVEX4:def 26 :
theorem