:: CONVEX3 semantic presentation
begin
definition
let V be RealLinearSpace;
defpred S1[ set ] means $1 is Convex_Combination of V;
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
ex b1 being set st
for L being set holds
( L in b1 iff L is Convex_Combination of V )
proof
consider A being set such that
A1: for x being set holds
( x in A iff ( x in Funcs ( the carrier of V,REAL) & S1[x] ) ) from XBOOLE_0:sch_1();
take A ; ::_thesis: for L being set holds
( L in A iff L is Convex_Combination of V )
let L be set ; ::_thesis: ( L in A iff L is Convex_Combination of V )
thus ( L in A implies L is Convex_Combination of V ) by A1; ::_thesis: ( L is Convex_Combination of V implies L in A )
assume L is Convex_Combination of V ; ::_thesis: L in A
hence L in A by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for L being set holds
( L in b1 iff L is Convex_Combination of V ) ) & ( for L being set holds
( L in b2 iff L is Convex_Combination of V ) ) holds
b1 = b2
proof
thus for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;
:: deftheorem Def1 defines ConvexComb CONVEX3:def_1_:_
for V being RealLinearSpace
for b2 being set holds
( b2 = ConvexComb V iff for L being set holds
( L in b2 iff L is Convex_Combination of V ) );
definition
let V be RealLinearSpace;
let M be non empty Subset of V;
defpred S1[ set ] means $1 is Convex_Combination of M;
func ConvexComb M -> set means :: CONVEX3:def 2
for L being set holds
( L in it iff L is Convex_Combination of M );
existence
ex b1 being set st
for L being set holds
( L in b1 iff L is Convex_Combination of M )
proof
consider A being set such that
A1: for x being set holds
( x in A iff ( x in Funcs ( the carrier of V,REAL) & S1[x] ) ) from XBOOLE_0:sch_1();
take A ; ::_thesis: for L being set holds
( L in A iff L is Convex_Combination of M )
let L be set ; ::_thesis: ( L in A iff L is Convex_Combination of M )
thus ( L in A implies L is Convex_Combination of M ) by A1; ::_thesis: ( L is Convex_Combination of M implies L in A )
assume L is Convex_Combination of M ; ::_thesis: L in A
hence L in A by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for L being set holds
( L in b1 iff L is Convex_Combination of M ) ) & ( for L being set holds
( L in b2 iff L is Convex_Combination of M ) ) holds
b1 = b2
proof
thus for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;
:: deftheorem defines ConvexComb CONVEX3:def_2_:_
for V being RealLinearSpace
for M being non empty Subset of V
for b3 being set holds
( b3 = ConvexComb M iff for L being set holds
( L in b3 iff L is Convex_Combination of M ) );
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 ) )
proof
let V be RealLinearSpace; ::_thesis: 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 ) )
let v be VECTOR of V; ::_thesis: 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 ) )
consider L being Linear_Combination of {v} such that
A1: L . v = 1 by RLVECT_4:37;
consider F being FinSequence of the carrier of V such that
A2: ( F is one-to-one & rng F = Carrier L ) and
Sum L = Sum (L (#) F) by RLVECT_2:def_8;
v in Carrier L by A1, RLVECT_2:19;
then ( Carrier L c= {v} & {v} c= Carrier L ) by RLVECT_2:def_6, ZFMISC_1:31;
then A3: {v} = Carrier L by XBOOLE_0:def_10;
then F = <*v*> by A2, FINSEQ_3:97;
then A4: F . 1 = v by FINSEQ_1:def_8;
deffunc H1( set ) -> set = L . (F . $1);
consider f being FinSequence such that
A5: ( len f = len F & ( for n being Nat st n in dom f holds
f . n = H1(n) ) ) from FINSEQ_1:sch_2();
A6: len F = 1 by A3, A2, FINSEQ_3:96;
then 1 in dom f by A5, FINSEQ_3:25;
then A7: f . 1 = L . (F . 1) by A5;
then f = <*1*> by A1, A5, A6, A4, FINSEQ_1:40;
then rng f = {1} by FINSEQ_1:38;
then rng f c= REAL by ZFMISC_1:31;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4;
A8: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )
proof
let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A9: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 )
then n in Seg (len f) by FINSEQ_1:def_3;
hence ( f . n = L . (F . n) & f . n >= 0 ) by A1, A5, A6, A7, A4, A9, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum
end;
f = <*1*> by A1, A5, A6, A7, A4, FINSEQ_1:40;
then Sum f = 1 by FINSOP_1:11;
then reconsider L = L as Convex_Combination of V by A2, A5, A8, CONVEX1:def_3;
A10: for A being non empty Subset of V st v in A holds
L is Convex_Combination of A
proof
let A be non empty Subset of V; ::_thesis: ( v in A implies L is Convex_Combination of A )
assume v in A ; ::_thesis: L is Convex_Combination of A
then {v} c= A by ZFMISC_1:31;
hence L is Convex_Combination of A by A3, RLVECT_2:def_6; ::_thesis: verum
end;
take L ; ::_thesis: ( Sum L = v & ( for A being non empty Subset of V st v in A holds
L is Convex_Combination of A ) )
Sum L = 1 * v by A1, A3, RLVECT_2:35;
hence ( Sum L = v & ( for A being non empty Subset of V st v in A holds
L is Convex_Combination of A ) ) by A10, RLVECT_1:def_8; ::_thesis: verum
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
proof
let V be RealLinearSpace; ::_thesis: 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
let v1, v2 be VECTOR of V; ::_thesis: ( v1 <> v2 implies 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 )
assume A1: v1 <> v2 ; ::_thesis: 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
consider L being Linear_Combination of {v1,v2} such that
A2: ( L . v1 = 1 / 2 & L . v2 = 1 / 2 ) by A1, RLVECT_4:38;
consider F being FinSequence of the carrier of V such that
A3: ( F is one-to-one & rng F = Carrier L ) and
Sum L = Sum (L (#) F) by RLVECT_2:def_8;
deffunc H1( set ) -> set = L . (F . $1);
consider f being FinSequence such that
A4: ( len f = len F & ( for n being Nat st n in dom f holds
f . n = H1(n) ) ) from FINSEQ_1:sch_2();
( v1 in Carrier L & v2 in Carrier L ) by A2, RLVECT_2:19;
then ( Carrier L c= {v1,v2} & {v1,v2} c= Carrier L ) by RLVECT_2:def_6, ZFMISC_1:32;
then A5: {v1,v2} = Carrier L by XBOOLE_0:def_10;
then A6: len F = 2 by A1, A3, FINSEQ_3:98;
then 2 in dom f by A4, FINSEQ_3:25;
then A7: f . 2 = L . (F . 2) by A4;
1 in dom f by A4, A6, FINSEQ_3:25;
then A8: f . 1 = L . (F . 1) by A4;
now__::_thesis:_ex_L,_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
percases ( F = <*v1,v2*> or F = <*v2,v1*> ) by A1, A5, A3, FINSEQ_3:99;
suppose F = <*v1,v2*> ; ::_thesis: ex L, 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
then A9: ( F . 1 = v1 & F . 2 = v2 ) by FINSEQ_1:44;
then f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, FINSEQ_1:44;
then f = <*(1 / 2)*> ^ <*(1 / 2)*> by FINSEQ_1:def_9;
then rng f = (rng <*(1 / 2)*>) \/ (rng <*(1 / 2)*>) by FINSEQ_1:31
.= {(1 / 2)} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4;
A10: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )
proof
let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A11: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 )
then n in Seg (len f) by FINSEQ_1:def_3;
hence ( f . n = L . (F . n) & f . n >= 0 ) by A2, A4, A6, A8, A7, A9, A11, FINSEQ_1:2, TARSKI:def_2; ::_thesis: verum
end;
f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, A9, FINSEQ_1:44;
then Sum f = (1 / 2) + (1 / 2) by RVSUM_1:77
.= 1 ;
then reconsider L = L as Convex_Combination of V by A3, A4, A10, CONVEX1:def_3;
take L = L; ::_thesis: 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 A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A by A5, RLVECT_2:def_6;
hence 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 ; ::_thesis: verum
end;
suppose F = <*v2,v1*> ; ::_thesis: ex L, 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
then A12: ( F . 1 = v2 & F . 2 = v1 ) by FINSEQ_1:44;
then f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, FINSEQ_1:44;
then f = <*(1 / 2)*> ^ <*(1 / 2)*> by FINSEQ_1:def_9;
then rng f = (rng <*(1 / 2)*>) \/ (rng <*(1 / 2)*>) by FINSEQ_1:31
.= {(1 / 2)} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4;
A13: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )
proof
let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A14: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 )
then n in Seg (len f) by FINSEQ_1:def_3;
hence ( f . n = L . (F . n) & f . n >= 0 ) by A2, A4, A6, A8, A7, A12, A14, FINSEQ_1:2, TARSKI:def_2; ::_thesis: verum
end;
f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, A12, FINSEQ_1:44;
then Sum f = (1 / 2) + (1 / 2) by RVSUM_1:77
.= 1 ;
then reconsider L = L as Convex_Combination of V by A3, A4, A13, CONVEX1:def_3;
take L = L; ::_thesis: 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 A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A by A5, RLVECT_2:def_6;
hence 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 ; ::_thesis: verum
end;
end;
end;
hence 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 ; ::_thesis: verum
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
proof
let V be RealLinearSpace; ::_thesis: 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
let v1, v2, v3 be VECTOR of V; ::_thesis: ( v1 <> v2 & v1 <> v3 & v2 <> v3 implies 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 )
assume that
A1: v1 <> v2 and
A2: v1 <> v3 and
A3: v2 <> v3 ; ::_thesis: 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
consider L being Linear_Combination of {v1,v2,v3} such that
A4: ( L . v1 = 1 / 3 & L . v2 = 1 / 3 & L . v3 = 1 / 3 ) by A1, A2, A3, RLVECT_4:39;
consider F being FinSequence of the carrier of V such that
A5: ( F is one-to-one & rng F = Carrier L ) and
Sum L = Sum (L (#) F) by RLVECT_2:def_8;
deffunc H1( set ) -> set = L . (F . $1);
consider f being FinSequence such that
A6: ( len f = len F & ( for n being Nat st n in dom f holds
f . n = H1(n) ) ) from FINSEQ_1:sch_2();
for x being set st x in {v1,v2,v3} holds
x in Carrier L
proof
let x be set ; ::_thesis: ( x in {v1,v2,v3} implies x in Carrier L )
assume A7: x in {v1,v2,v3} ; ::_thesis: x in Carrier L
then reconsider x = x as VECTOR of V ;
( x = v1 or x = v2 or x = v3 ) by A7, ENUMSET1:def_1;
hence x in Carrier L by A4, RLVECT_2:19; ::_thesis: verum
end;
then ( Carrier L c= {v1,v2,v3} & {v1,v2,v3} c= Carrier L ) by RLVECT_2:def_6, TARSKI:def_3;
then A8: {v1,v2,v3} = Carrier L by XBOOLE_0:def_10;
then A9: len F = 3 by A1, A2, A3, A5, FINSEQ_3:101;
then 2 in dom f by A6, FINSEQ_3:25;
then A10: f . 2 = L . (F . 2) by A6;
3 in dom f by A6, A9, FINSEQ_3:25;
then A11: f . 3 = L . (F . 3) by A6;
1 in dom f by A6, A9, FINSEQ_3:25;
then A12: f . 1 = L . (F . 1) by A6;
now__::_thesis:_ex_L,_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
percases ( F = <*v1,v2,v3*> or F = <*v1,v3,v2*> or F = <*v2,v1,v3*> or F = <*v2,v3,v1*> or F = <*v3,v1,v2*> or F = <*v3,v2,v1*> ) by A1, A2, A3, A8, A5, CONVEX1:31;
supposeA13: F = <*v1,v2,v3*> ; ::_thesis: ex L, 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
then A14: F . 3 = v3 by FINSEQ_1:45;
A15: ( F . 1 = v1 & F . 2 = v2 ) by A13, FINSEQ_1:45;
then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A14, FINSEQ_1:45;
then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def_10;
then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31
.= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31
.= {(1 / 3)} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4;
A16: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )
proof
let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A17: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 )
then n in Seg (len f) by FINSEQ_1:def_3;
hence ( f . n = L . (F . n) & f . n >= 0 ) by A4, A6, A9, A12, A10, A11, A15, A14, A17, ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: verum
end;
f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A15, A14, FINSEQ_1:45;
then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78
.= 1 ;
then reconsider L = L as Convex_Combination of V by A5, A6, A16, CONVEX1:def_3;
take L = L; ::_thesis: 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 A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A8, RLVECT_2:def_6;
hence 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 ; ::_thesis: verum
end;
supposeA18: F = <*v1,v3,v2*> ; ::_thesis: ex L, 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
then A19: F . 3 = v2 by FINSEQ_1:45;
A20: ( F . 1 = v1 & F . 2 = v3 ) by A18, FINSEQ_1:45;
then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A19, FINSEQ_1:45;
then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def_10;
then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31
.= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31
.= {(1 / 3)} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4;
A21: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )
proof
let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A22: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 )
then n in Seg (len f) by FINSEQ_1:def_3;
hence ( f . n = L . (F . n) & f . n >= 0 ) by A4, A6, A9, A12, A10, A11, A20, A19, A22, ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: verum
end;
f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A20, A19, FINSEQ_1:45;
then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78
.= 1 ;
then reconsider L = L as Convex_Combination of V by A5, A6, A21, CONVEX1:def_3;
take L = L; ::_thesis: 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 A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A8, RLVECT_2:def_6;
hence 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 ; ::_thesis: verum
end;
supposeA23: F = <*v2,v1,v3*> ; ::_thesis: ex L, 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
then A24: F . 3 = v3 by FINSEQ_1:45;
A25: ( F . 1 = v2 & F . 2 = v1 ) by A23, FINSEQ_1:45;
then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A24, FINSEQ_1:45;
then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def_10;
then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31
.= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31
.= {(1 / 3)} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4;
A26: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )
proof
let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A27: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 )
then n in Seg (len f) by FINSEQ_1:def_3;
hence ( f . n = L . (F . n) & f . n >= 0 ) by A4, A6, A9, A12, A10, A11, A25, A24, A27, ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: verum
end;
f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A25, A24, FINSEQ_1:45;
then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78
.= 1 ;
then reconsider L = L as Convex_Combination of V by A5, A6, A26, CONVEX1:def_3;
take L = L; ::_thesis: 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 A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A8, RLVECT_2:def_6;
hence 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 ; ::_thesis: verum
end;
supposeA28: F = <*v2,v3,v1*> ; ::_thesis: ex L, 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
then A29: F . 3 = v1 by FINSEQ_1:45;
A30: ( F . 1 = v2 & F . 2 = v3 ) by A28, FINSEQ_1:45;
then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A29, FINSEQ_1:45;
then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def_10;
then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31
.= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31
.= {(1 / 3)} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4;
A31: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )
proof
let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A32: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 )
then n in Seg (len f) by FINSEQ_1:def_3;
hence ( f . n = L . (F . n) & f . n >= 0 ) by A4, A6, A9, A12, A10, A11, A30, A29, A32, ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: verum
end;
f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A30, A29, FINSEQ_1:45;
then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78
.= 1 ;
then reconsider L = L as Convex_Combination of V by A5, A6, A31, CONVEX1:def_3;
take L = L; ::_thesis: 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 A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A8, RLVECT_2:def_6;
hence 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 ; ::_thesis: verum
end;
supposeA33: F = <*v3,v1,v2*> ; ::_thesis: ex L, 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
then A34: F . 3 = v2 by FINSEQ_1:45;
A35: ( F . 1 = v3 & F . 2 = v1 ) by A33, FINSEQ_1:45;
then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A34, FINSEQ_1:45;
then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def_10;
then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31
.= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31
.= {(1 / 3)} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4;
A36: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )
proof
let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A37: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 )
then n in Seg (len f) by FINSEQ_1:def_3;
hence ( f . n = L . (F . n) & f . n >= 0 ) by A4, A6, A9, A12, A10, A11, A35, A34, A37, ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: verum
end;
f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A35, A34, FINSEQ_1:45;
then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78
.= 1 ;
then reconsider L = L as Convex_Combination of V by A5, A6, A36, CONVEX1:def_3;
take L = L; ::_thesis: 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 A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A8, RLVECT_2:def_6;
hence 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 ; ::_thesis: verum
end;
supposeA38: F = <*v3,v2,v1*> ; ::_thesis: ex L, 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
then A39: F . 3 = v1 by FINSEQ_1:45;
A40: ( F . 1 = v3 & F . 2 = v2 ) by A38, FINSEQ_1:45;
then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A39, FINSEQ_1:45;
then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def_10;
then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31
.= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31
.= {(1 / 3)} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4;
A41: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )
proof
let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A42: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 )
then n in Seg (len f) by FINSEQ_1:def_3;
hence ( f . n = L . (F . n) & f . n >= 0 ) by A4, A6, A9, A12, A10, A11, A40, A39, A42, ENUMSET1:def_1, FINSEQ_3:1; ::_thesis: verum
end;
f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A40, A39, FINSEQ_1:45;
then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78
.= 1 ;
then reconsider L = L as Convex_Combination of V by A5, A6, A41, CONVEX1:def_3;
take L = L; ::_thesis: 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 A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A8, RLVECT_2:def_6;
hence 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 ; ::_thesis: verum
end;
end;
end;
hence 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 ; ::_thesis: verum
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
let V be RealLinearSpace; ::_thesis: 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
let M be non empty Subset of V; ::_thesis: ( { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M implies M is convex )
assume A1: { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M ; ::_thesis: M is convex
for u, v being VECTOR of V
for r being Real st 0 < r & r < 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M
proof
set S = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } ;
let u, v be VECTOR of V; ::_thesis: for r being Real st 0 < r & r < 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M
let r be Real; ::_thesis: ( 0 < r & r < 1 & u in M & v in M implies (r * u) + ((1 - r) * v) in M )
assume that
A2: ( 0 < r & r < 1 ) and
A3: u in M and
A4: v in M ; ::_thesis: (r * u) + ((1 - r) * v) in M
consider Lv being Convex_Combination of V such that
A5: Sum Lv = v and
A6: for A being non empty Subset of V st v in A holds
Lv is Convex_Combination of A by Th1;
reconsider Lv = Lv as Convex_Combination of M by A4, A6;
consider Lu being Convex_Combination of V such that
A7: Sum Lu = u and
A8: for A being non empty Subset of V st u in A holds
Lu is Convex_Combination of A by Th1;
reconsider Lu = Lu as Convex_Combination of M by A3, A8;
A9: (r * u) + ((1 - r) * v) = (Sum (r * Lu)) + ((1 - r) * (Sum Lv)) by A7, A5, RLVECT_3:2
.= (Sum (r * Lu)) + (Sum ((1 - r) * Lv)) by RLVECT_3:2
.= Sum ((r * Lu) + ((1 - r) * Lv)) by RLVECT_3:1 ;
A10: (r * Lu) + ((1 - r) * Lv) is Convex_Combination of M by A2, CONVEX2:9;
then (r * Lu) + ((1 - r) * Lv) in ConvexComb V by Def1;
then (r * u) + ((1 - r) * v) in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } by A9, A10;
hence (r * u) + ((1 - r) * v) in M by A1; ::_thesis: verum
end;
hence M is convex by CONVEX1:def_2; ::_thesis: verum
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
let V be RealLinearSpace; ::_thesis: 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 )
let M be non empty Subset of V; ::_thesis: 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 )
let L be Convex_Combination of M; ::_thesis: ( card (Carrier L) >= 2 implies 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 ) )
consider F being FinSequence of the carrier of V such that
A1: F is one-to-one and
A2: rng F = Carrier L and
A3: 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 ) ) ) by CONVEX1:def_3;
A4: for n, m being Element of NAT st 1 <= n & n < m & m <= len F holds
F . n <> F . m
proof
let n, m be Element of NAT ; ::_thesis: ( 1 <= n & n < m & m <= len F implies F . n <> F . m )
assume that
A5: 1 <= n and
A6: n < m and
A7: m <= len F ; ::_thesis: F . n <> F . m
n <= len F by A6, A7, XXREAL_0:2;
then n in Seg (len F) by A5, FINSEQ_1:1;
then A8: n in dom F by FINSEQ_1:def_3;
1 <= m by A5, A6, XXREAL_0:2;
then m in Seg (len F) by A7, FINSEQ_1:1;
then A9: m in dom F by FINSEQ_1:def_3;
assume F . n = F . m ; ::_thesis: contradiction
hence contradiction by A1, A6, A8, A9, FUNCT_1:def_4; ::_thesis: verum
end;
assume A10: card (Carrier L) >= 2 ; ::_thesis: 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 )
then A11: len F >= 2 by A2, A4, GRAPH_5:7;
then consider i being Nat such that
A12: len F = i + 1 by NAT_1:6;
set v = F . (len F);
A13: Carrier L c= M by RLVECT_2:def_6;
1 <= len F by A11, XXREAL_0:2;
then A14: len F in dom F by FINSEQ_3:25;
then A15: F . (len F) in rng F by FUNCT_1:3;
rng F c= the carrier of V by FINSEQ_1:def_4;
then reconsider v = F . (len F) as VECTOR of V by A15;
A16: F . (len F) in rng F by A14, FUNCT_1:3;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
consider f being FinSequence of REAL such that
A17: len f = len F and
A18: Sum f = 1 and
A19: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) by A3;
1 <= len f by A17, A11, XXREAL_0:2;
then A20: 1 in Seg (len f) by FINSEQ_1:1;
then A21: 1 in dom f by FINSEQ_1:def_3;
1 in dom F by A17, A20, FINSEQ_1:def_3;
then F . 1 in rng F by FUNCT_1:3;
then A22: L . (F . 1) <> 0 by A2, RLVECT_2:19;
A23: for k being Nat st k in dom (f | i) holds
0 <= (f | i) . k
proof
A24: dom (f | i) c= dom f by FINSEQ_5:18;
let k be Nat; ::_thesis: ( k in dom (f | i) implies 0 <= (f | i) . k )
assume A25: k in dom (f | i) ; ::_thesis: 0 <= (f | i) . k
f | i = f | (Seg i) by FINSEQ_1:def_15;
then (f | i) . k = f . k by A25, FUNCT_1:47;
hence 0 <= (f | i) . k by A19, A25, A24; ::_thesis: verum
end;
len F >= 1 + 1 by A10, A2, A4, GRAPH_5:7;
then (len F) - 1 >= 1 by XREAL_1:19;
then 1 in Seg i by A12, FINSEQ_1:1;
then A26: 1 in dom (f | (Seg i)) by A21, RELAT_1:57;
f | i = f | (Seg i) by FINSEQ_1:def_15;
then A27: (f | i) . 1 = f . 1 by A26, FUNCT_1:47
.= L . (F . 1) by A19, A21 ;
A28: 1 in dom (f | i) by A26, FINSEQ_1:def_15;
then (f | i) . 1 >= 0 by A23;
then A29: Sum (f | i) > 0 by A23, A28, A27, A22, RVSUM_1:85;
1 <= len f by A17, A11, XXREAL_0:2;
then len f in Seg (len f) by FINSEQ_1:1;
then A30: len f in dom f by FINSEQ_1:def_3;
then f . (len f) in rng f by FUNCT_1:3;
then reconsider r = f . (len f) as Real ;
A31: f = (f | i) ^ (f /^ i) by RFINSEQ:8;
for n, m being Element of NAT st n in dom (F | i) & m in dom (F | i) & (F | i) /. n = (F | i) /. m holds
n = m
proof
A32: dom (F | i) c= dom F by FINSEQ_5:18;
let n, m be Element of NAT ; ::_thesis: ( n in dom (F | i) & m in dom (F | i) & (F | i) /. n = (F | i) /. m implies n = m )
assume that
A33: n in dom (F | i) and
A34: m in dom (F | i) and
A35: (F | i) /. n = (F | i) /. m ; ::_thesis: n = m
F /. n = (F | i) /. n by A33, FINSEQ_4:70
.= F /. m by A34, A35, FINSEQ_4:70 ;
hence n = m by A1, A33, A34, A32, PARTFUN2:10; ::_thesis: verum
end;
then A36: F | i is one-to-one by PARTFUN2:9;
reconsider B = {v} as non empty Subset of V ;
consider L1 being Convex_Combination of V such that
Sum L1 = v and
A37: for A being non empty Subset of V st v in A holds
L1 is Convex_Combination of A by Th1;
A38: f = (f | i) ^ (f /^ i) by RFINSEQ:8;
set r9 = 1 / (1 - r);
defpred S1[ set , set ] means ( ( $1 in (rng F) \ {v} implies $2 = (1 / (1 - r)) * (L . $1) ) & ( not $1 in (rng F) \ {v} implies $2 = 0 ) );
A39: for x being set st x in the carrier of V holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier of V implies ex y being set st S1[x,y] )
assume x in the carrier of V ; ::_thesis: ex y being set st S1[x,y]
( x in (rng F) \ {v} or not x in (rng F) \ {v} ) ;
hence ex y being set st S1[x,y] ; ::_thesis: verum
end;
consider L2 being Function such that
A40: ( dom L2 = the carrier of V & ( for x being set st x in the carrier of V holds
S1[x,L2 . x] ) ) from CLASSES1:sch_1(A39);
for y being set st y in rng L2 holds
y in REAL
proof
let y be set ; ::_thesis: ( y in rng L2 implies y in REAL )
assume y in rng L2 ; ::_thesis: y in REAL
then consider x being set such that
A41: x in dom L2 and
A42: y = L2 . x by FUNCT_1:def_3;
percases ( x in (rng F) \ {v} or not x in (rng F) \ {v} ) ;
supposeA43: x in (rng F) \ {v} ; ::_thesis: y in REAL
then x in rng F ;
then reconsider x = x as VECTOR of V by A2;
y = (1 / (1 - r)) * (L . x) by A40, A42, A43
.= ((1 / (1 - r)) * L) . x by RLVECT_2:def_11 ;
hence y in REAL ; ::_thesis: verum
end;
suppose not x in (rng F) \ {v} ; ::_thesis: y in REAL
then y = 0 by A40, A41, A42;
hence y in REAL ; ::_thesis: verum
end;
end;
end;
then rng L2 c= REAL by TARSKI:def_3;
then A44: L2 is Element of Funcs ( the carrier of V,REAL) by A40, FUNCT_2:def_2;
ex T being finite Subset of V st
for v being Element of V st not v in T holds
L2 . v = 0
proof
reconsider T = (Carrier L) \ {v} as finite Subset of V ;
take T ; ::_thesis: for v being Element of V st not v in T holds
L2 . v = 0
thus for v being Element of V st not v in T holds
L2 . v = 0 by A2, A40; ::_thesis: verum
end;
then reconsider L2 = L2 as Linear_Combination of V by A44, RLVECT_2:def_3;
for u being set st u in Carrier L2 holds
u in (Carrier L) \ {v}
proof
let u be set ; ::_thesis: ( u in Carrier L2 implies u in (Carrier L) \ {v} )
assume A45: u in Carrier L2 ; ::_thesis: u in (Carrier L) \ {v}
then reconsider u = u as Element of V ;
L2 . u <> 0 by A45, RLVECT_2:19;
hence u in (Carrier L) \ {v} by A2, A40; ::_thesis: verum
end;
then A46: Carrier L2 c= (Carrier L) \ {v} by TARSKI:def_3;
f /^ i = <*(f /. (len f))*> by A17, A12, FINSEQ_5:30
.= <*(f . (len f))*> by A30, PARTFUN1:def_6 ;
then A47: Sum f = (Sum (f | i)) + r by A31, RVSUM_1:74;
then Sum (f | i) = 1 - r by A18;
then A48: 1 > r + 0 by A29, XREAL_1:20;
A49: 1 / (1 - r) > 0 by A18, A47, A29, XREAL_1:139;
for u being set st u in (Carrier L) \ {v} holds
u in Carrier L2
proof
let u be set ; ::_thesis: ( u in (Carrier L) \ {v} implies u in Carrier L2 )
assume A50: u in (Carrier L) \ {v} ; ::_thesis: u in Carrier L2
then reconsider u = u as Element of V ;
u in Carrier L by A50, XBOOLE_0:def_5;
then A51: L . u <> 0 by RLVECT_2:19;
L2 . u = (1 / (1 - r)) * (L . u) by A2, A40, A50;
then L2 . u <> 0 by A49, A51, XCMPLX_1:6;
hence u in Carrier L2 by RLVECT_2:19; ::_thesis: verum
end;
then (Carrier L) \ {v} c= Carrier L2 by TARSKI:def_3;
then A52: Carrier L2 = (Carrier L) \ {v} by A46, XBOOLE_0:def_10;
then Carrier L2 c= Carrier L by XBOOLE_1:36;
then Carrier L2 c= M by A13, XBOOLE_1:1;
then reconsider L2 = L2 as Linear_Combination of M by RLVECT_2:def_6;
deffunc H1( set ) -> set = L2 . ((F | i) . $1);
consider f2 being FinSequence such that
A53: ( len f2 = len (F | i) & ( for k being Nat st k in dom f2 holds
f2 . k = H1(k) ) ) from FINSEQ_1:sch_2();
F = (F | i) ^ (F /^ i) by RFINSEQ:8;
then Carrier L = (rng (F | i)) \/ (rng (F /^ i)) by A2, FINSEQ_1:31;
then A54: (Carrier L) \ (rng (F /^ i)) = rng (F | i) by A1, FINSEQ_5:34, XBOOLE_1:88;
for y being set st y in rng f2 holds
y in REAL
proof
let y be set ; ::_thesis: ( y in rng f2 implies y in REAL )
A55: ex L29 being Function st
( L2 = L29 & dom L29 = the carrier of V & rng L29 c= REAL ) by FUNCT_2:def_2;
assume y in rng f2 ; ::_thesis: y in REAL
then consider x being set such that
A56: x in dom f2 and
A57: y = f2 . x by FUNCT_1:def_3;
A58: x in Seg (len f2) by A56, FINSEQ_1:def_3;
reconsider x = x as Element of NAT by A56;
x in dom (F | i) by A53, A58, FINSEQ_1:def_3;
then (F | i) . x in rng (F | i) by FUNCT_1:3;
then L2 . ((F | i) . x) in rng L2 by A54, A55, FUNCT_1:3;
then L2 . ((F | i) . x) in REAL ;
hence y in REAL by A53, A56, A57; ::_thesis: verum
end;
then rng f2 c= REAL by TARSKI:def_3;
then reconsider f2 = f2 as FinSequence of REAL by FINSEQ_1:def_4;
A59: dom f2 = Seg (len (F | i)) by A53, FINSEQ_1:def_3;
then A60: dom f2 = Seg i by A12, FINSEQ_1:59, NAT_1:12
.= Seg (len (f | i)) by A17, A12, FINSEQ_1:59, NAT_1:12
.= dom (f | i) by FINSEQ_1:def_3 ;
A61: (len F) - 1 = i by A12;
A62: for k being Element of NAT st k in dom f2 holds
( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 )
proof
let k be Element of NAT ; ::_thesis: ( k in dom f2 implies ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 ) )
assume A63: k in dom f2 ; ::_thesis: ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 )
then A64: f2 . k = L2 . ((F | i) . k) by A53;
k in dom (f | (Seg i)) by A60, A63, FINSEQ_1:def_15;
then k in (dom f) /\ (Seg i) by RELAT_1:61;
then A65: k in dom f by XBOOLE_0:def_4;
A66: k in dom (F | i) by A59, A63, FINSEQ_1:def_3;
then (F | i) . k in rng (F | i) by FUNCT_1:3;
then reconsider w = (F | i) . k as Element of V by A54;
A67: F | i = F | (Seg i) by FINSEQ_1:def_15;
then A68: (F | i) . k = F . k by A66, FUNCT_1:47;
A69: not w in {v}
proof
( k <= len (F | i) & len (F | i) <= i ) by A59, A63, FINSEQ_1:1, FINSEQ_5:17;
then k <= i by XXREAL_0:2;
then A70: k + 1 <= len F by A61, XREAL_1:19;
assume w in {v} ; ::_thesis: contradiction
then A71: F . k = v by A68, TARSKI:def_1;
dom (F | (Seg i)) c= dom F by RELAT_1:60;
then k = len F by A1, A14, A66, A67, A71, FUNCT_1:def_4;
hence contradiction by A70, NAT_1:13; ::_thesis: verum
end;
f | i = f | (Seg i) by FINSEQ_1:def_15;
then A72: (f | i) . k = f . k by A60, A63, FUNCT_1:47;
then A73: (f | i) . k = L . (F . k) by A19, A65;
then A74: (f | i) . k = L . ((F | i) . k) by A66, A67, FUNCT_1:47;
percases ( w in (rng F) \ {v} or not w in (rng F) \ {v} ) ;
supposeA75: w in (rng F) \ {v} ; ::_thesis: ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 )
f . k >= 0 by A19, A65;
then A76: (1 / (1 - r)) * ((f | i) . k) >= 0 by A18, A47, A29, A72;
L2 . w = (1 / (1 - r)) * (L . w) by A40, A75
.= (1 / (1 - r)) * ((f | i) . k) by A73, A66, A67, FUNCT_1:47
.= ((1 / (1 - r)) * (f | i)) . k by RVSUM_1:44 ;
hence ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 ) by A64, A76, RVSUM_1:44; ::_thesis: verum
end;
supposeA77: not w in (rng F) \ {v} ; ::_thesis: ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 )
then not w in rng F by A69, XBOOLE_0:def_5;
then L . w = 0 by A2, RLVECT_2:19;
then A78: (1 / (1 - r)) * ((f | i) . k) = 0 by A74;
f2 . k = 0 by A40, A64, A77;
hence ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 ) by A78, RVSUM_1:44; ::_thesis: verum
end;
end;
end;
then A79: for n being Nat st n in dom f2 holds
( f2 . n = L2 . ((F | i) . n) & f2 . n >= 0 ) by A53;
f /^ i = <*(f /. (len f))*> by A17, A12, FINSEQ_5:30
.= <*(f . (len f))*> by A30, PARTFUN1:def_6 ;
then A80: Sum f = (Sum (f | i)) + r by A38, RVSUM_1:74;
F /^ i = <*(F /. (len F))*> by A12, FINSEQ_5:30
.= <*(F . (len F))*> by A14, PARTFUN1:def_6 ;
then A81: rng (F | i) = Carrier L2 by A52, A54, FINSEQ_1:38;
A82: for k being Nat st k in dom f2 holds
f2 . k = ((1 / (1 - r)) * (f | i)) . k by A62;
dom f2 = dom ((1 / (1 - r)) * (f | i)) by A60, VALUED_1:def_5;
then f2 = (1 / (1 - r)) * (f | i) by A82, FINSEQ_1:13;
then Sum f2 = (1 / (1 - r)) * (1 - r) by A18, A80, RVSUM_1:87
.= 1 / ((1 - r) / (1 - r)) by XCMPLX_1:81
.= 1 / 1 by A18, A47, A29, XCMPLX_1:60
.= 1 ;
then reconsider L2 = L2 as Convex_Combination of M by A36, A81, A53, A79, CONVEX1:def_3;
A83: v in Carrier L by A2, A14, FUNCT_1:3;
then {v} c= Carrier L by ZFMISC_1:31;
then A84: card (Carrier L2) = (card (Carrier L)) - (card {v}) by A52, CARD_2:44;
Carrier L c= M by RLVECT_2:def_6;
then reconsider L1 = L1 as Convex_Combination of M by A37, A83;
v in {v} by TARSKI:def_1;
then L1 is Convex_Combination of B by A37;
then A85: Carrier L1 c= {v} by RLVECT_2:def_6;
then A86: ( Carrier L1 = {} or Carrier L1 = {v} ) by ZFMISC_1:33;
A87: for u being Element of V holds L . u = ((r * L1) + ((1 - r) * L2)) . u
proof
let u be Element of V; ::_thesis: L . u = ((r * L1) + ((1 - r) * L2)) . u
A88: ((r * L1) + ((1 - r) * L2)) . u = ((r * L1) . u) + (((1 - r) * L2) . u) by RLVECT_2:def_10;
percases ( u in Carrier L or not u in Carrier L ) ;
supposeA89: u in Carrier L ; ::_thesis: L . u = ((r * L1) + ((1 - r) * L2)) . u
percases ( u = v or u <> v ) ;
supposeA90: u = v ; ::_thesis: L . u = ((r * L1) + ((1 - r) * L2)) . u
then u in {v} by TARSKI:def_1;
then not u in Carrier L2 by A46, XBOOLE_0:def_5;
then L2 . u = 0 by RLVECT_2:19;
then (1 - r) * (L2 . u) = 0 ;
then A91: ((1 - r) * L2) . u = 0 by RLVECT_2:def_11;
L1 . u = 1 by A86, A90, CONVEX1:21, CONVEX1:27;
then A92: r * (L1 . u) = r ;
L . u = r + 0 by A17, A19, A30, A90;
hence L . u = ((r * L1) + ((1 - r) * L2)) . u by A88, A92, A91, RLVECT_2:def_11; ::_thesis: verum
end;
suppose u <> v ; ::_thesis: L . u = ((r * L1) + ((1 - r) * L2)) . u
then A93: not u in Carrier L1 by A85, TARSKI:def_1;
then L1 . u = 0 by RLVECT_2:19;
then r * (L1 . u) = 0 ;
then A94: (r * L1) . u = 0 by RLVECT_2:def_11;
u in Carrier L2 by A52, A86, A89, A93, CONVEX1:21, XBOOLE_0:def_5;
then L2 . u = (1 / (1 - r)) * (L . u) by A2, A40, A46;
then (1 - r) * (L2 . u) = ((1 - r) * (1 / (1 - r))) * (L . u)
.= (1 / ((1 - r) / (1 - r))) * (L . u) by XCMPLX_1:81
.= 1 * (L . u) by A18, A47, A29, XCMPLX_1:51
.= L . u ;
hence L . u = ((r * L1) + ((1 - r) * L2)) . u by A88, A94, RLVECT_2:def_11; ::_thesis: verum
end;
end;
end;
supposeA95: not u in Carrier L ; ::_thesis: L . u = ((r * L1) + ((1 - r) * L2)) . u
then not u in Carrier L1 by A2, A15, A85, TARSKI:def_1;
then L1 . u = 0 by RLVECT_2:19;
then r * (L1 . u) = 0 ;
then A96: (r * L1) . u = 0 by RLVECT_2:def_11;
not u in Carrier L2 by A46, A95, XBOOLE_0:def_5;
then L2 . u = 0 by RLVECT_2:19;
then A97: (1 - r) * (L2 . u) = 0 ;
L . u = 0 + 0 by A95, RLVECT_2:19;
hence L . u = ((r * L1) + ((1 - r) * L2)) . u by A88, A96, A97, RLVECT_2:def_11; ::_thesis: verum
end;
end;
end;
take L1 ; ::_thesis: ex 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 )
take L2 ; ::_thesis: 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 )
take r ; ::_thesis: ( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 )
f . (len f) = L . (F . (len f)) by A19, A30;
then r <> 0 by A2, A17, A16, RLVECT_2:19;
hence ( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 ) by A19, A30, A48, A86, A87, A84, CARD_1:30, CONVEX1:21, RLVECT_2:def_9; ::_thesis: verum
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
let V be RealLinearSpace; ::_thesis: 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
let M be non empty Subset of V; ::_thesis: ( M is convex implies { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M )
set S = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } ;
assume A1: M is convex ; ::_thesis: { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M
for v being set st v in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } holds
v in M
proof
let v be set ; ::_thesis: ( v in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } implies v in M )
assume v in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } ; ::_thesis: v in M
then consider L being Convex_Combination of M such that
A2: v = Sum L and
L in ConvexComb V ;
reconsider v = v as VECTOR of V by A2;
percases ( card (Carrier L) < 2 or card (Carrier L) >= 2 ) ;
supposeA3: card (Carrier L) < 2 ; ::_thesis: v in M
Carrier L <> 0 by CONVEX1:21;
then A4: card (Carrier L) >= 0 + 1 by NAT_1:13;
card (Carrier L) < 1 + 1 by A3;
then card (Carrier L) <= 1 by NAT_1:13;
then card (Carrier L) = 1 by A4, XXREAL_0:1;
then consider x being set such that
A5: Carrier L = {x} by CARD_2:42;
x in Carrier L by A5, TARSKI:def_1;
then reconsider x = x as VECTOR of V ;
A6: {x} c= M by A5, RLVECT_2:def_6;
v = (L . x) * x by A2, A5, RLVECT_2:35
.= 1 * x by A5, CONVEX1:27
.= x by RLVECT_1:def_8 ;
hence v in M by A6, ZFMISC_1:31; ::_thesis: verum
end;
supposeA7: card (Carrier L) >= 2 ; ::_thesis: v in M
defpred S1[ Nat] means for LL being Convex_Combination of M st card (Carrier LL) = 1 + $1 & ex L1, L2 being Convex_Combination of M ex r being Real st
( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) holds
Sum LL in M;
A8: S1[1]
proof
let LL be Convex_Combination of M; ::_thesis: ( card (Carrier LL) = 1 + 1 & ex L1, L2 being Convex_Combination of M ex r being Real st
( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) implies Sum LL in M )
assume that
A9: card (Carrier LL) = 1 + 1 and
A10: ex L1, L2 being Convex_Combination of M ex r being Real st
( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) ; ::_thesis: Sum LL in M
consider L1, L2 being Convex_Combination of M, r being Real such that
A11: ( 0 < r & r < 1 ) and
A12: LL = (r * L1) + ((1 - r) * L2) and
A13: card (Carrier L1) = 1 and
A14: card (Carrier L2) = (card (Carrier LL)) - 1 by A10;
consider x2 being set such that
A15: Carrier L2 = {x2} by A9, A14, CARD_2:42;
x2 in Carrier L2 by A15, TARSKI:def_1;
then reconsider x2 = x2 as VECTOR of V ;
( Sum L2 = (L2 . x2) * x2 & L2 . x2 = 1 ) by A15, CONVEX1:27, RLVECT_2:35;
then A16: Sum L2 = x2 by RLVECT_1:def_8;
{x2} c= M by A15, RLVECT_2:def_6;
then A17: Sum L2 in M by A16, ZFMISC_1:31;
consider x1 being set such that
A18: Carrier L1 = {x1} by A13, CARD_2:42;
x1 in Carrier L1 by A18, TARSKI:def_1;
then reconsider x1 = x1 as VECTOR of V ;
( Sum L1 = (L1 . x1) * x1 & L1 . x1 = 1 ) by A18, CONVEX1:27, RLVECT_2:35;
then A19: Sum L1 = x1 by RLVECT_1:def_8;
{x1} c= M by A18, RLVECT_2:def_6;
then A20: Sum L1 in M by A19, ZFMISC_1:31;
Sum LL = (Sum (r * L1)) + (Sum ((1 - r) * L2)) by A12, RLVECT_3:1
.= (r * (Sum L1)) + (Sum ((1 - r) * L2)) by RLVECT_3:2
.= (r * (Sum L1)) + ((1 - r) * (Sum L2)) by RLVECT_3:2 ;
hence Sum LL in M by A1, A11, A20, A17, CONVEX1:def_2; ::_thesis: verum
end;
consider k being Nat such that
A21: card (Carrier L) = k + 1 by A7, NAT_1:6;
reconsider k = k as non empty Element of NAT by A7, A21, ORDINAL1:def_12;
A22: card (Carrier L) = 1 + k by A21;
A23: 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 ) by A7, Lm2;
A24: for k being non empty Nat st S1[k] holds
S1[k + 1]
proof
let k be non empty Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A25: S1[k] ; ::_thesis: S1[k + 1]
let LL be Convex_Combination of M; ::_thesis: ( card (Carrier LL) = 1 + (k + 1) & ex L1, L2 being Convex_Combination of M ex r being Real st
( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) implies Sum LL in M )
assume that
A26: card (Carrier LL) = 1 + (k + 1) and
A27: ex L1, L2 being Convex_Combination of M ex r being Real st
( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) ; ::_thesis: Sum LL in M
consider L1, L2 being Convex_Combination of M, r being Real such that
A28: ( 0 < r & r < 1 ) and
A29: LL = (r * L1) + ((1 - r) * L2) and
A30: card (Carrier L1) = 1 and
A31: card (Carrier L2) = (card (Carrier LL)) - 1 by A27;
k >= 0 + 1 by NAT_1:13;
then k + 1 >= 1 + 1 by XREAL_1:6;
then ex LL1, LL2 being Convex_Combination of M ex rr being Real st
( 0 < rr & rr < 1 & L2 = (rr * LL1) + ((1 - rr) * LL2) & card (Carrier LL1) = 1 & card (Carrier LL2) = (card (Carrier L2)) - 1 ) by A26, A31, Lm2;
then A32: Sum L2 in M by A25, A26, A31;
consider x1 being set such that
A33: Carrier L1 = {x1} by A30, CARD_2:42;
x1 in Carrier L1 by A33, TARSKI:def_1;
then reconsider x1 = x1 as VECTOR of V ;
( Sum L1 = (L1 . x1) * x1 & L1 . x1 = 1 ) by A33, CONVEX1:27, RLVECT_2:35;
then A34: Sum L1 = x1 by RLVECT_1:def_8;
{x1} c= M by A33, RLVECT_2:def_6;
then A35: Sum L1 in M by A34, ZFMISC_1:31;
Sum LL = (Sum (r * L1)) + (Sum ((1 - r) * L2)) by A29, RLVECT_3:1
.= (r * (Sum L1)) + (Sum ((1 - r) * L2)) by RLVECT_3:2
.= (r * (Sum L1)) + ((1 - r) * (Sum L2)) by RLVECT_3:2 ;
hence Sum LL in M by A1, A28, A35, A32, CONVEX1:def_2; ::_thesis: verum
end;
for k being non empty Nat holds S1[k] from NAT_1:sch_10(A8, A24);
hence v in M by A2, A22, A23; ::_thesis: verum
end;
end;
end;
hence { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M by TARSKI:def_3; ::_thesis: verum
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;
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 }
proof
let V be RealLinearSpace; ::_thesis: for M being non empty Subset of V holds conv M = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V }
let M be non empty Subset of V; ::_thesis: conv M = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V }
consider m being set such that
A1: m in M by XBOOLE_0:def_1;
reconsider m = m as VECTOR of V by A1;
consider LL being Convex_Combination of V such that
A2: Sum LL = m and
A3: for A being non empty Subset of V st m in A holds
LL is Convex_Combination of A by Th1;
reconsider LL = LL as Convex_Combination of M by A1, A3;
LL in ConvexComb V by Def1;
then m in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } by A2;
then reconsider N = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } as non empty set ;
for x being set st x in N holds
x in the carrier of V
proof
let x be set ; ::_thesis: ( x in N implies x in the carrier of V )
assume x in N ; ::_thesis: x in the carrier of V
then ex L being Convex_Combination of M st
( x = Sum L & L in ConvexComb V ) ;
hence x in the carrier of V ; ::_thesis: verum
end;
then reconsider N = N as Subset of V by TARSKI:def_3;
for x being set st x in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } holds
x in conv M
proof
let x be set ; ::_thesis: ( x in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } implies x in conv M )
assume x in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } ; ::_thesis: x in conv M
then A4: ex L being Convex_Combination of M st
( x = Sum L & L in ConvexComb V ) ;
M c= conv M by CONVEX1:41;
hence x in conv M by A4, CONVEX2:6; ::_thesis: verum
end;
then A5: { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= conv M by TARSKI:def_3;
for u, v being VECTOR of V
for r being Real st 0 < r & r < 1 & u in N & v in N holds
(r * u) + ((1 - r) * v) in N
proof
let u, v be VECTOR of V; ::_thesis: for r being Real st 0 < r & r < 1 & u in N & v in N holds
(r * u) + ((1 - r) * v) in N
let r be Real; ::_thesis: ( 0 < r & r < 1 & u in N & v in N implies (r * u) + ((1 - r) * v) in N )
assume that
A6: ( 0 < r & r < 1 ) and
A7: u in N and
A8: v in N ; ::_thesis: (r * u) + ((1 - r) * v) in N
consider Lv being Convex_Combination of M such that
A9: v = Sum Lv and
Lv in ConvexComb V by A8;
consider Lu being Convex_Combination of M such that
A10: u = Sum Lu and
Lu in ConvexComb V by A7;
reconsider LL = (r * Lu) + ((1 - r) * Lv) as Convex_Combination of M by A6, CONVEX2:9;
(r * Lu) + ((1 - r) * Lv) is Convex_Combination of V by A6, CONVEX2:8;
then A11: (r * Lu) + ((1 - r) * Lv) in ConvexComb V by Def1;
Sum LL = (Sum (r * Lu)) + (Sum ((1 - r) * Lv)) by RLVECT_3:1
.= (r * (Sum Lu)) + (Sum ((1 - r) * Lv)) by RLVECT_3:2
.= (r * (Sum Lu)) + ((1 - r) * (Sum Lv)) by RLVECT_3:2 ;
hence (r * u) + ((1 - r) * v) in N by A10, A9, A11; ::_thesis: verum
end;
then A12: N is convex by CONVEX1:def_2;
for v being set st v in M holds
v in N
proof
let v be set ; ::_thesis: ( v in M implies v in N )
assume A13: v in M ; ::_thesis: v in N
then reconsider v = v as VECTOR of V ;
consider LL being Convex_Combination of V such that
A14: Sum LL = v and
A15: for A being non empty Subset of V st v in A holds
LL is Convex_Combination of A by Th1;
reconsider LL = LL as Convex_Combination of M by A13, A15;
LL in ConvexComb V by Def1;
hence v in N by A14; ::_thesis: verum
end;
then M c= N by TARSKI:def_3;
then conv M c= N by A12, CONVEX1:30;
hence conv M = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
definition
let V be non empty RLSStruct ;
let M be Subset of V;
attrM is cone means :Def3: :: CONVEX3:def 3
for r being Real
for v being VECTOR of V st r > 0 & v in M holds
r * v in M;
end;
:: 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 );
theorem Th6: :: CONVEX3:6
for V being non empty RLSStruct
for M being Subset of V st M = {} holds
M is cone
proof
let V be non empty RLSStruct ; ::_thesis: for M being Subset of V st M = {} holds
M is cone
let M be Subset of V; ::_thesis: ( M = {} implies M is cone )
A1: for r being Real
for v being VECTOR of V st r > 0 & v in {} holds
r * v in {} ;
assume M = {} ; ::_thesis: M is cone
hence M is cone by A1, Def3; ::_thesis: verum
end;
registration
let V be non empty RLSStruct ;
cluster cone for Element of K32( the carrier of V);
existence
ex b1 being Subset of V st b1 is cone
proof
{} V is cone by Th6;
hence ex b1 being Subset of V st b1 is cone ; ::_thesis: verum
end;
end;
registration
let V be non empty RLSStruct ;
cluster empty cone for Element of K32( the carrier of V);
existence
ex b1 being Subset of V st
( b1 is empty & b1 is cone )
proof
set M = {} ;
reconsider M = {} as Subset of V by XBOOLE_1:2;
reconsider M = M as cone Subset of V by Th6;
take M ; ::_thesis: ( M is empty & M is cone )
thus ( M is empty & M is cone ) ; ::_thesis: verum
end;
end;
registration
let V be RealLinearSpace;
cluster non empty cone for Element of K32( the carrier of V);
existence
ex b1 being Subset of V st
( not b1 is empty & b1 is cone )
proof
set M = {(0. V)};
reconsider M = {(0. V)} as Subset of V ;
for r being Real
for v being VECTOR of V st r > 0 & v in M holds
r * v in M
proof
let r be Real; ::_thesis: for v being VECTOR of V st r > 0 & v in M holds
r * v in M
let v be VECTOR of V; ::_thesis: ( r > 0 & v in M implies r * v in M )
assume that
r > 0 and
A1: v in M ; ::_thesis: r * v in M
v = 0. V by A1, TARSKI:def_1;
then r * v = 0. V by RLVECT_1:10;
hence r * v in M by TARSKI:def_1; ::_thesis: verum
end;
then reconsider M = M as cone Subset of V by Def3;
take M ; ::_thesis: ( not M is empty & M is cone )
thus ( not M is empty & M is cone ) ; ::_thesis: verum
end;
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 )
proof
let V be non empty RLSStruct ; ::_thesis: 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 )
let M be cone Subset of V; ::_thesis: ( V is vector-distributive & V is scalar-distributive & V is scalar-associative & V is scalar-unital implies ( M is convex iff for u, v being VECTOR of V st u in M & v in M holds
u + v in M ) )
A1: ( ( for u, v being VECTOR of V st u in M & v in M holds
u + v in M ) implies M is convex )
proof
assume A2: for u, v being VECTOR of V st u in M & v in M holds
u + v in M ; ::_thesis: M is convex
for u, v being VECTOR of V
for r being Real st 0 < r & r < 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M
proof
let u, v be VECTOR of V; ::_thesis: for r being Real st 0 < r & r < 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M
let r be Real; ::_thesis: ( 0 < r & r < 1 & u in M & v in M implies (r * u) + ((1 - r) * v) in M )
assume that
A3: 0 < r and
A4: r < 1 and
A5: u in M and
A6: v in M ; ::_thesis: (r * u) + ((1 - r) * v) in M
r + 0 < 1 by A4;
then 1 - r > 0 by XREAL_1:20;
then A7: (1 - r) * v in M by A6, Def3;
r * u in M by A3, A5, Def3;
hence (r * u) + ((1 - r) * v) in M by A2, A7; ::_thesis: verum
end;
hence M is convex by CONVEX1:def_2; ::_thesis: verum
end;
assume A8: ( V is vector-distributive & V is scalar-distributive & V is scalar-associative & V is scalar-unital ) ; ::_thesis: ( M is convex iff for u, v being VECTOR of V st u in M & v in M holds
u + v in M )
( M is convex implies for u, v being VECTOR of V st u in M & v in M holds
u + v in M )
proof
assume A9: M is convex ; ::_thesis: for u, v being VECTOR of V st u in M & v in M holds
u + v in M
for u, v being VECTOR of V st u in M & v in M holds
u + v in M
proof
let u, v be VECTOR of V; ::_thesis: ( u in M & v in M implies u + v in M )
assume ( u in M & v in M ) ; ::_thesis: u + v in M
then ((1 / 2) * u) + ((1 - (1 / 2)) * v) in M by A9, CONVEX1:def_2;
then A10: 2 * (((1 / 2) * u) + ((1 / 2) * v)) in M by Def3;
2 * (((1 / 2) * u) + ((1 / 2) * v)) = (2 * ((1 / 2) * u)) + (2 * ((1 / 2) * v)) by A8, RLVECT_1:def_5
.= ((2 * (1 / 2)) * u) + (2 * ((1 / 2) * v)) by A8, RLVECT_1:def_7
.= (1 * u) + ((2 * (1 / 2)) * v) by A8, RLVECT_1:def_7
.= u + (1 * v) by A8, RLVECT_1:def_8 ;
hence u + v in M by A8, A10, RLVECT_1:def_8; ::_thesis: verum
end;
hence for u, v being VECTOR of V st u in M & v in M holds
u + v in M ; ::_thesis: verum
end;
hence ( M is convex iff for u, v being VECTOR of V st u in M & v in M holds
u + v in M ) by A1; ::_thesis: verum
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
let V be RealLinearSpace; ::_thesis: 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 ) )
let M be Subset of V; ::_thesis: 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 ) )
let L be Linear_Combination of M; ::_thesis: ( card (Carrier L) >= 1 implies 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 ) ) )
assume card (Carrier L) >= 1 ; ::_thesis: 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 ) )
then Carrier L <> {} ;
then consider u being set such that
A1: u in Carrier L by XBOOLE_0:def_1;
reconsider u = u as VECTOR of V by A1;
consider L1 being Linear_Combination of {u} such that
A2: L1 . u = L . u by RLVECT_4:37;
A3: Carrier L1 c= {u} by RLVECT_2:def_6;
Carrier L c= M by RLVECT_2:def_6;
then {u} c= M by A1, ZFMISC_1:31;
then Carrier L1 c= M by A3, XBOOLE_1:1;
then reconsider L1 = L1 as Linear_Combination of M by RLVECT_2:def_6;
A4: for v being VECTOR of V st v in Carrier L1 holds
L1 . v = L . v
proof
let v be VECTOR of V; ::_thesis: ( v in Carrier L1 implies L1 . v = L . v )
assume v in Carrier L1 ; ::_thesis: L1 . v = L . v
then v = u by A3, TARSKI:def_1;
hence L1 . v = L . v by A2; ::_thesis: verum
end;
defpred S1[ set , set ] means ( ( $1 in (Carrier L) \ {u} implies $2 = L . $1 ) & ( not $1 in (Carrier L) \ {u} implies $2 = 0 ) );
A5: for x being set st x in the carrier of V holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier of V implies ex y being set st S1[x,y] )
assume x in the carrier of V ; ::_thesis: ex y being set st S1[x,y]
( x in (Carrier L) \ {u} or not x in (Carrier L) \ {u} ) ;
hence ex y being set st S1[x,y] ; ::_thesis: verum
end;
consider L2 being Function such that
A6: ( dom L2 = the carrier of V & ( for x being set st x in the carrier of V holds
S1[x,L2 . x] ) ) from CLASSES1:sch_1(A5);
for y being set st y in rng L2 holds
y in REAL
proof
let y be set ; ::_thesis: ( y in rng L2 implies y in REAL )
assume y in rng L2 ; ::_thesis: y in REAL
then consider x being set such that
A7: x in dom L2 and
A8: y = L2 . x by FUNCT_1:def_3;
percases ( x in (Carrier L) \ {u} or not x in (Carrier L) \ {u} ) ;
supposeA9: x in (Carrier L) \ {u} ; ::_thesis: y in REAL
then reconsider x = x as VECTOR of V ;
y = L . x by A6, A8, A9;
hence y in REAL ; ::_thesis: verum
end;
suppose not x in (Carrier L) \ {u} ; ::_thesis: y in REAL
then y = 0 by A6, A7, A8;
hence y in REAL ; ::_thesis: verum
end;
end;
end;
then rng L2 c= REAL by TARSKI:def_3;
then A10: L2 is Element of Funcs ( the carrier of V,REAL) by A6, FUNCT_2:def_2;
ex T being finite Subset of V st
for v being Element of V st not v in T holds
L2 . v = 0
proof
set T = (Carrier L) \ {u};
reconsider T = (Carrier L) \ {u} as finite Subset of V ;
take T ; ::_thesis: for v being Element of V st not v in T holds
L2 . v = 0
thus for v being Element of V st not v in T holds
L2 . v = 0 by A6; ::_thesis: verum
end;
then reconsider L2 = L2 as Linear_Combination of V by A10, RLVECT_2:def_3;
for x being set st x in Carrier L2 holds
x in M
proof
let x be set ; ::_thesis: ( x in Carrier L2 implies x in M )
assume A11: x in Carrier L2 ; ::_thesis: x in M
then reconsider x = x as VECTOR of V ;
L2 . x <> 0 by A11, RLVECT_2:19;
then x in (Carrier L) \ {u} by A6;
then A12: x in Carrier L by XBOOLE_0:def_5;
Carrier L c= M by RLVECT_2:def_6;
hence x in M by A12; ::_thesis: verum
end;
then Carrier L2 c= M by TARSKI:def_3;
then reconsider L2 = L2 as Linear_Combination of M by RLVECT_2:def_6;
for x being set st x in Carrier L2 holds
x in (Carrier L) \ {u}
proof
let x be set ; ::_thesis: ( x in Carrier L2 implies x in (Carrier L) \ {u} )
assume A13: x in Carrier L2 ; ::_thesis: x in (Carrier L) \ {u}
then reconsider x = x as VECTOR of V ;
L2 . x <> 0 by A13, RLVECT_2:19;
hence x in (Carrier L) \ {u} by A6; ::_thesis: verum
end;
then A14: Carrier L2 c= (Carrier L) \ {u} by TARSKI:def_3;
for v being VECTOR of V holds L . v = (L1 + L2) . v
proof
let v be VECTOR of V; ::_thesis: L . v = (L1 + L2) . v
percases ( v in Carrier L or not v in Carrier L ) ;
supposeA15: v in Carrier L ; ::_thesis: L . v = (L1 + L2) . v
percases ( v = u or v <> u ) ;
supposeA16: v = u ; ::_thesis: L . v = (L1 + L2) . v
then A17: not v in Carrier L2 by A14, ZFMISC_1:56;
(L1 + L2) . v = (L1 . v) + (L2 . v) by RLVECT_2:def_10
.= (L . v) + 0 by A2, A16, A17, RLVECT_2:19 ;
hence L . v = (L1 + L2) . v ; ::_thesis: verum
end;
supposeA18: v <> u ; ::_thesis: L . v = (L1 + L2) . v
then not v in Carrier L1 by A3, TARSKI:def_1;
then A19: L1 . v = 0 by RLVECT_2:19;
A20: v in (Carrier L) \ {u} by A15, A18, ZFMISC_1:56;
(L1 + L2) . v = (L1 . v) + (L2 . v) by RLVECT_2:def_10
.= 0 + (L . v) by A6, A19, A20 ;
hence L . v = (L1 + L2) . v ; ::_thesis: verum
end;
end;
end;
supposeA21: not v in Carrier L ; ::_thesis: L . v = (L1 + L2) . v
then not v in Carrier L2 by A14, ZFMISC_1:56;
then A22: L2 . v = 0 by RLVECT_2:19;
A23: not v in Carrier L1 by A1, A3, A21, TARSKI:def_1;
(L1 + L2) . v = (L1 . v) + (L2 . v) by RLVECT_2:def_10
.= 0 by A23, A22, RLVECT_2:19 ;
hence L . v = (L1 + L2) . v by A21, RLVECT_2:19; ::_thesis: verum
end;
end;
end;
then A24: L = L1 + L2 by RLVECT_2:def_9;
for x being set st x in (Carrier L) \ {u} holds
x in Carrier L2
proof
let x be set ; ::_thesis: ( x in (Carrier L) \ {u} implies x in Carrier L2 )
assume A25: x in (Carrier L) \ {u} ; ::_thesis: x in Carrier L2
then reconsider x = x as VECTOR of V ;
x in Carrier L by A25, XBOOLE_0:def_5;
then A26: L . x <> 0 by RLVECT_2:19;
L2 . x = L . x by A6, A25;
hence x in Carrier L2 by A26, RLVECT_2:19; ::_thesis: verum
end;
then (Carrier L) \ {u} c= Carrier L2 by TARSKI:def_3;
then A27: Carrier L2 = (Carrier L) \ {u} by A14, XBOOLE_0:def_10;
take L1 ; ::_thesis: ex 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 ) )
take L2 ; ::_thesis: ( 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 ) )
A28: (Carrier L) \ {u} c= Carrier L by XBOOLE_1:36;
Carrier L1 <> {}
proof
assume Carrier L1 = {} ; ::_thesis: contradiction
then L . u = 0 by A2, RLVECT_2:19;
hence contradiction by A1, RLVECT_2:19; ::_thesis: verum
end;
then A29: Carrier L1 = {u} by A3, ZFMISC_1:33;
then Carrier L1 c= Carrier L by A1, ZFMISC_1:31;
then card (Carrier L2) = (card (Carrier L)) - (card (Carrier L1)) by A29, A27, CARD_2:44
.= (card (Carrier L)) - 1 by A29, CARD_1:30 ;
hence ( 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 ) ) by A1, A4, A6, A29, A14, A24, A28, CARD_1:30, RLVECT_3:1, XBOOLE_1:1, ZFMISC_1:31; ::_thesis: verum
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 )
proof
let V be RealLinearSpace; ::_thesis: 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 )
let M be Subset of V; ::_thesis: ( ( 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 )
A1: ( ( 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 ) implies ( M is convex & M is cone ) )
proof
assume A2: 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 ; ::_thesis: ( M is convex & M is cone )
A3: for r being Real
for v being VECTOR of V st r > 0 & v in M holds
r * v in M
proof
let r be Real; ::_thesis: for v being VECTOR of V st r > 0 & v in M holds
r * v in M
let v be VECTOR of V; ::_thesis: ( r > 0 & v in M implies r * v in M )
assume that
A4: r > 0 and
A5: v in M ; ::_thesis: r * v in M
consider L being Linear_Combination of {v} such that
A6: L . v = r by RLVECT_4:37;
A7: for u being VECTOR of V st u in Carrier L holds
L . u > 0
proof
let u be VECTOR of V; ::_thesis: ( u in Carrier L implies L . u > 0 )
A8: Carrier L c= {v} by RLVECT_2:def_6;
assume u in Carrier L ; ::_thesis: L . u > 0
hence L . u > 0 by A4, A6, A8, TARSKI:def_1; ::_thesis: verum
end;
A9: v in Carrier L by A4, A6, RLVECT_2:19;
{v} c= M by A5, ZFMISC_1:31;
then reconsider L = L as Linear_Combination of M by RLVECT_2:21;
Sum L in M by A2, A9, A7;
hence r * v in M by A6, RLVECT_2:32; ::_thesis: verum
end;
A10: for u, v being VECTOR of V st u in M & v in M holds
u + v in M
proof
let u, v be VECTOR of V; ::_thesis: ( u in M & v in M implies u + v in M )
assume that
A11: u in M and
A12: v in M ; ::_thesis: u + v in M
percases ( u <> v or u = v ) ;
supposeA13: u <> v ; ::_thesis: u + v in M
consider L being Linear_Combination of {u,v} such that
A14: ( L . u = 1 & L . v = 1 ) by A13, RLVECT_4:38;
A15: Sum L = (1 * u) + (1 * v) by A13, A14, RLVECT_2:33
.= u + (1 * v) by RLVECT_1:def_8
.= u + v by RLVECT_1:def_8 ;
A16: Carrier L <> {} by A14, RLVECT_2:19;
A17: for v1 being VECTOR of V st v1 in Carrier L holds
L . v1 > 0
proof
let v1 be VECTOR of V; ::_thesis: ( v1 in Carrier L implies L . v1 > 0 )
A18: Carrier L c= {u,v} by RLVECT_2:def_6;
assume A19: v1 in Carrier L ; ::_thesis: L . v1 > 0
percases ( v1 = u or v1 = v ) by A19, A18, TARSKI:def_2;
suppose v1 = u ; ::_thesis: L . v1 > 0
hence L . v1 > 0 by A14; ::_thesis: verum
end;
suppose v1 = v ; ::_thesis: L . v1 > 0
hence L . v1 > 0 by A14; ::_thesis: verum
end;
end;
end;
{u,v} c= M by A11, A12, ZFMISC_1:32;
then reconsider L = L as Linear_Combination of M by RLVECT_2:21;
Sum L in M by A2, A16, A17;
hence u + v in M by A15; ::_thesis: verum
end;
supposeA20: u = v ; ::_thesis: u + v in M
(1 + 1) * u in M by A3, A11;
then (1 * u) + (1 * u) in M by RLVECT_1:def_6;
then u + (1 * u) in M by RLVECT_1:def_8;
hence u + v in M by A20, RLVECT_1:def_8; ::_thesis: verum
end;
end;
end;
M is cone by A3, Def3;
hence ( M is convex & M is cone ) by A10, Th7; ::_thesis: verum
end;
( M is convex & M is cone implies 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
defpred S1[ Nat] means for LL being Linear_Combination of M st card (Carrier LL) = $1 & ( for u being VECTOR of V st u in Carrier LL holds
LL . u > 0 ) & ex L1, L2 being Linear_Combination of M st
( Sum LL = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 & Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL & ( for v being VECTOR of V st v in Carrier L1 holds
L1 . v = LL . v ) & ( for v being VECTOR of V st v in Carrier L2 holds
L2 . v = LL . v ) ) holds
Sum LL in M;
assume that
A21: M is convex and
A22: M is cone ; ::_thesis: 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
A23: S1[1]
proof
let LL be Linear_Combination of M; ::_thesis: ( card (Carrier LL) = 1 & ( for u being VECTOR of V st u in Carrier LL holds
LL . u > 0 ) & ex L1, L2 being Linear_Combination of M st
( Sum LL = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 & Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL & ( for v being VECTOR of V st v in Carrier L1 holds
L1 . v = LL . v ) & ( for v being VECTOR of V st v in Carrier L2 holds
L2 . v = LL . v ) ) implies Sum LL in M )
assume that
A24: card (Carrier LL) = 1 and
A25: for u being VECTOR of V st u in Carrier LL holds
LL . u > 0 and
ex L1, L2 being Linear_Combination of M st
( Sum LL = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 & Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL & ( for v being VECTOR of V st v in Carrier L1 holds
L1 . v = LL . v ) & ( for v being VECTOR of V st v in Carrier L2 holds
L2 . v = LL . v ) ) ; ::_thesis: Sum LL in M
consider x being set such that
A26: Carrier LL = {x} by A24, CARD_2:42;
{x} c= M by A26, RLVECT_2:def_6;
then A27: x in M by ZFMISC_1:31;
then reconsider x = x as VECTOR of V ;
x in Carrier LL by A26, TARSKI:def_1;
then A28: LL . x > 0 by A25;
Sum LL = (LL . x) * x by A26, RLVECT_2:35;
hence Sum LL in M by A22, A27, A28, Def3; ::_thesis: verum
end;
A29: for k being non empty Nat st S1[k] holds
S1[k + 1]
proof
let k be non empty Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A30: S1[k] ; ::_thesis: S1[k + 1]
let LL be Linear_Combination of M; ::_thesis: ( card (Carrier LL) = k + 1 & ( for u being VECTOR of V st u in Carrier LL holds
LL . u > 0 ) & ex L1, L2 being Linear_Combination of M st
( Sum LL = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 & Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL & ( for v being VECTOR of V st v in Carrier L1 holds
L1 . v = LL . v ) & ( for v being VECTOR of V st v in Carrier L2 holds
L2 . v = LL . v ) ) implies Sum LL in M )
assume that
A31: card (Carrier LL) = k + 1 and
A32: for u being VECTOR of V st u in Carrier LL holds
LL . u > 0 and
A33: ex L1, L2 being Linear_Combination of M st
( Sum LL = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 & Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL & ( for v being VECTOR of V st v in Carrier L1 holds
L1 . v = LL . v ) & ( for v being VECTOR of V st v in Carrier L2 holds
L2 . v = LL . v ) ) ; ::_thesis: Sum LL in M
consider L1, L2 being Linear_Combination of M such that
A34: Sum LL = (Sum L1) + (Sum L2) and
A35: card (Carrier L1) = 1 and
A36: card (Carrier L2) = (card (Carrier LL)) - 1 and
A37: Carrier L1 c= Carrier LL and
A38: Carrier L2 c= Carrier LL and
A39: for v being VECTOR of V st v in Carrier L1 holds
L1 . v = LL . v and
A40: for v being VECTOR of V st v in Carrier L2 holds
L2 . v = LL . v by A33;
A41: for u being VECTOR of V st u in Carrier L1 holds
L1 . u > 0
proof
let u be VECTOR of V; ::_thesis: ( u in Carrier L1 implies L1 . u > 0 )
assume A42: u in Carrier L1 ; ::_thesis: L1 . u > 0
then L1 . u = LL . u by A39;
hence L1 . u > 0 by A32, A37, A42; ::_thesis: verum
end;
A43: for u being VECTOR of V st u in Carrier L2 holds
L2 . u > 0
proof
let u be VECTOR of V; ::_thesis: ( u in Carrier L2 implies L2 . u > 0 )
assume A44: u in Carrier L2 ; ::_thesis: L2 . u > 0
then L2 . u = LL . u by A40;
hence L2 . u > 0 by A32, A38, A44; ::_thesis: verum
end;
ex LL1, LL2 being Linear_Combination of M st
( Sum L1 = (Sum LL1) + (Sum LL2) & card (Carrier LL1) = 1 & card (Carrier LL2) = (card (Carrier L1)) - 1 & Carrier LL1 c= Carrier L1 & Carrier LL2 c= Carrier L1 & ( for v being VECTOR of V st v in Carrier LL1 holds
LL1 . v = L1 . v ) & ( for v being VECTOR of V st v in Carrier LL2 holds
LL2 . v = L1 . v ) ) by A35, Lm4;
then A45: Sum L1 in M by A23, A35, A41;
card (Carrier L2) >= 0 + 1 by A31, A36, NAT_1:13;
then ex LL1, LL2 being Linear_Combination of M st
( Sum L2 = (Sum LL1) + (Sum LL2) & card (Carrier LL1) = 1 & card (Carrier LL2) = (card (Carrier L2)) - 1 & Carrier LL1 c= Carrier L2 & Carrier LL2 c= Carrier L2 & ( for v being VECTOR of V st v in Carrier LL1 holds
LL1 . v = L2 . v ) & ( for v being VECTOR of V st v in Carrier LL2 holds
LL2 . v = L2 . v ) ) by Lm4;
then Sum L2 in M by A30, A31, A36, A43;
hence Sum LL in M by A21, A22, A34, A45, Th7; ::_thesis: verum
end;
A46: for k being non empty Nat holds S1[k] from NAT_1:sch_10(A23, A29);
let L be Linear_Combination of M; ::_thesis: ( Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds
L . v > 0 ) implies Sum L in M )
assume that
A47: Carrier L <> {} and
A48: for v being VECTOR of V st v in Carrier L holds
L . v > 0 ; ::_thesis: Sum L in M
card (Carrier L) >= 0 + 1 by A47, NAT_1:13;
then 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 ) ) by Lm4;
hence Sum L in M by A47, A48, A46; ::_thesis: verum
end;
hence ( ( 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 ) by A1; ::_thesis: verum
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
proof
let V be non empty RLSStruct ; ::_thesis: for M, N being Subset of V st M is cone & N is cone holds
M /\ N is cone
let M, N be Subset of V; ::_thesis: ( M is cone & N is cone implies M /\ N is cone )
assume that
A1: M is cone and
A2: N is cone ; ::_thesis: M /\ N is cone
let r be Real; :: according to CONVEX3:def_3 ::_thesis: for v being VECTOR of V st r > 0 & v in M /\ N holds
r * v in M /\ N
let v be VECTOR of V; ::_thesis: ( r > 0 & v in M /\ N implies r * v in M /\ N )
assume that
A3: r > 0 and
A4: v in M /\ N ; ::_thesis: r * v in M /\ N
v in N by A4, XBOOLE_0:def_4;
then A5: r * v in N by A2, A3, Def3;
v in M by A4, XBOOLE_0:def_4;
then r * v in M by A1, A3, Def3;
hence r * v in M /\ N by A5, XBOOLE_0:def_4; ::_thesis: verum
end;