:: by Hidenori Matsuzaki , Noboru Endou and Yasunari Shidama

::

:: Received March 3, 2008

:: Copyright (c) 2008-2018 Association of Mizar Users

definition

let V be non empty 1-sorted ;

ex b_{1} 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

b_{1} . v = 0

end;
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 T being finite Subset of V st

for v being Element of V st not v in T holds

it . v = 0 ;

ex b

for v being Element of V st not v in T holds

b

proof end;

:: deftheorem Def1 defines C_Linear_Combination CONVEX4:def 1 :

for V being non empty 1-sorted

for b_{2} being Element of Funcs ( the carrier of V,COMPLEX) holds

( b_{2} 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

b_{2} . v = 0 );

for V being non empty 1-sorted

for b

( b

for v being Element of V st not v in T holds

b

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;
let L be Element of Funcs ( the carrier of V,COMPLEX);

synonym Carrier L for support V;

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

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

end;
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 object ; :: according to TARSKI: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;
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

definition

let V be non empty addLoopStr ;

let L be Element of Funcs ( the carrier of V,COMPLEX);

Carrier is Subset of V by Lm1;

compatibility

for b_{1} being Subset of V holds

( b_{1} = Carrier iff b_{1} = { v where v is Element of V : L . v <> 0c } )

end;
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 redefine func Carrier L -> Subset of V equals :: CONVEX4:def 2

{ v where v is Element of V : L . v <> 0c } ;

Carrier is Subset of V by Lm1;

compatibility

for b

( b

proof 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 } ;

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;

coherence

Carrier L is finite

end;
let L be C_Linear_Combination of V;

coherence

Carrier L is finite

proof 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 )

for L being C_Linear_Combination of V

for v being Element of V holds

( L . v = 0c iff not v in Carrier L )

proof end;

definition

let V be non empty addLoopStr ;

existence

ex b_{1} being C_Linear_Combination of V st Carrier b_{1} = {}

for b_{1}, b_{2} being C_Linear_Combination of V st Carrier b_{1} = {} & Carrier b_{2} = {} holds

b_{1} = b_{2}

end;
existence

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines ZeroCLC CONVEX4:def 3 :

for V being non empty addLoopStr

for b_{2} being C_Linear_Combination of V holds

( b_{2} = ZeroCLC V iff Carrier b_{2} = {} );

for V being non empty addLoopStr

for b

( b

definition

let V be non empty addLoopStr ;

let A be Subset of V;

ex b_{1} being C_Linear_Combination of V st Carrier b_{1} c= A

end;
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 Carrier it c= A;

ex b

proof end;

:: deftheorem Def4 defines C_Linear_Combination CONVEX4:def 4 :

for V being non empty addLoopStr

for A being Subset of V

for b_{3} being C_Linear_Combination of V holds

( b_{3} is C_Linear_Combination of A iff Carrier b_{3} c= A );

for V being non empty addLoopStr

for A being Subset of V

for b

( b

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

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

proof end;

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

for A being Subset of V holds ZeroCLC V is C_Linear_Combination of A

proof end;

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

for l being C_Linear_Combination of {} the carrier of V holds l = ZeroCLC V

proof end;

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;

ex b_{1} being FinSequence of the carrier of V st

( len b_{1} = len F & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (f . (F /. i)) * (F /. i) ) )

for b_{1}, b_{2} being FinSequence of the carrier of V st len b_{1} = len F & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (f . (F /. i)) * (F /. i) ) & len b_{2} = len F & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = (f . (F /. i)) * (F /. i) ) holds

b_{1} = b_{2}

end;
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 :Def5: :: CONVEX4:def 5

( len it = len F & ( for i being Nat st i in dom it holds

it . i = (f . (F /. i)) * (F /. i) ) );

