:: 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 Def2 defines ZeroCLC CONVEX4:def 3 :
theorem Th30: :: CONVEX4:2
:: deftheorem Def3 defines C_Linear_Combination CONVEX4:def 4 :
theorem :: CONVEX4:3
theorem Th34: :: CONVEX4:4
theorem Th35: :: CONVEX4:5
:: deftheorem Def4 defines (#) CONVEX4:def 5 :
theorem Th40: :: CONVEX4:6
theorem :: CONVEX4:7
theorem Th42: :: CONVEX4:8
theorem Th43: :: CONVEX4:9
theorem Th44: :: CONVEX4:10
:: deftheorem Def5 defines Sum CONVEX4:def 6 :
theorem Lm2: :: CONVEX4:11
theorem :: CONVEX4:12
theorem :: CONVEX4:13
theorem Th50: :: CONVEX4:14
theorem Th51: :: CONVEX4:15
theorem :: CONVEX4:16
theorem :: CONVEX4:17
theorem Th54: :: CONVEX4:18
:: deftheorem defines = CONVEX4:def 7 :
:: deftheorem Def6 defines + CONVEX4:def 8 :
theorem Th58: :: CONVEX4:19
theorem Th59: :: CONVEX4:20
theorem :: CONVEX4:21
theorem Th61: :: CONVEX4:22
theorem Th62: :: CONVEX4:23
:: deftheorem Def7 defines * CONVEX4:def 9 :
theorem Th65: :: CONVEX4:24
theorem Th66: :: CONVEX4:25
theorem Th67: :: CONVEX4:26
theorem Th68: :: CONVEX4:27
theorem Th69: :: CONVEX4:28
theorem Th70: :: CONVEX4:29
theorem Th71: :: CONVEX4:30
:: deftheorem defines - CONVEX4:def 10 :
theorem Th73: :: CONVEX4:31
theorem :: CONVEX4:32
theorem :: CONVEX4:33
:: deftheorem defines - CONVEX4:def 11 :
theorem Th79: :: CONVEX4:34
theorem :: CONVEX4:35
theorem :: CONVEX4:36
theorem Th82: :: CONVEX4:37
:: deftheorem Def8 defines C_LinComb CONVEX4:def 12 :
:: deftheorem defines @ CONVEX4:def 13 :
:: deftheorem defines @ CONVEX4:def 14 :
:: deftheorem Def9 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 :
Def10:
:: 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 Def10 defines C_LCMult CONVEX4:def 16 :
:: deftheorem defines LC_CLSpace CONVEX4:def 17 :
theorem Th96: :: CONVEX4:38
theorem Th97: :: CONVEX4:39
theorem Th98: :: CONVEX4:40
theorem :: CONVEX4:41
:: deftheorem defines LC_CLSpace CONVEX4:def 18 :
:: deftheorem defines Up CONVEX4:def 19 :
:: deftheorem Def101 defines Affine CONVEX4:def 20 :
:: deftheorem defines (Omega). CONVEX4:def 21 :
theorem Th101: :: CONVEX4:42
theorem Th102: :: CONVEX4:43
theorem Th103: :: CONVEX4:44
:: deftheorem defines * CONVEX4:def 22 :
:: deftheorem Def202 defines convex CONVEX4:def 23 :
theorem :: CONVEX4:45
theorem :: CONVEX4:46
theorem :: CONVEX4:47
theorem Th204: :: CONVEX4:48
theorem :: CONVEX4:49
theorem :: CONVEX4:50
theorem Lm201: :: CONVEX4:51
theorem Lm202: :: CONVEX4:52
theorem :: CONVEX4:53
theorem Lm204: :: CONVEX4:54
theorem Lm205: :: CONVEX4:55
theorem :: CONVEX4:56
theorem :: CONVEX4:57
theorem :: CONVEX4:58
theorem Th210: :: CONVEX4:59
theorem Th211: :: CONVEX4:60
theorem Th212: :: CONVEX4:61
theorem Lm206: :: CONVEX4:62
theorem Lm207: :: CONVEX4:63
theorem Lm208: :: CONVEX4:64
theorem Lm209: :: CONVEX4:65
Lm210:
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 Th215: :: CONVEX4:68
theorem Th216: :: 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 Def203 defines convex CONVEX4:def 24 :
theorem Th221: :: CONVEX4:80
theorem :: CONVEX4:81
theorem :: CONVEX4:82
theorem Lm211: :: CONVEX4:83
theorem Lm212: :: CONVEX4:84
Lm214:
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 Lm215: :: CONVEX4:85
theorem :: CONVEX4:86
theorem :: CONVEX4:87
theorem :: CONVEX4:88
:: deftheorem Def204 defines Convex-Family CONVEX4:def 25 :
:: deftheorem defines conv CONVEX4:def 26 :
theorem :: CONVEX4:89