:: Convex Sets and Convex Combinations on Complex Linear Spaces
:: by Hidenori Matsuzaki , Noboru Endou and Yasunari Shidama
::
:: Received March 3, 2008
:: Copyright (c) 2008 Association of Mizar Users
:: deftheorem Def1 defines C_Linear_Combination CONVEX4:def 1 :
:: deftheorem defines Carrier CONVEX4:def 2 :
theorem Th1: :: CONVEX4:1
:: deftheorem Def3 defines ZeroCLC CONVEX4:def 3 :
theorem Th2: :: CONVEX4:2
:: deftheorem Def4 defines C_Linear_Combination CONVEX4:def 4 :
theorem :: CONVEX4:3
theorem Th4: :: CONVEX4:4
theorem Th5: :: CONVEX4:5
:: deftheorem Def5 defines (#) CONVEX4:def 5 :
theorem Th6: :: CONVEX4:6
theorem :: CONVEX4:7
theorem Th8: :: CONVEX4:8
theorem Th9: :: CONVEX4:9
theorem Th10: :: CONVEX4:10
:: deftheorem Def6 defines Sum CONVEX4:def 6 :
theorem Th11: :: CONVEX4:11
theorem :: CONVEX4:12
theorem :: CONVEX4:13
theorem Th14: :: CONVEX4:14
theorem Th15: :: CONVEX4:15
theorem :: CONVEX4:16
theorem :: CONVEX4:17
theorem Th18: :: CONVEX4:18
:: deftheorem defines = CONVEX4:def 7 :
:: deftheorem Def8 defines + CONVEX4:def 8 :
theorem Th19: :: CONVEX4:19
theorem Th20: :: CONVEX4:20
theorem :: CONVEX4:21
theorem Th22: :: CONVEX4:22
theorem Th23: :: CONVEX4:23
:: deftheorem Def9 defines * CONVEX4:def 9 :
theorem Th24: :: CONVEX4:24
theorem Th25: :: CONVEX4:25
theorem Th26: :: CONVEX4:26
theorem Th27: :: CONVEX4:27
theorem Th28: :: CONVEX4:28
theorem Th29: :: CONVEX4:29
theorem Th30: :: CONVEX4:30
:: deftheorem defines - CONVEX4:def 10 :
theorem Th31: :: CONVEX4:31
theorem :: CONVEX4:32
theorem :: CONVEX4:33
:: deftheorem defines - CONVEX4:def 11 :
theorem Th34: :: CONVEX4:34
theorem :: CONVEX4:35
theorem :: CONVEX4:36
theorem Th37: :: CONVEX4:37
:: 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:
:: 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)
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: :: CONVEX4:38
theorem Th39: :: CONVEX4:39
theorem Th40: :: CONVEX4:40
theorem :: CONVEX4:41
:: deftheorem defines LC_CLSpace CONVEX4:def 18 :
:: deftheorem defines Up CONVEX4:def 19 :
:: deftheorem Def20 defines Affine CONVEX4:def 20 :
:: deftheorem defines (Omega). CONVEX4:def 21 :
theorem Th42: :: CONVEX4:42
theorem Th43: :: CONVEX4:43
theorem Th44: :: CONVEX4:44
:: deftheorem defines * CONVEX4:def 22 :
:: deftheorem Def23 defines convex CONVEX4:def 23 :
theorem :: CONVEX4:45
theorem :: CONVEX4:46
theorem :: CONVEX4:47
theorem Th48: :: CONVEX4:48
theorem :: CONVEX4:49
theorem :: CONVEX4:50
theorem Th51: :: CONVEX4:51
theorem Th52: :: CONVEX4:52
theorem :: CONVEX4:53
theorem Th54: :: CONVEX4:54
theorem Th55: :: CONVEX4:55
theorem :: CONVEX4:56
theorem :: CONVEX4:57
theorem :: CONVEX4:58
theorem Th59: :: CONVEX4:59
theorem Th60: :: CONVEX4:60
theorem Th61: :: CONVEX4:61
theorem Th62: :: CONVEX4:62
theorem Th63: :: CONVEX4:63
theorem Th64: :: CONVEX4:64
theorem Th65: :: CONVEX4:65
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 :: CONVEX4:66
theorem :: CONVEX4:67
theorem Th68: :: CONVEX4:68
theorem Th69: :: CONVEX4:69
theorem :: CONVEX4:70
theorem :: CONVEX4:71
theorem :: CONVEX4:72
theorem :: CONVEX4:73
theorem :: CONVEX4:74
theorem :: CONVEX4:75
theorem :: CONVEX4:76
theorem :: CONVEX4:77
theorem :: CONVEX4:78
theorem :: CONVEX4:79
:: deftheorem Def24 defines convex CONVEX4:def 24 :
theorem Th80: :: CONVEX4:80
theorem :: CONVEX4:81
theorem :: CONVEX4:82
theorem Th83: :: CONVEX4:83
theorem Th84: :: CONVEX4:84
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: :: CONVEX4:85
theorem :: CONVEX4:86
theorem :: CONVEX4:87
theorem :: CONVEX4:88
:: deftheorem Def25 defines Convex-Family CONVEX4:def 25 :
:: deftheorem defines conv CONVEX4:def 26 :
theorem :: CONVEX4:89