existence ( len it = len F & ( for i being Nat st i in dom it holds

it . i = (f . (F /. i)) * (F /. i) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{4} being FinSequence of the carrier of V holds

( b_{4} = f (#) F iff ( len b_{4} = len F & ( for i being Nat st i in dom b_{4} holds

b_{4} . i = (f . (F /. i)) * (F /. i) ) ) );

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 b

( b

b

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 & v = F . x holds

(f (#) F) . x = (f . v) * v

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 & v = F . x holds

(f (#) F) . x = (f . v) * v

proof end;

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

for f being Function of the carrier of V,COMPLEX holds f (#) (<*> the carrier of V) = <*> the carrier of V

proof end;

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)*>

for v being VECTOR of V

for f being Function of the carrier of V,COMPLEX holds f (#) <*v*> = <*((f . v) * v)*>

proof end;

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)*>

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)*>

proof end;

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)*>

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)*>

proof end;

definition

let V be non empty right_complementable Abelian add-associative right_zeroed CLSStruct ;

let L be C_Linear_Combination of V;

ex b_{1} being Element of V ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = Carrier L & b_{1} = Sum (L (#) F) )

for b_{1}, b_{2} being Element of V st ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = Carrier L & b_{1} = Sum (L (#) F) ) & ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = Carrier L & b_{2} = Sum (L (#) F) ) holds

b_{1} = b_{2}

end;
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 & rng F = Carrier L & it = Sum (L (#) F) );

existence ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = Carrier L & it = Sum (L (#) F) );

ex b

( F is one-to-one & rng F = Carrier L & b

proof end;

uniqueness for b

( F is one-to-one & rng F = Carrier L & b

( F is one-to-one & rng F = Carrier L & b

b

proof 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 b_{3} being Element of V holds

( b_{3} = Sum L iff ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = Carrier L & b_{3} = Sum (L (#) F) ) );

for V being non empty right_complementable Abelian add-associative right_zeroed CLSStruct

for L being C_Linear_Combination of V

for b

( b

( F is one-to-one & rng F = Carrier L & b

theorem Th11: :: CONVEX4:11

for V being non empty right_complementable Abelian add-associative right_zeroed CLSStruct holds Sum (ZeroCLC V) = 0. V

proof end;

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 )

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 )

proof end;

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

for l being C_Linear_Combination of {} the carrier of V holds Sum l = 0. V

proof end;

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

for v being VECTOR of V

for l being C_Linear_Combination of {v} holds Sum l = (l . v) * v

proof end;

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)

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)

proof end;

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

for L being C_Linear_Combination of V st Carrier L = {} holds

Sum L = 0. V

proof end;

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

for L being C_Linear_Combination of V

for v being VECTOR of V st Carrier L = {v} holds

Sum L = (L . v) * v

proof end;

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} & v1 <> v2 holds

Sum L = ((L . v1) * v1) + ((L . v2) * v2)

for L being C_Linear_Combination of V

for v1, v2 being VECTOR of V st Carrier L = {v1,v2} & v1 <> v2 holds

Sum L = ((L . v1) * v1) + ((L . v2) * v2)

proof end;

definition

let V be non empty addLoopStr ;

let L1, L2 be C_Linear_Combination of V;

( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v ) by FUNCT_2:63;

end;
let L1, L2 be C_Linear_Combination of V;

:: original: =

redefine pred L1 = L2 means :: CONVEX4:def 7

for v being Element of V holds L1 . v = L2 . v;

compatibility redefine pred L1 = L2 means :: CONVEX4:def 7

for v being Element of V holds L1 . v = L2 . v;

( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v ) by FUNCT_2:63;

:: 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 );

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;

L1 + L2 is C_Linear_Combination of V

for b_{1} being C_Linear_Combination of V holds

( b_{1} = L1 + L2 iff for v being Element of V holds b_{1} . v = (L1 . v) + (L2 . v) )

end;
let L1, L2 be C_Linear_Combination of V;

:: original: +

redefine func L1 + 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 redefine func L1 + L2 -> C_Linear_Combination of V means :Def8: :: CONVEX4:def 8

for v being Element of V holds it . v = (L1 . v) + (L2 . v);

L1 + L2 is C_Linear_Combination of V

proof end;

compatibility for b

( b

proof end;

:: deftheorem Def8 defines + CONVEX4:def 8 :

for V being non empty addLoopStr

for L1, L2, b_{4} being C_Linear_Combination of V holds

( b_{4} = L1 + L2 iff for v being Element of V holds b_{4} . v = (L1 . v) + (L2 . v) );

for V being non empty addLoopStr

for L1, L2, b

( b

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)

for L1, L2 being C_Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)

proof end;

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 & L2 is C_Linear_Combination of A holds

L1 + L2 is C_Linear_Combination of A

for A being Subset of V

for L1, L2 being C_Linear_Combination of V st L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A holds

L1 + L2 is C_Linear_Combination of A

proof end;

definition

let V be non empty CLSStruct ;

let A be Subset of V;

let L1, L2 be C_Linear_Combination of A;

:: original: +

redefine func L1 + L2 -> C_Linear_Combination of A;

coherence

L1 + L2 is C_Linear_Combination of A by Th20;

end;
let A be Subset of V;

let L1, L2 be C_Linear_Combination of A;

:: original: +

redefine func L1 + L2 -> C_Linear_Combination of A;

coherence

L1 + L2 is C_Linear_Combination of A by Th20;

theorem :: CONVEX4:21

for V being non empty addLoopStr

for L1, L2 being C_Linear_Combination of V holds L1 + L2 = L2 + L1 ;

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

for L1, L2, L3 being C_Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3

proof end;

definition

let V be non empty CLSStruct ;

let a be Complex;

let L be C_Linear_Combination of V;

ex b_{1} being C_Linear_Combination of V st

for v being VECTOR of V holds b_{1} . v = a * (L . v)

for b_{1}, b_{2} being C_Linear_Combination of V st ( for v being VECTOR of V holds b_{1} . v = a * (L . v) ) & ( for v being VECTOR of V holds b_{2} . v = a * (L . v) ) holds

b_{1} = b_{2}

end;
let a be Complex;

let L be C_Linear_Combination of V;

func a * L -> C_Linear_Combination of V means :Def9: :: CONVEX4:def 9

for v being VECTOR of V holds it . v = a * (L . v);

existence for v being VECTOR of V holds it . v = a * (L . v);

ex b

for v being VECTOR of V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines * CONVEX4:def 9 :

for V being non empty CLSStruct

for a being Complex

for L, b_{4} being C_Linear_Combination of V holds

( b_{4} = a * L iff for v being VECTOR of V holds b_{4} . v = a * (L . v) );

for V being non empty CLSStruct

for a being Complex

for L, b

( b

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

for a being Complex

for L being C_Linear_Combination of V st a <> 0c holds

Carrier (a * L) = Carrier L

proof end;

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

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

proof end;

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)

for a, b being Complex

for L being C_Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)

proof end;

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)

for a being Complex

for L1, L2 being C_Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)

proof end;

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

for a, b being Complex

for L being C_Linear_Combination of V holds a * (b * L) = (a * b) * L

proof end;

definition

let V be non empty CLSStruct ;

let L be C_Linear_Combination of V;

correctness

coherence

(- 1r) * L is C_Linear_Combination of V;

;

end;
let L be C_Linear_Combination of V;

correctness

coherence

(- 1r) * L is C_Linear_Combination of V;

;

:: deftheorem defines - CONVEX4:def 10 :

for V being non empty CLSStruct

for L being C_Linear_Combination of V holds - L = (- 1r) * L;

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)

for v being VECTOR of V

for L being C_Linear_Combination of V holds (- L) . v = - (L . v)

proof end;

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

for L1, L2 being C_Linear_Combination of V st L1 + L2 = ZeroCLC V holds

L2 = - L1

proof end;

definition

let V be non empty CLSStruct ;

let L1, L2 be C_Linear_Combination of V;

correctness

coherence

L1 + (- L2) is C_Linear_Combination of V;

;

end;
let L1, L2 be C_Linear_Combination of V;

correctness

coherence

L1 + (- L2) is C_Linear_Combination of V;

;

:: 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);

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)

for v being VECTOR of V

for L1, L2 being C_Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)

proof end;

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)

for L1, L2 being C_Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)

proof end;

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 & L2 is C_Linear_Combination of A holds

L1 - L2 is C_Linear_Combination of A

for A being Subset of V

for L1, L2 being C_Linear_Combination of V st L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A holds

L1 - L2 is C_Linear_Combination of A

proof end;

definition

let V be non empty CLSStruct ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is C_Linear_Combination of V )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is C_Linear_Combination of V ) ) & ( for x being set holds

( x in b_{2} iff x is C_Linear_Combination of V ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in it iff x is C_Linear_Combination of V );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def12 defines C_LinComb CONVEX4:def 12 :

for V being non empty CLSStruct

for b_{2} being set holds

( b_{2} = C_LinComb V iff for x being set holds

( x in b_{2} iff x is C_Linear_Combination of V ) );

for V being non empty CLSStruct

for b

( b

( x in b

definition

let V be non empty CLSStruct ;

let e be Element of C_LinComb V;

coherence

e is C_Linear_Combination of V by Def12;

end;
let e be Element of C_LinComb V;

coherence

e is C_Linear_Combination of V by Def12;

:: deftheorem defines @ CONVEX4:def 13 :

for V being non empty CLSStruct

for e being Element of C_LinComb V holds @ e = e;

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;

coherence

L is Element of C_LinComb V by Def12;

end;
let L be C_Linear_Combination of V;

coherence

L is Element of C_LinComb V by Def12;

:: deftheorem defines @ CONVEX4:def 14 :

for V being non empty CLSStruct

for L being C_Linear_Combination of V holds @ L = L;

for V being non empty CLSStruct

for L being C_Linear_Combination of V holds @ L = L;

definition

let V be non empty CLSStruct ;

ex b_{1} being BinOp of (C_LinComb V) st

for e1, e2 being Element of C_LinComb V holds b_{1} . (e1,e2) = (@ e1) + (@ e2)

for b_{1}, b_{2} being BinOp of (C_LinComb V) st ( for e1, e2 being Element of C_LinComb V holds b_{1} . (e1,e2) = (@ e1) + (@ e2) ) & ( for e1, e2 being Element of C_LinComb V holds b_{2} . (e1,e2) = (@ e1) + (@ e2) ) holds

b_{1} = b_{2}

end;
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 for e1, e2 being Element of C_LinComb V holds it . (e1,e2) = (@ e1) + (@ e2);

ex b

for e1, e2 being Element of C_LinComb V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def15 defines C_LCAdd CONVEX4:def 15 :

for V being non empty CLSStruct

for b_{2} being BinOp of (C_LinComb V) holds

( b_{2} = C_LCAdd V iff for e1, e2 being Element of C_LinComb V holds b_{2} . (e1,e2) = (@ e1) + (@ e2) );

for V being non empty CLSStruct

for b

( b

definition

let V be non empty CLSStruct ;

ex b_{1} being Function of [:COMPLEX,(C_LinComb V):],(C_LinComb V) st

for a being Complex

for e being Element of C_LinComb V holds b_{1} . [a,e] = a * (@ e)

for b_{1}, b_{2} being Function of [:COMPLEX,(C_LinComb V):],(C_LinComb V) st ( for a being Complex

for e being Element of C_LinComb V holds b_{1} . [a,e] = a * (@ e) ) & ( for a being Complex

for e being Element of C_LinComb V holds b_{2} . [a,e] = a * (@ e) ) holds

b_{1} = b_{2}

end;
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 for a being Complex

for e being Element of C_LinComb V holds it . [a,e] = a * (@ e);

ex b

for a being Complex

for e being Element of C_LinComb V holds b

proof end;

uniqueness for b

for e being Element of C_LinComb V holds b

for e being Element of C_LinComb V holds b

b

proof end;

:: deftheorem Def16 defines C_LCMult CONVEX4:def 16 :

for V being non empty CLSStruct

for b_{2} being Function of [:COMPLEX,(C_LinComb V):],(C_LinComb V) holds

( b_{2} = C_LCMult V iff for a being Complex

for e being Element of C_LinComb V holds b_{2} . [a,e] = a * (@ e) );

for V being non empty CLSStruct

for b

( b

for e being Element of C_LinComb V holds b

definition

let V be non empty CLSStruct ;

CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) is ComplexLinearSpace

end;
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) #);

CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) is ComplexLinearSpace

proof 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) #);

for V being non empty CLSStruct holds LC_CLSpace V = CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #);

registration
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

for L1, L2 being C_Linear_Combination of V holds (vector ((LC_CLSpace V),L1)) + (vector ((LC_CLSpace V),L2)) = L1 + L2

proof end;

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

for a being Complex

for L being C_Linear_Combination of V holds a * (vector ((LC_CLSpace V),L)) = a * L

proof end;

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

for L being C_Linear_Combination of V holds - (vector ((LC_CLSpace V),L)) = - L

proof end;

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

for L1, L2 being C_Linear_Combination of V holds (vector ((LC_CLSpace V),L1)) - (vector ((LC_CLSpace V),L2)) = L1 - L2

proof end;

definition

let V be non empty CLSStruct ;

let A be Subset of V;

ex b_{1} being strict Subspace of LC_CLSpace V st the carrier of b_{1} = { l where l is C_Linear_Combination of A : verum }

for b_{1}, b_{2} being strict Subspace of LC_CLSpace V st the carrier of b_{1} = { l where l is C_Linear_Combination of A : verum } & the carrier of b_{2} = { l where l is C_Linear_Combination of A : verum } holds

b_{1} = b_{2}
by CLVECT_1:49;

end;
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 the carrier of it = { l where l is C_Linear_Combination of A : verum } ;

ex b

proof end;

uniqueness for b

b

:: deftheorem defines LC_CLSpace CONVEX4:def 18 :

for V being non empty CLSStruct

for A being Subset of V

for b_{3} being strict Subspace of LC_CLSpace V holds

( b_{3} = LC_CLSpace A iff the carrier of b_{3} = { l where l is C_Linear_Combination of A : verum } );

for V being non empty CLSStruct

for A being Subset of V

for b

( b

definition

let V be ComplexLinearSpace;

let W be Subspace of V;

coherence

the carrier of W is Subset of V by CLVECT_1:def 8;

end;
let W be Subspace of V;

coherence

the carrier of W is Subset of V by CLVECT_1:def 8;

:: deftheorem defines Up CONVEX4:def 19 :

for V being ComplexLinearSpace

for W being Subspace of V holds Up W = the carrier of W;

for V being ComplexLinearSpace

for W being Subspace of V holds Up W = the carrier of W;

:: deftheorem 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 & x in S & y in S holds

((1r - z) * x) + (z * y) in S );

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 & x in S & y in S holds

((1r - z) * x) + (z * y) in S );

definition

let V be ComplexLinearSpace;

CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V

end;
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 #);

CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V

proof 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 #);

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 ;

coherence

[#] V is Affine ;

coherence

for b_{1} being Subset of V st b_{1} is empty holds

b_{1} is Affine
;

end;
coherence

[#] V is Affine ;

coherence

for b

b

registration

let V be non empty CLSStruct ;

existence

ex b_{1} being Subset of V st

( not b_{1} is empty & b_{1} is Affine )

ex b_{1} being Subset of V st

( b_{1} is empty & b_{1} is Affine )

end;
existence

ex b

( not b

proof end;

existence ex b

( b

proof end;

theorem Th44: :: CONVEX4:44

for a being Real

for z being Complex st 0 <= a & a <= 1 holds

( |.(a * z).| = a * |.z.| & |.((1r - a) * z).| = (1r - a) * |.z.| )

for z being Complex st 0 <= a & a <= 1 holds

( |.(a * z).| = a * |.z.| & |.((1r - a) * z).| = (1r - a) * |.z.| )

proof end;

definition

let V be non empty CLSStruct ;

let M be Subset of V;

let r be Complex;

coherence

{ (r * v) where v is Element of V : v in M } is Subset of V

end;
let M be Subset of V;

let r be Complex;

coherence

{ (r * v) where v is Element of V : v in M } is Subset of V

proof 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 } ;

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 } ;

:: deftheorem 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 & 0 < r & r < 1 ) & u in M & v in M holds

(z * u) + ((1r - z) * v) in M );

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 & 0 < r & r < 1 ) & u in M & 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

