:: by Noboru Endou and Yasunari Shidama

::

:: Received June 16, 2003

:: Copyright (c) 2003-2012 Association of Mizar Users

begin

definition

let V be RealLinearSpace;

defpred S_{1}[ set ] means $1 is Convex_Combination of V;

ex b_{1} being set st

for L being set holds

( L in b_{1} iff L is Convex_Combination of V )

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

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

( L in b_{2} iff L is Convex_Combination of V ) ) holds

b_{1} = b_{2}

end;
defpred S

func ConvexComb V -> set means :Def1: :: CONVEX3:def 1

for L being set holds

( L in it iff L is Convex_Combination of V );

existence for L being set holds

( L in it iff L is Convex_Combination of V );

ex b

for L being set holds

( L in b

proof end;

uniqueness for b

( L in b

( L in b

b

proof end;

:: deftheorem Def1 defines ConvexComb CONVEX3:def 1 :

for V being RealLinearSpace

for b_{2} being set holds

( b_{2} = ConvexComb V iff for L being set holds

( L in b_{2} iff L is Convex_Combination of V ) );

for V being RealLinearSpace

for b

( b

( L in b

definition

let V be RealLinearSpace;

let M be non empty Subset of V;

defpred S_{1}[ set ] means $1 is Convex_Combination of M;

ex b_{1} being set st

for L being set holds

( L in b_{1} iff L is Convex_Combination of M )

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

( L in b_{1} iff L is Convex_Combination of M ) ) & ( for L being set holds

( L in b_{2} iff L is Convex_Combination of M ) ) holds

b_{1} = b_{2}

end;
let M be non empty Subset of V;

defpred S

func ConvexComb M -> set means :: CONVEX3:def 2

for L being set holds

( L in it iff L is Convex_Combination of M );

existence for L being set holds

( L in it iff L is Convex_Combination of M );

ex b

for L being set holds

( L in b

proof end;

uniqueness for b

( L in b

( L in b

b

proof end;

:: deftheorem defines ConvexComb CONVEX3:def 2 :

for V being RealLinearSpace

for M being non empty Subset of V

for b_{3} being set holds

( b_{3} = ConvexComb M iff for L being set holds

( L in b_{3} iff L is Convex_Combination of M ) );

for V being RealLinearSpace

for M being non empty Subset of V

for b

( b

( L in b

theorem Th1: :: CONVEX3:1

for V being RealLinearSpace

for v being VECTOR of V ex L being Convex_Combination of V st

( Sum L = v & ( for A being non empty Subset of V st v in A holds

L is Convex_Combination of A ) )

for v being VECTOR of V ex L being Convex_Combination of V st

( Sum L = v & ( for A being non empty Subset of V st v in A holds

L is Convex_Combination of A ) )

proof end;

theorem :: CONVEX3:2

for V being RealLinearSpace

for v1, v2 being VECTOR of V st v1 <> v2 holds

ex L being Convex_Combination of V st

for A being non empty Subset of V st {v1,v2} c= A holds

L is Convex_Combination of A

for v1, v2 being VECTOR of V st v1 <> v2 holds

ex L being Convex_Combination of V st

for A being non empty Subset of V st {v1,v2} c= A holds

L is Convex_Combination of A

proof end;

theorem :: CONVEX3:3

for V being RealLinearSpace

for v1, v2, v3 being VECTOR of V st v1 <> v2 & v1 <> v3 & v2 <> v3 holds

ex L being Convex_Combination of V st

for A being non empty Subset of V st {v1,v2,v3} c= A holds

L is Convex_Combination of A

for v1, v2, v3 being VECTOR of V st v1 <> v2 & v1 <> v3 & v2 <> v3 holds

ex L being Convex_Combination of V st

for A being non empty Subset of V st {v1,v2,v3} c= A holds

L is Convex_Combination of A

proof end;

Lm1: for V being RealLinearSpace

for M being non empty Subset of V st { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M holds

M is convex

proof end;

Lm2: for V being RealLinearSpace

for M being non empty Subset of V

for L being Convex_Combination of M st card (Carrier L) >= 2 holds

ex L1, L2 being Convex_Combination of M ex r being Real st

( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 )

proof end;

Lm3: for V being RealLinearSpace

for M being non empty Subset of V st M is convex holds

{ (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M

proof end;

theorem :: CONVEX3:4

for V being RealLinearSpace

for M being non empty Subset of V holds

( M is convex iff { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M ) by Lm1, Lm3;

for M being non empty Subset of V holds

( M is convex iff { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M ) by Lm1, Lm3;

theorem :: CONVEX3:5

for V being RealLinearSpace

for M being non empty Subset of V holds conv M = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V }

for M being non empty Subset of V holds conv M = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V }

proof end;

begin

:: deftheorem Def3 defines cone CONVEX3:def 3 :

for V being non empty RLSStruct

for M being Subset of V holds

( M is cone iff for r being Real

for v being VECTOR of V st r > 0 & v in M holds

r * v in M );

for V being non empty RLSStruct

for M being Subset of V holds

( M is cone iff for r being Real

for v being VECTOR of V st r > 0 & v in M holds

r * v in M );

registration
end;

registration

let V be non empty RLSStruct ;

existence

ex b_{1} being Subset of V st

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

end;
existence

ex b

( b

proof end;

registration

let V be RealLinearSpace;

existence

ex b_{1} being Subset of V st

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

end;
existence

ex b

( not b

proof end;

theorem Th7: :: CONVEX3:7

for V being non empty RLSStruct

for M being cone Subset of V st V is vector-distributive & V is scalar-distributive & V is scalar-associative & V is scalar-unital holds

( M is convex iff for u, v being VECTOR of V st u in M & v in M holds

u + v in M )

for M being cone Subset of V st V is vector-distributive & V is scalar-distributive & V is scalar-associative & V is scalar-unital holds

( M is convex iff for u, v being VECTOR of V st u in M & v in M holds

u + v in M )

proof end;

Lm4: for V being RealLinearSpace

for M being Subset of V

for L being Linear_Combination of M st card (Carrier L) >= 1 holds

ex L1, L2 being Linear_Combination of M st

( Sum L = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 & Carrier L1 c= Carrier L & Carrier L2 c= Carrier L & ( for v being VECTOR of V st v in Carrier L1 holds

L1 . v = L . v ) & ( for v being VECTOR of V st v in Carrier L2 holds

L2 . v = L . v ) )

proof end;

theorem :: CONVEX3:8

for V being RealLinearSpace

for M being Subset of V holds

( ( M is convex & M is cone ) iff for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds

L . v > 0 ) holds

Sum L in M )

for M being Subset of V holds

( ( M is convex & M is cone ) iff for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds

L . v > 0 ) holds

Sum L in M )

proof end;

theorem :: CONVEX3:9

for V being non empty RLSStruct

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

M /\ N is cone

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

M /\ N is cone

proof end;