for M being Subset of V

for z being Complex st M is convex holds

z * M is convex

proof end;

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 & N is convex holds

M + N is convex

for M, N being Subset of V st M is convex & N is convex holds

M + N is convex

proof end;

theorem :: CONVEX4:47

for V being ComplexLinearSpace

for M, N being Subset of V st M is convex & N is convex holds

M - N is convex

for M, N being Subset of V st M is convex & N is convex holds

M - N is convex

proof end;

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 & 0 < r & r < 1 ) holds

(z * M) + ((1r - z) * M) c= M )

for 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 )

proof end;

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 & 0 < r & r < 1 ) holds

((1r - z) * M) + (z * M) c= M

for 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

proof end;

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 & N is convex holds

for z being Complex holds (z * M) + ((1r - z) * N) is convex

for 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

proof end;

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

for M being Subset of V holds 1r * M = M

proof end;

::$CT

theorem Th53: :: 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

for M being Subset of V

for z1, z2 being Complex holds z1 * (z2 * M) = (z1 * z2) * M

proof end;

theorem Th54: :: 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)

for M1, M2 being Subset of V

for z being Complex holds z * (M1 + M2) = (z * M1) + (z * M2)

proof end;

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 )

for M being Subset of V

for v being VECTOR of V holds

( M is convex iff v + M is convex )

proof end;

theorem :: CONVEX4:59

theorem Th59: :: 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 & M2 is convex holds

(z1 * M1) + (z2 * M2) is convex

for M1, M2 being Subset of V

for z1, z2 being Complex st M1 is convex & M2 is convex holds

(z1 * M1) + (z2 * M2) is convex

proof end;

theorem Th60: :: 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)

for M being Subset of V

for z1, z2 being Complex holds (z1 + z2) * M c= (z1 * M) + (z2 * M)

proof end;

theorem Th61: :: 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

for M, N being Subset of V

for z being Complex st M c= N holds

z * M c= z * N

proof end;

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 & z2 = r2 & r1 >= 0 & r2 >= 0 ) & M is convex holds

(z1 * M) + (z2 * M) c= (z1 + z2) * M

proof end;

::$CT 2

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 & z2 = r2 & r1 >= 0 & r2 >= 0 ) & M is convex holds

(z1 * M) + (z2 * M) = (z1 + z2) * M

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) = (z1 + z2) * M

proof end;

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 & M2 is convex & M3 is convex holds

((z1 * M1) + (z2 * M2)) + (z3 * M3) is convex

for M1, M2, M3 being Subset of V

for z1, z2, z3 being Complex st M1 is convex & M2 is convex & M3 is convex holds

((z1 * M1) + (z2 * M2)) + (z3 * M3) is convex

proof end;

theorem Th65: :: 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

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

proof end;

registration

let V be non empty CLSStruct ;

existence

ex b_{1} being Subset of V st

( not b_{1} is empty & b_{1} is convex )

end;
existence

ex b

( not b

proof end;

registration

let V be non empty CLSStruct ;

existence

ex b_{1} being Subset of V st

( b_{1} is empty & b_{1} is convex )

end;
existence

ex b

( b

proof 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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

:: deftheorem 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 & 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 ) ) ) ) );

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 & 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 ) ) ) ) );

theorem Th77: :: CONVEX4:80

for V being ComplexLinearSpace

for L being C_Linear_Combination of V st L is convex holds

Carrier L <> {}

for L being C_Linear_Combination of V st L is convex holds

Carrier L <> {}

proof end;

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 & ex r being Real st

( r = L . v & r <= 0 ) holds

not v in Carrier L

for L being C_Linear_Combination of V

for 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

proof end;

theorem :: CONVEX4:82

for V being ComplexLinearSpace

for L being C_Linear_Combination of V st L is convex holds

L <> ZeroCLC V

for L being C_Linear_Combination of V st L is convex holds

L <> ZeroCLC V

proof end;

theorem Th80: :: CONVEX4:83

for V being ComplexLinearSpace

for v being VECTOR of V

for 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 )

for v being VECTOR of V

for 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 )

proof end;

theorem Th81: :: 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 & 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) )

for v1, v2 being VECTOR of V

for 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) )

proof end;

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 & v2 <> v3 & v3 <> v1 holds

Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)

proof end;

theorem Th82: :: 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 & 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) )

for v1, v2, v3 being VECTOR of V

for 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) )

proof end;

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 & r = 1 ) & Sum L = (L . v) * v )

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 & r = 1 ) & Sum L = (L . v) * v )

proof end;

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 & 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) )

for v1, v2 being VECTOR of V

for 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) )

proof end;

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 & 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) )

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 & 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) )

proof end;

definition

let V be non empty CLSStruct ;

let M be Subset of V;

ex b_{1} being Subset-Family of V st

for N being Subset of V holds

( N in b_{1} iff ( N is convex & M c= N ) )

for b_{1}, b_{2} being Subset-Family of V st ( for N being Subset of V holds

( N in b_{1} iff ( N is convex & M c= N ) ) ) & ( for N being Subset of V holds

( N in b_{2} iff ( N is convex & M c= N ) ) ) holds

b_{1} = b_{2}

end;
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 & M c= N ) );

existence for N being Subset of V holds

( N in it iff ( N is convex & M c= N ) );

ex b

for N being Subset of V holds

( N in b

proof end;

uniqueness for b

( N in b

( N in b

b

proof end;

:: deftheorem Def25 defines Convex-Family CONVEX4:def 25 :

for V being non empty CLSStruct

for M being Subset of V

for b_{3} being Subset-Family of V holds

( b_{3} = Convex-Family M iff for N being Subset of V holds

( N in b_{3} iff ( N is convex & M c= N ) ) );

for V being non empty CLSStruct

for M being Subset of V

for b

( b

( N in b

definition

let V be non empty CLSStruct ;

let M be Subset of V;

coherence

meet (Convex-Family M) is convex Subset of V

end;
let M be Subset of V;

coherence

meet (Convex-Family M) is convex Subset of V

proof 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);

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

for M being Subset of V

for N being convex Subset of V st M c= N holds

conv M c= N

proof end;