Copyright (c) 2003 Association of Mizar Users
environ
vocabulary RLVECT_1, FUNCT_1, ARYTM_1, RELAT_1, FINSEQ_1, BOOLE, JORDAN1,
ARYTM_3, CONVEX1, FINSEQ_4, SEQ_1, CARD_1, RLVECT_2, FUNCT_2, RFINSEQ,
FINSET_1, CONVEX2, CONVEX3;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1,
FINSEQ_1, RELAT_1, FUNCT_1, FINSET_1, CARD_1, NAT_1, STRUCT_0, FUNCT_2,
RLVECT_1, FINSEQ_4, RLVECT_2, RVSUM_1, CONVEX1, TOPREAL1, RFINSEQ,
CONVEX2;
constructors REAL_1, SEQ_1, RUSUB_5, FINSEQ_4, CONVEX1, NAT_1, MONOID_0,
TOPREAL1, RFINSEQ, MEMBERED;
clusters RELSET_1, ARYTM_3, STRUCT_0, RLVECT_1, SEQ_1, RUSUB_4, BINARITH,
XREAL_0, MEMBERED, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
theorems RLVECT_1, RVSUM_1, FUNCT_1, FINSEQ_1, TARSKI, ZFMISC_1, REAL_1,
XBOOLE_0, REAL_2, AXIOMS, XBOOLE_1, RLVECT_2, CARD_1, FINSEQ_3, FINSEQ_4,
ENUMSET1, CONVEX1, FUNCT_2, NAT_1, TOPREAL1, RFINSEQ, SQUARE_1, CONVEX2,
RLVECT_3, CARD_2, CARD_4, FINSEQ_5, PARTFUN2, GRAPH_5, RELAT_1, XCMPLX_1;
schemes BINARITH, RLVECT_4, XBOOLE_0, FINSEQ_1, FUNCT_1;
begin :: Equality of Convex Hull and Set of Convex Combinations
definition let V be RealLinearSpace;
defpred P[set] means $1 is Convex_Combination of V;
func ConvexComb(V) -> set means :Def1:
for L being set holds
L in it iff L is Convex_Combination of V;
existence
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) & P[x] from Separation;
take A;
let L be set;
thus L in A implies L is Convex_Combination of V by A1;
assume L is Convex_Combination of V;
hence thesis by A1;
end;
uniqueness
proof
thus for X1,X2 being set st
(for x being set holds x in X1 iff P[x]) &
(for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
end;
end;
definition let V be RealLinearSpace, M be non empty Subset of V;
defpred P[set] means $1 is Convex_Combination of M;
func ConvexComb(M) -> set means
for L being set holds
L in it iff L is Convex_Combination of M;
existence
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) & P[x] from Separation;
take A;
let L be set;
thus L in A implies L is Convex_Combination of M by A1;
assume L is Convex_Combination of M;
hence thesis by A1;
end;
uniqueness
proof
thus for X1,X2 being set st
(for x being set holds x in X1 iff P[x]) &
(for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
end;
end;
theorem Th1:
for V being RealLinearSpace, v being VECTOR of V holds
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;
let v be VECTOR of V;
consider L being Linear_Combination of {v} such that
A1:L.v = 1 from LinCEx1;
A2:Carrier(L) c= {v} by RLVECT_2:def 8;
v in Carrier(L) by A1,RLVECT_2:28;
then {v} c= Carrier(L) by ZFMISC_1:37;
then A3:{v} = Carrier(L) by A2,XBOOLE_0:def 10;
consider F being FinSequence of the carrier of V such that
A4:F is one-to-one & rng F = Carrier(L) & Sum(L) = Sum(L (#) F)
by RLVECT_2:def 10;
deffunc F(set) = L.(F.$1);
consider f being FinSequence such that
A5:len f = len F &
for n being Nat st n in Seg(len F) holds f.n = F(n) from SeqLambda;
A6:len F = 1 by A3,A4,FINSEQ_3:105;
then 1 in Seg len F by FINSEQ_1:4,TARSKI:def 1;
then A7:f.1 = L.(F.1) by A5;
F = <*v*> by A3,A4,FINSEQ_3:106;
then A8:F.1 = v by FINSEQ_1:def 8;
rng f c= REAL
proof
f = <*1*> by A1,A5,A6,A7,A8,FINSEQ_1:57;
then rng f = {1} by FINSEQ_1:55;
hence thesis by ZFMISC_1:37;
end;
then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;
A9:f.1 >= 0 by A1,A7,A8;
f = <*1*> by A1,A5,A6,A7,A8,FINSEQ_1:57;
then A10:Sum(f) = 1 by RVSUM_1:103;
for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
proof
let n be Nat;
assume n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A5,A6,A9,FINSEQ_1:4,TARSKI:def 1;
end;
then reconsider L as Convex_Combination of V by A4,A5,A10,CONVEX1:def 3;
A11: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;
assume v in A;
then {v} c= A by ZFMISC_1:37;
hence thesis by A3,RLVECT_2:def 8;
end;
take L;
Sum(L) = 1 * v by A1,A3,RLVECT_2:53;
hence thesis by A11,RLVECT_1:def 9;
end;
theorem
for V being RealLinearSpace, 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;
let v1,v2 be VECTOR of V;
assume
A1:v1 <> v2;
consider L being Linear_Combination of {v1,v2} such that
A2:L.v1 = 1/2 & L.v2 = 1/2 from LinCEx2(A1);
A3:Carrier(L) c= {v1,v2} by RLVECT_2:def 8;
v1 in Carrier(L) & v2 in Carrier(L) by A2,RLVECT_2:28;
then {v1,v2} c= Carrier(L) by ZFMISC_1:38;
then A4:{v1,v2} = Carrier(L) by A3,XBOOLE_0:def 10;
consider F being FinSequence of the carrier of V such that
A5:F is one-to-one & rng F = Carrier(L) & Sum(L) = Sum(L (#) F)
by RLVECT_2:def 10;
deffunc F(set) = L.(F.$1);
consider f being FinSequence such that
A6:len f = len F &
for n being Nat st n in Seg(len F) holds f.n = F(n) from SeqLambda;
A7:len F = 2 by A1,A4,A5,FINSEQ_3:107;
then 1 in Seg len F & 2 in Seg len F by FINSEQ_1:3;
then A8:f.1 = L.(F.1) & f.2 = L.(F.2) by A6;
now per cases by A1,A4,A5,FINSEQ_3:108;
suppose F = <*v1,v2*>;
then A9: F.1 = v1 & F.2 = v2 by FINSEQ_1:61;
rng f c= REAL
proof
f = <*1/2,1/2*> by A2,A6,A7,A8,A9,FINSEQ_1:61;
then f = <*1/2*>^<*1/2*> by FINSEQ_1:def 9;
then rng f = rng <*1/2*> \/ rng <*1/2*> by FINSEQ_1:44
.= {1/2} by FINSEQ_1:55;
hence thesis by ZFMISC_1:37;
end;
then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;
A10: f.1 >= 0 & f.2 >= 0 by A2,A8,A9;
f = <*1/2,1/2*> by A2,A6,A7,A8,A9,FINSEQ_1:61;
then A11: Sum(f) = 1/2 + 1/2 by RVSUM_1:107 .= 1;
for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
proof
let n be Nat;
assume n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A6,A7,A10,FINSEQ_1:4,TARSKI:def 2;
end;
then reconsider L as Convex_Combination of V by A5,A6,A11,CONVEX1:def 3;
A12: for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A by A4,RLVECT_2:def 8;
take L;
thus thesis by A12;
suppose F = <*v2,v1*>;
then A13: F.1 = v2 & F.2 = v1 by FINSEQ_1:61;
rng f c= REAL
proof
f = <*1/2,1/2*> by A2,A6,A7,A8,A13,FINSEQ_1:61;
then f = <*1/2*>^<*1/2*> by FINSEQ_1:def 9;
then rng f = rng <*1/2*> \/ rng <*1/2*> by FINSEQ_1:44
.= {1/2} by FINSEQ_1:55;
hence thesis by ZFMISC_1:37;
end;
then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;
A14: f.1 >= 0 & f.2 >= 0 by A2,A8,A13;
f = <*1/2,1/2*> by A2,A6,A7,A8,A13,FINSEQ_1:61;
then A15: Sum(f) = 1/2 + 1/2 by RVSUM_1:107 .= 1;
for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
proof
let n be Nat;
assume n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A6,A7,A14,FINSEQ_1:4,TARSKI:def 2;
end;
then reconsider L as Convex_Combination of V by A5,A6,A15,CONVEX1:def 3;
A16: for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A by A4,RLVECT_2:def 8;
take L;
thus thesis by A16;
end;
hence thesis;
end;
theorem
for V being RealLinearSpace, 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;
let v1,v2,v3 be VECTOR of V;
assume that
A1:v1 <> v2 and
A2:v1 <> v3 and
A3:v2 <> v3;
consider L being Linear_Combination of {v1,v2,v3} such that
A4:L.v1 = 1/3 & L.v2 = 1/3 & L.v3 = 1/3 from LinCEx3(A1,A2,A3);
A5:Carrier(L) c= {v1,v2,v3} by RLVECT_2:def 8;
for x being set st x in {v1,v2,v3} holds x in Carrier(L)
proof
let x be set;
assume A6:x in {v1,v2,v3};
then reconsider x as VECTOR of V;
x = v1 or x = v2 or x = v3 by A6,ENUMSET1:13;
hence thesis by A4,RLVECT_2:28;
end;
then {v1,v2,v3} c= Carrier(L) by TARSKI:def 3;
then A7:{v1,v2,v3} = Carrier(L) by A5,XBOOLE_0:def 10;
consider F being FinSequence of the carrier of V such that
A8:F is one-to-one & rng F = Carrier(L) & Sum(L) = Sum(L (#) F)
by RLVECT_2:def 10;
deffunc F(set) = L.(F.$1);
consider f being FinSequence such that
A9:len f = len F &
for n being Nat st n in Seg(len F) holds f.n = F(n) from SeqLambda;
A10:len F = 3 by A1,A2,A3,A7,A8,FINSEQ_3:110;
then 1 in Seg len F & 2 in Seg len F & 3 in Seg len F by FINSEQ_1:3;
then A11:f.1 = L.(F.1) & f.2 = L.(F.2) & f.3 = L.(F.3) by A9;
now per cases by A1,A2,A3,A7,A8,CONVEX1:31;
suppose F = <*v1,v2,v3*>;
then A12: F.1 = v1 & F.2 = v2 & F.3 = v3 by FINSEQ_1:62;
rng f c= REAL
proof
f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A12,FINSEQ_1:62;
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:44
.= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44
.= {1/3} by FINSEQ_1:55;
hence thesis by ZFMISC_1:37;
end;
then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;
A13: f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A12;
f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A12,FINSEQ_1:62;
then A14: Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1;
for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
proof
let n be Nat;
assume n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A9,A10,A13,ENUMSET1:13,FINSEQ_3:1;
end;
then reconsider L as Convex_Combination of V by A8,A9,A14,CONVEX1:def 3;
A15: for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A7,RLVECT_2:def 8;
take L;
thus thesis by A15;
suppose F = <* v1,v3,v2*>;
then A16: F.1 = v1 & F.2 = v3 & F.3 = v2 by FINSEQ_1:62;
rng f c= REAL
proof
f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A16,FINSEQ_1:62;
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:44
.= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44
.= {1/3} by FINSEQ_1:55;
hence thesis by ZFMISC_1:37;
end;
then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;
A17: f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A16;
f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A16,FINSEQ_1:62;
then A18: Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1;
for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
proof
let n be Nat;
assume n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A9,A10,A17,ENUMSET1:13,FINSEQ_3:1;
end;
then reconsider L as Convex_Combination of V by A8,A9,A18,CONVEX1:def 3;
A19: for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A7,RLVECT_2:def 8;
take L;
thus thesis by A19;
suppose F = <*v2,v1,v3*>;
then A20: F.1 = v2 & F.2 = v1 & F.3 = v3 by FINSEQ_1:62;
rng f c= REAL
proof
f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A20,FINSEQ_1:62;
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:44
.= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44
.= {1/3} by FINSEQ_1:55;
hence thesis by ZFMISC_1:37;
end;
then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;
A21: f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A20;
f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A20,FINSEQ_1:62;
then A22: Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1;
for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
proof
let n be Nat;
assume n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A9,A10,A21,ENUMSET1:13,FINSEQ_3:1;
end;
then reconsider L as Convex_Combination of V by A8,A9,A22,CONVEX1:def 3;
A23: for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A7,RLVECT_2:def 8;
take L;
thus thesis by A23;
suppose F = <* v2,v3,v1*>;
then A24: F.1 = v2 & F.2 = v3 & F.3 = v1 by FINSEQ_1:62;
rng f c= REAL
proof
f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A24,FINSEQ_1:62;
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:44
.= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44
.= {1/3} by FINSEQ_1:55;
hence thesis by ZFMISC_1:37;
end;
then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;
A25: f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A24;
f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A24,FINSEQ_1:62;
then A26: Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1;
for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
proof
let n be Nat;
assume n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A9,A10,A25,ENUMSET1:13,FINSEQ_3:1;
end;
then reconsider L as Convex_Combination of V by A8,A9,A26,CONVEX1:def 3;
A27: for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A7,RLVECT_2:def 8;
take L;
thus thesis by A27;
suppose F = <* v3,v1,v2*>;
then A28: F.1 = v3 & F.2 = v1 & F.3 = v2 by FINSEQ_1:62;
rng f c= REAL
proof
f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A28,FINSEQ_1:62;
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:44
.= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44
.= {1/3} by FINSEQ_1:55;
hence thesis by ZFMISC_1:37;
end;
then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;
A29: f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A28;
f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A28,FINSEQ_1:62;
then A30: Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1;
for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
proof
let n be Nat;
assume n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A9,A10,A29,ENUMSET1:13,FINSEQ_3:1;
end;
then reconsider L as Convex_Combination of V by A8,A9,A30,CONVEX1:def 3;
A31: for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A7,RLVECT_2:def 8;
take L;
thus thesis by A31;
suppose F = <* v3,v2,v1*>;
then A32: F.1 = v3 & F.2 = v2 & F.3 = v1 by FINSEQ_1:62;
rng f c= REAL
proof
f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A32,FINSEQ_1:62;
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:44
.= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44
.= {1/3} by FINSEQ_1:55;
hence thesis by ZFMISC_1:37;
end;
then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;
A33: f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A32;
f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A32,FINSEQ_1:62;
then A34: Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1;
for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
proof
let n be Nat;
assume n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A9,A10,A33,ENUMSET1:13,FINSEQ_3:1;
end;
then reconsider L as Convex_Combination of V by A8,A9,A34,CONVEX1:def 3;
A35: for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A7,RLVECT_2:def 8;
take L;
thus thesis by A35;
end;
hence thesis;
end;
Lm1:
for V being RealLinearSpace, 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;
let M be non empty Subset of V;
assume
A1:{Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)} c= M;
for u,v being VECTOR of V, 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;
let r be Real;
set S = {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)};
assume
A2: 0 < r & r < 1 & u in M & v in M;
consider Lu being Convex_Combination of V such that
A3: Sum(Lu) = u &
(for A being non empty Subset of V st u in A holds
Lu is Convex_Combination of A) by Th1;
reconsider Lu as Convex_Combination of M by A2,A3;
consider Lv being Convex_Combination of V such that
A4: Sum(Lv) = v &
(for A being non empty Subset of V st v in A holds
Lv is Convex_Combination of A) by Th1;
reconsider Lv as Convex_Combination of M by A2,A4;
A5: r*u + (1-r)*v = Sum(r*Lu) + (1-r)*Sum(Lv) by A3,A4,RLVECT_3:2
.= Sum(r*Lu) + Sum((1-r)*Lv) by RLVECT_3:2
.= Sum(r*Lu + (1-r)*Lv) by RLVECT_3:1;
A6: r*Lu + (1-r)*Lv is Convex_Combination of M by A2,CONVEX2:10;
then r*Lu + (1-r)*Lv in ConvexComb(V) by Def1;
then r*u + (1-r)*v in S by A5,A6;
hence thesis by A1;
end;
hence thesis by CONVEX1:def 2;
end;
Lm2:
for V being RealLinearSpace, M being non empty Subset of V,
L being Convex_Combination of M st card Carrier(L) >= 2 holds
ex L1,L2 being Convex_Combination of M, 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;
let M be non empty Subset of V;
let L be Convex_Combination of M;
assume
A1:card Carrier(L) >= 2;
consider F being FinSequence of the carrier of V such that
A2: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))
by CONVEX1:def 3;
consider f being FinSequence of REAL such that
A3: 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 A2;
A4: for n,m being Nat st 1 <= n & n < m & m <= len F holds F.n <> F.m
proof
let n,m be Nat;
assume
A5: 1 <= n & n < m & m <= len F;
assume
A6: F.n = F.m;
n <= len F & 1 <= m by A5,AXIOMS:22;
then n in Seg len F & m in Seg len F by A5,FINSEQ_1:3;
then n in dom F & m in dom F by FINSEQ_1:def 3;
hence contradiction by A2,A5,A6,FUNCT_1:def 8;
end;
then A7:len F >= 2 by A1,A2,GRAPH_5:10;
len F >= 1 + 1 by A1,A2,A4,GRAPH_5:10;
then A8:len F - 1 >= 1 by REAL_1:84;
len F <> 0 by A7;
then consider i being Nat such that
A9:len F = i + 1 by NAT_1:22;
A10:len F - 1 = i by A9,XCMPLX_1:26;
set v = F.len F;
1 <= len F by A7,AXIOMS:22;
then A11:len F in dom F by FINSEQ_3:27;
then A12:F.(len F) in rng F & rng F c= the carrier of V by FINSEQ_1:def 4,
FUNCT_1:12;
then reconsider v as VECTOR of V;
consider L1 being Convex_Combination of V such that
A13:Sum(L1) = v &
(for A being non empty Subset of V st v in A holds
L1 is Convex_Combination of A) by Th1;
A14:v in Carrier L & Carrier L c= M
by A2,A11,FUNCT_1:12,RLVECT_2:def 8;
then reconsider L1 as Convex_Combination of M by A13;
1 <= len f by A3,A7,AXIOMS:22;
then len f in Seg len f by FINSEQ_1:3;
then A15:len f in dom f by FINSEQ_1:def 3;
then f.(len f) in rng f & rng f c= REAL by FINSEQ_1:def 4,FUNCT_1:12;
then reconsider r = f.len f as Real;
A16:0 < r & r < 1
proof
A17: f.(len f) = L.(F.(len f)) & f.(len f) >= 0 by A3,A15;
F.(len F) in rng F by A11,FUNCT_1:12;
then A18: r <> 0 & r >= 0 by A2,A3,A17,RLVECT_2:28;
A19: f = (f|i)^(f/^i) by RFINSEQ:21;
f/^i = <*f/.(len f)*> by A3,A9,FINSEQ_5:33
.= <*f.(len f)*> by A15,FINSEQ_4:def 4;
then Sum(f) = Sum(f|i) + r by A19,RVSUM_1:104;
then A20: Sum(f|i) = 1 - r by A3,XCMPLX_1:26;
Sum(f|i) > 0
proof
A21: for k being Nat st k in dom(f|i) holds 0 <= (f|i).k
proof
let k be Nat;
assume
A22: k in dom(f|i);
f|i = f|Seg i by TOPREAL1:def 1;
then A23: (f|i).k = f.k by A22,FUNCT_1:68;
dom(f|i) c= dom f by FINSEQ_5:20;
hence thesis by A3,A22,A23;
end;
ex k being Nat st k in dom(f|i) & 0 < (f|i).k
proof
A24: 1 in Seg i by A8,A10,FINSEQ_1:3;
1 <= len f by A3,A7,AXIOMS:22;
then A25: 1 in Seg len f by FINSEQ_1:3;
then A26: 1 in dom f by FINSEQ_1:def 3;
then A27: 1 in dom(f|(Seg i)) by A24,RELAT_1:86;
then A28: 1 in dom(f|i) by TOPREAL1:def 1;
f|i = f|Seg i by TOPREAL1:def 1;
then A29: (f|i).1 = f.1 by A27,FUNCT_1:68
.= L.(F.1) by A3,A26;
1 in dom F by A3,A25,FINSEQ_1:def 3;
then F.1 in rng F by FUNCT_1:12;
then A30: L.(F.1) <> 0 by A2,RLVECT_2:28;
(f|i).1 >= 0 by A21,A28;
hence thesis by A28,A29,A30;
end;
hence thesis by A21,RVSUM_1:115;
end;
then 1 > r + 0 by A20,REAL_1:86;
hence thesis by A18;
end;
set r' = 1/(1 - r);
1 > r + 0 by A16;
then A31:1 - r > 0 by REAL_1:86;
then A32:r' > 0 by REAL_2:127;
defpred P[set,set] means
($1 in (rng F \ {v}) implies $2 = r'*(L.$1)) &
(not ($1 in (rng F \ {v})) implies $2 = 0);
A33:for x,y1,y2 being set st
x in the carrier of V & P[x,y1] & P[x,y2]
holds y1 = y2;
A34:for x being set st x in the carrier of V
ex y being set st P[x,y]
proof
let x be set;
assume x in the carrier of V;
x in (rng F \ {v}) or not (x in (rng F \ {v}));
hence thesis;
end;
consider L2 being Function such that
A35:dom L2 = the carrier of V &
for x being set st x in the carrier of V holds P[x,L2.x]
from FuncEx(A33,A34);
for y being set st y in rng L2 holds y in REAL
proof
let y be set;
assume y in rng L2;
then consider x being set such that
A36: x in dom L2 & y = L2.x by FUNCT_1:def 5;
now per cases;
suppose
A37: x in (rng F \ {v});
then x in rng F by XBOOLE_0:def 4;
then reconsider x as VECTOR of V by A2;
y = r'*L.x by A35,A36,A37 .= (r'*L).x by RLVECT_2:def 13;
hence thesis;
suppose not (x in (rng F \ {v}));
then y = 0 by A35,A36;
hence thesis;
end;
hence thesis;
end;
then rng L2 c= REAL by TARSKI:def 3;
then A38:L2 is Element of Funcs(the carrier of V, REAL) by A35,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;
thus thesis by A2,A35;
end;
then reconsider L2 as Linear_Combination of V by A38,RLVECT_2:def 5;
for n,m being Nat st
n in dom (F|i) & m in dom (F|i) & (F|i)/.n = (F|i)/.m holds n = m
proof
let n,m be Nat;
assume that
A39: n in dom(F|i) and
A40: m in dom(F|i) and
A41: (F|i)/.n = (F|i)/.m;
A42: dom(F|i) c= dom F by FINSEQ_5:20;
F/.n = (F|i)/.n by A39,TOPREAL1:1 .= F/.m by A40,A41,TOPREAL1:1;
hence thesis by A2,A39,A40,A42,PARTFUN2:17;
end;
then A43:F|i is one-to-one by PARTFUN2:16;
A44:Carrier(L2) = Carrier(L) \ {v}
proof
for u being set st u in Carrier(L2) holds u in Carrier(L) \ {v}
proof
let u be set;
assume
A45: u in Carrier(L2);
then reconsider u as Element of V;
L2.u <> 0 by A45,RLVECT_2:28;
hence thesis by A2,A35;
end;
then A46: Carrier(L2) c= Carrier(L) \ {v} by TARSKI:def 3;
for u being set st u in Carrier(L) \ {v} holds u in Carrier(L2)
proof
let u be set;
assume
A47: u in Carrier(L) \ {v};
then reconsider u as Element of V;
A48: u in Carrier(L) by A47,XBOOLE_0:def 4;
A49: L2.u = r'*L.u by A2,A35,A47;
L.u <> 0 by A48,RLVECT_2:28;
then L2.u <> 0 by A32,A49,XCMPLX_1:6;
hence thesis by RLVECT_2:28;
end;
then Carrier(L) \ {v} c= Carrier(L2) by TARSKI:def 3;
hence thesis by A46,XBOOLE_0:def 10;
end;
then Carrier(L2) c= Carrier(L) & Carrier(L) c= M
by RLVECT_2:def 8,XBOOLE_1:36;
then Carrier(L2) c= M by XBOOLE_1:1;
then reconsider L2 as Linear_Combination of M by RLVECT_2:def 8;
A50:rng(F|i) = Carrier(L2)
proof
F = (F|i)^(F/^i) by RFINSEQ:21;
then A51: Carrier(L) = rng(F|i) \/ rng(F/^i) by A2,FINSEQ_1:44;
rng(F|i) misses rng(F/^i) by A2,FINSEQ_5:37;
then A52: Carrier(L) \ rng(F/^i) = rng(F|i) by A51,XBOOLE_1:88;
F/^i = <*F/.(len F)*> by A9,FINSEQ_5:33
.= <*F.(len F)*> by A11,FINSEQ_4:def 4;
hence thesis by A44,A52,FINSEQ_1:55;
end;
deffunc F(set) = L2.((F|i).$1);
consider f2 being FinSequence such that
A53:len f2 = len(F|i) &
for k being Nat st k in Seg len(F|i) holds f2.k = F(k) from SeqLambda;
for y being set st y in rng f2 holds y in REAL
proof
let y be set;
assume y in rng f2;
then consider x being set such that
A54: x in dom f2 & y = f2.x by FUNCT_1:def 5;
A55: x in Seg len f2 by A54,FINSEQ_1:def 3;
then reconsider x as Nat;
x in dom (F|i) by A53,A55,FINSEQ_1:def 3;
then A56: (F|i).x in rng (F|i) by FUNCT_1:12;
consider L2' being Function such that
A57: L2 = L2' & dom L2' = the carrier of V & rng L2' c= REAL by FUNCT_2:def 2;
L2.((F|i).x) in rng L2 by A50,A56,A57,FUNCT_1:12;
then L2.((F|i).x) in REAL by A57;
hence thesis by A53,A54,A55;
end;
then rng f2 c= REAL by TARSKI:def 3;
then reconsider f2 as FinSequence of REAL by FINSEQ_1:def 4;
Sum(f2) = 1 &
(for n being Nat st n in dom(f2) holds f2.n = L2.((F|i).n) & f2.n >= 0)
proof
A58: i <= len F by A9,NAT_1:37;
A59: dom f2 = Seg len (F|i) by A53,FINSEQ_1:def 3;
then A60: dom f2 = Seg i by A58,TOPREAL1:3
.= Seg len (f|i) by A3,A58,TOPREAL1:3
.= dom (f|i) by FINSEQ_1:def 3;
then A61: dom f2 = dom (r'*(f|i)) by RVSUM_1:65;
A62: for k being Nat st k in dom f2 holds f2.k = (r'*(f|i)).k & f2.k >= 0
proof
let k be Nat;
assume
A63: k in dom f2;
then A64: f2.k = L2.((F|i).k) by A53,A59;
k in dom (f|Seg i) & f|i = f|(Seg i) by A60,A63,TOPREAL1:def 1;
then A65: k in dom f /\ Seg i & (f|i).k = f.k
by FUNCT_1:68;
then A66: k in dom f by XBOOLE_0:def 3;
then A67: (f|i).k = L.(F.k) by A3,A65;
A68: k in dom (F|i) by A59,A63,FINSEQ_1:def 3;
A69: F|i = F|Seg i by TOPREAL1:def 1;
then A70: (F|i).k = F.k by A68,FUNCT_1:68;
A71: (f|i).k = L.((F|i).k) by A67,A68,A69,FUNCT_1:68;
(F|i).k in rng(F|i) by A68,FUNCT_1:12;
then reconsider w = (F|i).k as Element of V by A50;
A72: not w in {v}
proof
assume w in {v};
then A73: F.k = v by A70,TARSKI:def 1;
dom (F|Seg i) c= dom F by FUNCT_1:76;
then A74: k = len F by A2,A11,A68,A69,A73,FUNCT_1:def 8;
k <= len(F|i) & len(F|i) <= i by A59,A63,FINSEQ_1:3,FINSEQ_5:19;
then k <= i by AXIOMS:22;
then k + 1 <= len F by A10,REAL_1:84;
hence contradiction by A74,NAT_1:38;
end;
now per cases;
suppose w in (rng F \ {v});
then A75: L2.w = r'*(L.w) by A35
.= r'*(f|i).k by A67,A68,A69,FUNCT_1:68
.= (r'*(f|i)).k by RVSUM_1:66;
f.k >= 0 by A3,A66;
then r'*(f|i).k >= 0 by A32,A65,SQUARE_1:19;
hence thesis by A64,A75,RVSUM_1:66;
suppose
A76: not w in (rng F \ {v});
then A77: not w in rng F by A72,XBOOLE_0:def 4;
A78: f2.k = 0 by A35,A64,A76;
L.w = 0 by A2,A77,RLVECT_2:28;
then r'*(f|i).k = 0 by A71;
hence thesis by A78,RVSUM_1:66;
end;
hence thesis;
end;
then for k being Nat st k in dom f2 holds f2.k = (r'*(f|i)).k;
then A79: f2 = r'*(f|i) by A61,FINSEQ_1:17;
A80: f = (f|i)^(f/^i) by RFINSEQ:21;
f/^i = <*f/.(len f)*> by A3,A9,FINSEQ_5:33
.= <*f.(len f)*> by A15,FINSEQ_4:def 4;
then Sum(f) = Sum(f|i) + r by A80,RVSUM_1:104;
then Sum(f|i) = 1 - r by A3,XCMPLX_1:26;
hence Sum(f2) = 1/(1-r)*(1-r) by A79,RVSUM_1:117
.= 1/((1-r)/(1-r)) by XCMPLX_1:82
.= 1/1 by A31,XCMPLX_1:60
.= 1;
thus thesis by A53,A59,A62;
end;
then reconsider L2 as Convex_Combination of M by A43,A50,A53,CONVEX1:def 3;
A81:v in {v} by TARSKI:def 1;
reconsider B = {v} as non empty Subset of V by TARSKI:def 1;
L1 is Convex_Combination of B by A13,A81;
then A82:Carrier L1 c= {v} by RLVECT_2:def 8;
then A83:Carrier L1 = {} or Carrier L1 = {v} by ZFMISC_1:39;
A84:for u being Element of V holds L.u = (r*L1 + (1-r)*L2).u
proof
let u be Element of V;
A85: (r*L1 +(1-r)*L2).u = (r*L1).u +((1-r)*L2).u by RLVECT_2:def 12;
now per cases;
suppose
A86: u in Carrier L;
now per cases;
suppose A87:u = v;
then L1.u = 1 by A83,CONVEX1:21,27;
then A88: r*L1.u = r;
u in {v} by A87,TARSKI:def 1;
then not u in Carrier L2 by A44,XBOOLE_0:def 4;
then L2.u = 0 by RLVECT_2:28;
then (1-r)*L2.u = 0;
then A89: ((1-r)*L2).u = 0 by RLVECT_2:def 13;
L.u = r + 0 by A3,A15,A87;
hence thesis by A85,A88,A89,RLVECT_2:def 13;
suppose u <> v;
then A90: not u in Carrier L1 by A82,TARSKI:def 1;
then L1.u = 0 by RLVECT_2:28;
then r*L1.u = 0;
then A91: (r*L1).u = 0 by RLVECT_2:def 13;
u in Carrier L2 by A44,A83,A86,A90,CONVEX1:21,XBOOLE_0:def 4;
then L2.u = r'*(L.u) by A2,A35,A44;
then (1-r)*L2.u = ((1-r)*r')*L.u by XCMPLX_1:4
.= 1/((1-r)/(1-r))*L.u by XCMPLX_1:82
.= 1*L.u by A31,XCMPLX_1:51
.= L.u;
hence thesis by A85,A91,RLVECT_2:def 13;
end;
hence thesis;
suppose A92:not u in Carrier L;
then A93: L.u = 0 + 0 by RLVECT_2:28;
not u in Carrier L1 by A2,A12,A82,A92,TARSKI:def 1;
then L1.u = 0 by RLVECT_2:28;
then r*L1.u = 0;
then A94: (r*L1).u = 0 by RLVECT_2:def 13;
not u in Carrier L2 by A44,A92,XBOOLE_0:def 4;
then L2.u = 0 by RLVECT_2:28;
then (1-r)*L2.u = 0;
hence thesis by A85,A93,A94,RLVECT_2:def 13;
end;
hence thesis;
end;
take L1,L2,r;
{v} c= Carrier L by A14,ZFMISC_1:37;
then card Carrier L2 = card Carrier L - card {v} by A44,CARD_2:63;
hence thesis by A16,A83,A84,CARD_1:79,CONVEX1:21,RLVECT_2:def 11;
end;
Lm3:
for V being RealLinearSpace, 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;
let M be non empty Subset of V;
assume
A1:M is convex;
set S = {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)};
for v being set st v in S holds v in M
proof
let v being set;
assume v in S;
then consider L being Convex_Combination of M such that
A2: v = Sum(L) & L in ConvexComb(V);
reconsider v as VECTOR of V by A2;
now per cases;
suppose card Carrier(L) < 2;
then card Carrier(L) < 1 + 1;
then A3: card Carrier(L) <= 1 by NAT_1:38;
card Carrier(L) <> 0
proof
assume card Carrier(L) = 0;
then Carrier(L) = {} by CARD_2:59;
hence contradiction by CONVEX1:21;
end;
then card Carrier(L) > 0 by NAT_1:19;
then card Carrier(L) >= 0 + 1 by NAT_1:38;
then card Carrier(L) = 1 by A3,AXIOMS:21;
then consider x being set such that
A4: Carrier(L) = {x} by CARD_2:60;
x in Carrier(L) by A4,TARSKI:def 1;
then reconsider x as VECTOR of V;
A5: v = L.x*x by A2,A4,RLVECT_2:53
.= 1*x by A4,CONVEX1:27
.= x by RLVECT_1:def 9;
{x} c= M by A4,RLVECT_2:def 8;
hence thesis by A5,ZFMISC_1:37;
suppose
A6: card Carrier(L) >= 2;
defpred P[Nat] means
for LL being Convex_Combination of M st card Carrier LL = 1 + $1 &
(ex L1,L2 being Convex_Combination of M, 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;
A7: P[1]
proof
let LL be Convex_Combination of M;
assume that
A8: card Carrier LL = 1 + 1 and
A9: ex L1,L2 being Convex_Combination of M, 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;
consider L1,L2 be Convex_Combination of M, r be Real such that
A10: 0 < r & r < 1 & LL = r*L1 + (1-r)*L2 &
card Carrier(L1) = 1 & card Carrier(L2) = card Carrier(LL) - 1 by A9;
consider x1 being set such that
A11: Carrier(L1) = {x1} by A10,CARD_2:60;
x1 in Carrier(L1) by A11,TARSKI:def 1;
then reconsider x1 as VECTOR of V;
Sum L1 = L1.x1 * x1 & L1.x1 = 1 by A11,CONVEX1:27,RLVECT_2:53;
then A12: Sum L1 = x1 by RLVECT_1:def 9;
A13: {x1} c= M by A11,RLVECT_2:def 8;
consider x2 being set such that
A14: Carrier(L2) = {x2} by A8,A10,CARD_2:60;
x2 in Carrier(L2) by A14,TARSKI:def 1;
then reconsider x2 as VECTOR of V;
Sum L2 = L2.x2 * x2 & L2.x2 = 1 by A14,CONVEX1:27,RLVECT_2:53;
then A15: Sum L2 = x2 by RLVECT_1:def 9;
{x2} c= M by A14,RLVECT_2:def 8;
then A16: Sum L1 in M & Sum L2 in M by A12,A13,A15,ZFMISC_1:37;
Sum LL = Sum(r*L1) + Sum((1-r)*L2) by A10,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,A10,A16,CONVEX1:def 2;
end;
A17: for k being non empty Nat st P[k] holds P[k+1]
proof
let k being non empty Nat;
assume
A18: P[k];
let LL be Convex_Combination of M;
assume that
A19: card Carrier LL = 1 + (k+1) and
A20: ex L1,L2 being Convex_Combination of M, 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;
consider L1,L2 be Convex_Combination of M, r be Real such that
A21: 0 < r & r < 1 & LL = r*L1 + (1-r)*L2 &
card Carrier(L1) = 1 & card Carrier(L2) = card Carrier(LL) - 1 by A20;
consider x1 being set such that
A22: Carrier(L1) = {x1} by A21,CARD_2:60;
x1 in Carrier(L1) by A22,TARSKI:def 1;
then reconsider x1 as VECTOR of V;
Sum L1 = L1.x1 * x1 & L1.x1 = 1 by A22,CONVEX1:27,RLVECT_2:53;
then A23: Sum L1 = x1 by RLVECT_1:def 9;
{x1} c= M by A22,RLVECT_2:def 8;
then A24: Sum L1 in M by A23,ZFMISC_1:37;
A25: card Carrier(L2) = (k+1) + (1-1) by A19,A21,XCMPLX_1:29
.= k + 1;
k > 0 by NAT_1:19;
then k >= 0 + 1 by NAT_1:38;
then k + 1 >= 1 + 1 by AXIOMS:24;
then consider LL1,LL2 be Convex_Combination of M, rr be Real such that
A26: 0 < rr & rr < 1 & L2 = rr*LL1 + (1-rr)*LL2 & card Carrier(LL1) = 1 &
card Carrier(LL2) = card Carrier(L2) - 1 by A25,Lm2;
A27: Sum L2 in M by A18,A25,A26;
Sum LL = Sum(r*L1) + Sum((1-r)*L2) by A21,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,A21,A24,A27,CONVEX1:def 2;
end;
A28: for k being non empty Nat holds P[k] from Ind_from_1(A7,A17);
card Carrier(L) <> 0 by A6;
then ex k being Nat st card Carrier L = k + 1 by NAT_1:22;
then consider k being Nat such that
A29: card Carrier L = 1 + k;
k <> 0 by A6,A29;
then reconsider k as non empty Nat;
A30: card Carrier L = 1 + k by A29;
ex L1,L2 being Convex_Combination of M, 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 A6,Lm2;
hence thesis by A2,A28,A30;
end;
hence thesis;
end;
hence thesis by TARSKI:def 3;
end;
theorem
for V being RealLinearSpace, 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
for V being RealLinearSpace, 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;
let M be non empty Subset of V;
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;
assume
x in {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)};
then consider L being Convex_Combination of M such that
A1: x = Sum(L) & L in ConvexComb(V);
M c= conv(M) by CONVEX2:8;
hence thesis by A1,CONVEX2:6;
end;
then A2:{Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)} c=
conv(M)
by TARSKI:def 3;
consider m being set such that
A3:m in M by XBOOLE_0:def 1;
reconsider m as VECTOR of V by A3;
consider LL being Convex_Combination of V such that
A4:Sum LL = m &
for A being non empty Subset of V st m in A holds
LL is Convex_Combination of A by Th1;
reconsider LL as Convex_Combination of M by A3,A4;
LL in ConvexComb(V) by Def1;
then m in {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)}
by A4;
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;
assume x in N;
then consider L being Convex_Combination of M such that
A5: x = Sum L & L in ConvexComb(V);
thus thesis by A5;
end;
then N c= the carrier of V by TARSKI:def 3;
then reconsider N as Subset of V;
for u,v being VECTOR of V,
r be 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;
let r be Real;
assume
A6: 0 < r & r < 1 & u in N & v in N;
then consider Lu being Convex_Combination of M such that
A7: u = Sum Lu & Lu in ConvexComb(V);
consider Lv being Convex_Combination of M such that
A8: v = Sum Lv & Lv in ConvexComb(V) by A6;
r*Lu + (1-r)*Lv is Convex_Combination of V by A6,CONVEX2:9;
then A9: r*Lu + (1-r)*Lv in ConvexComb(V) by Def1;
reconsider LL = r*Lu + (1-r)*Lv as Convex_Combination of M
by A6,CONVEX2:10;
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 A7,A8,A9;
end;
then A10:N is convex by CONVEX1:def 2;
for v being set st v in M holds v in N
proof
let v be set;
assume
A11: v in M;
then reconsider v as VECTOR of V;
consider LL being Convex_Combination of V such that
A12: Sum LL = v &
for A being non empty Subset of V st v in A holds
LL is Convex_Combination of A by Th1;
reconsider LL as Convex_Combination of M by A11,A12;
LL in ConvexComb(V) by Def1;
hence thesis by A12;
end;
then M c= N by TARSKI:def 3;
then conv(M) c= N by A10,CONVEX1:30;
hence thesis by A2,XBOOLE_0:def 10;
end;
begin :: Cone and Convex Cone
definition let V be non empty RLSStruct, M be Subset of V;
attr M is cone means :Def3:
for r being Real, v being VECTOR of V st r > 0 & v in M holds
r*v in M;
end;
theorem Th6:
for V being non empty RLSStruct, M being Subset of V st
M = {} holds M is cone
proof
let V be non empty RLSStruct;
let M be Subset of V;
assume
A1:M = {};
for r being Real, v being VECTOR of V st r > 0 & v in {} holds
r*v in {};
hence thesis by A1,Def3;
end;
definition let V be non empty RLSStruct;
cluster cone Subset of V;
existence
proof
consider M being empty Subset of V;
M is cone by Th6;
hence thesis;
end;
end;
definition let V be non empty RLSStruct;
cluster empty cone Subset of V;
existence
proof
set M = {};
M c= the carrier of V by XBOOLE_1:2;
then reconsider M as Subset of V;
reconsider M as cone Subset of V by Th6;
take M;
thus thesis;
end;
end;
definition let V be RealLinearSpace;
cluster non empty cone Subset of V;
existence
proof
set M = {0.V};
reconsider M as Subset of V;
for r being Real, v being VECTOR of V st r > 0 & v in M holds
r*v in M
proof
let r be Real;
let v be VECTOR of V;
assume r > 0 & v in M;
then v = 0.V by TARSKI:def 1;
then r*v = 0.V by RLVECT_1:23;
hence thesis by TARSKI:def 1;
end;
then reconsider M as cone Subset of V by Def3;
take M;
thus thesis by TARSKI:def 1;
end;
end;
theorem Th7:
for V being non empty RLSStruct, M being cone Subset of V st
V is RealLinearSpace-like 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;
let M be cone Subset of V;
assume
A1:V is RealLinearSpace-like;
A2: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
A3: M is convex;
for u,v being VECTOR of V st u in M & v in M holds u + v in M
proof
let u,v being VECTOR of V;
assume
u in M & v in M;
then (1/2)*u + (1-(1/2))*v in M by A3,CONVEX1:def 2;
then A4: 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 A1,RLVECT_1:def 9
.= (2*(1/2))*u + 2*((1/2)*v) by A1,RLVECT_1:def 9
.= 1*u + (2*(1/2))*v by A1,RLVECT_1:def 9
.= u + 1*v by A1,RLVECT_1:def 9;
hence thesis by A1,A4,RLVECT_1:def 9;
end;
hence thesis;
end;
(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
A5: 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,
r be 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;
let r be Real;
assume that
A6: 0 < r & r < 1 and
A7: u in M & v in M;
r + 0 < 1 by A6;
then 1 - r > 0 by REAL_1:86;
then r*u in M & (1-r)*v in M by A6,A7,Def3;
hence thesis by A5;
end;
hence thesis by CONVEX1:def 2;
end;
hence thesis by A2;
end;
Lm4:
for V being RealLinearSpace, M being Subset of V,
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;
let M be Subset of V;
let L be Linear_Combination of M;
assume
card Carrier(L) >= 1;
then card Carrier L <> 0;
then Carrier L <> {} by CARD_4:17;
then consider u being set such that
A1:u in Carrier L by XBOOLE_0:def 1;
reconsider u as VECTOR of V by A1;
consider L1 be Linear_Combination of {u} such that
A2:L1.u = L.u from LinCEx1;
Carrier L c= M by RLVECT_2:def 8;
then A3:{u} c= M by A1,ZFMISC_1:37;
A4:Carrier L1 c= {u} by RLVECT_2:def 8;
then Carrier L1 c= M by A3,XBOOLE_1:1;
then reconsider L1 as Linear_Combination of M by RLVECT_2:def 8;
A5:for v being VECTOR of V st v in Carrier L1 holds L1.v = L.v
proof
let v be VECTOR of V;
assume v in Carrier L1;
then v = u by A4,TARSKI:def 1;
hence thesis by A2;
end;
defpred P[set,set] means
($1 in (Carrier L \ {u}) implies $2 = L.$1) &
(not ($1 in (Carrier L \ {u})) implies $2 = 0);
A6:for x,y1,y2 being set st
x in the carrier of V & P[x,y1] & P[x,y2]
holds y1 = y2;
A7:for x being set st x in the carrier of V
ex y being set st P[x,y]
proof
let x be set;
assume x in the carrier of V;
x in (Carrier L \ {u}) or not (x in (Carrier L \ {u}));
hence thesis;
end;
consider L2 being Function such that
A8:dom L2 = the carrier of V &
for x being set st x in the carrier of V holds P[x,L2.x]
from FuncEx(A6,A7);
for y being set st y in rng L2 holds y in REAL
proof
let y be set;
assume y in rng L2;
then consider x being set such that
A9: x in dom L2 & y = L2.x by FUNCT_1:def 5;
now per cases;
suppose
A10: x in (Carrier L \ {u});
then reconsider x as VECTOR of V;
y = L.x by A8,A9,A10;
hence thesis;
suppose not (x in (Carrier L \ {u}));
then y = 0 by A8,A9;
hence thesis;
end;
hence thesis;
end;
then rng L2 c= REAL by TARSKI:def 3;
then A11:L2 is Element of Funcs(the carrier of V, REAL) by A8,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 as finite Subset of V;
take T;
thus thesis by A8;
end;
then reconsider L2 as Linear_Combination of V by A11,RLVECT_2:def 5;
for x being set st x in Carrier L2 holds x in M
proof
let x be set;
assume
A12: x in Carrier L2;
then reconsider x as VECTOR of V;
L2.x <> 0 by A12,RLVECT_2:28;
then x in Carrier L \ {u} by A8;
then A13: x in Carrier L by XBOOLE_0:def 4;
Carrier L c= M by RLVECT_2:def 8;
hence thesis by A13;
end;
then Carrier L2 c= M by TARSKI:def 3;
then reconsider L2 as Linear_Combination of M by RLVECT_2:def 8;
Carrier L1 <> {}
proof
assume
Carrier L1 = {};
then L.u = 0 by A2,RLVECT_2:28;
hence contradiction by A1,RLVECT_2:28;
end;
then A14:Carrier L1 = {u} by A4,ZFMISC_1:39;
for x being set st x in Carrier L2 holds x in Carrier L \ {u}
proof
let x be set;
assume
A15: x in Carrier L2;
then reconsider x as VECTOR of V;
L2.x <> 0 by A15,RLVECT_2:28;
hence thesis by A8;
end;
then A16:Carrier L2 c= Carrier L \ {u} by TARSKI:def 3;
for x being set st x in Carrier L \ {u} holds x in Carrier L2
proof
let x be set;
assume
A17: x in Carrier L \ {u};
then reconsider x as VECTOR of V;
A18: L2.x = L.x by A8,A17;
x in Carrier L by A17,XBOOLE_0:def 4;
then L.x <> 0 by RLVECT_2:28;
hence thesis by A18,RLVECT_2:28;
end;
then Carrier L \ {u} c= Carrier L2 by TARSKI:def 3;
then A19:Carrier L2 = Carrier L \ {u} by A16,XBOOLE_0:def 10;
for v being VECTOR of V holds L.v = (L1 + L2).v
proof
let v be VECTOR of V;
now per cases;
suppose
A20: v in Carrier L;
now per cases;
suppose
A21: v = u;
then A22: not v in Carrier L2 by A16,ZFMISC_1:64;
(L1 + L2).v = L1.v + L2.v by RLVECT_2:def 12
.= L.v + 0 by A2,A21,A22,RLVECT_2:28;
hence thesis;
suppose
A23: v <> u;
then not v in Carrier L1 by A4,TARSKI:def 1;
then A24: L1.v = 0 by RLVECT_2:28;
A25: v in Carrier L \ {u} by A20,A23,ZFMISC_1:64;
(L1 + L2).v = L1.v + L2.v by RLVECT_2:def 12
.= 0 + L.v by A8,A24,A25;
hence thesis;
end;
hence thesis;
suppose
A26: not v in Carrier L;
then A27: not v in Carrier L1 by A1,A4,TARSKI:def 1;
not v in Carrier L2 by A16,A26,ZFMISC_1:64;
then A28: L2.v = 0 by RLVECT_2:28;
(L1 + L2).v = L1.v + L2.v by RLVECT_2:def 12
.= 0 by A27,A28,RLVECT_2:28;
hence thesis by A26,RLVECT_2:28;
end;
hence thesis;
end;
then A29:L = L1 + L2 by RLVECT_2:def 11;
Carrier L1 c= Carrier L by A1,A14,ZFMISC_1:37;
then A30:card Carrier L2 = card Carrier L - card Carrier L1
by A14,A19,CARD_2:63
.= card Carrier L - 1 by A14,CARD_1:79;
take L1,L2;
Carrier L \ {u} c= Carrier L by XBOOLE_1:36;
hence thesis by A1,A5,A8,A14,A16,A29,A30,CARD_1:79,RLVECT_3:1,XBOOLE_1:1,
ZFMISC_1:37;
end;
theorem
for V being RealLinearSpace, 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;
let M be Subset of V;
A1: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
assume
A2: M is convex & M is cone;
let L be Linear_Combination of M;
assume
A3: Carrier L <> {} &
for v being VECTOR of V st v in Carrier L holds L.v > 0;
defpred P[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;
A4: P[1]
proof
let LL be Linear_Combination of M;
assume that
A5: card Carrier LL = 1 and
A6: 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);
consider x being set such that
A7: Carrier LL = {x} by A5,CARD_2:60;
{x} c= M by A7,RLVECT_2:def 8;
then A8: x in M by ZFMISC_1:37;
then reconsider x as VECTOR of V;
A9: Sum LL = LL.x * x by A7,RLVECT_2:53;
x in Carrier LL by A7,TARSKI:def 1;
then LL.x > 0 by A6;
hence thesis by A2,A8,A9,Def3;
end;
A10: for k being non empty Nat st P[k] holds P[k+1]
proof
let k be non empty Nat;
assume
A11: P[k];
let LL be Linear_Combination of M;
assume that
A12: card Carrier LL = k + 1 and
A13: for u being VECTOR of V st u in Carrier LL holds LL.u > 0 and
A14: 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);
consider L1,L2 be Linear_Combination of M such that
A15: 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) by A14;
A16: card Carrier L2 = k by A12,A15,XCMPLX_1:26;
then card Carrier L2 > 0 by NAT_1:19;
then card Carrier L2 >= 0 + 1 by NAT_1:38;
then A17: 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;
for u being VECTOR of V st u in Carrier L2 holds L2.u > 0
proof
let u be VECTOR of V;
assume u in Carrier L2;
then u in Carrier LL & L2.u = LL.u by A15;
hence thesis by A13;
end;
then A18: Sum L2 in M by A11,A16,A17;
A19: 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 A15,Lm4;
for u being VECTOR of V st u in Carrier L1 holds L1.u > 0
proof
let u be VECTOR of V;
assume u in Carrier L1;
then u in Carrier LL & L1.u = LL.u by A15;
hence thesis by A13;
end;
then Sum L1 in M by A4,A15,A19;
hence thesis by A2,A15,A18,Th7;
end;
A20: for k being non empty Nat holds P[k] from Ind_from_1(A4,A10);
A21: card Carrier L <> 0 by A3,CARD_2:59;
then card Carrier L > 0 by NAT_1:19;
then card Carrier L >= 0 + 1 by NAT_1:38;
then A22: 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;
consider k being non empty Nat such that
A23: card Carrier L = k by A21;
thus thesis by A3,A20,A22,A23;
end;
(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
A24: (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);
A25: for r being Real, v being VECTOR of V st r > 0 & v in M holds r*v in M
proof
let r be Real;
let v be VECTOR of V;
assume
A26: r > 0 & v in M;
consider L being Linear_Combination of {v} such that
A27: L.v = r from LinCEx1;
A28: v in Carrier L by A26,A27,RLVECT_2:28;
A29: for u being VECTOR of V st u in Carrier L holds L.u > 0
proof
let u be VECTOR of V;
assume
A30: u in Carrier L;
Carrier L c= {v} by RLVECT_2:def 8;
hence thesis by A26,A27,A30,TARSKI:def 1;
end;
{v} c= M by A26,ZFMISC_1:37;
then reconsider L as Linear_Combination of M by RLVECT_2:33;
Sum L in M by A24,A28,A29;
hence thesis by A27,RLVECT_2:50;
end;
then A31: M is cone by Def3;
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;
assume
A32: u in M & v in M;
now per cases;
suppose
A33: u <> v;
consider L being Linear_Combination of {u,v} such that
A34: L.u = 1 & L.v = 1 from LinCEx2(A33);
A35: Carrier L <> {} by A34,RLVECT_2:28;
A36: for v1 being VECTOR of V st v1 in Carrier L holds L.v1 > 0
proof
let v1 be VECTOR of V;
assume
A37: v1 in Carrier L;
A38: Carrier L c= {u,v} by RLVECT_2:def 8;
now per cases by A37,A38,TARSKI:def 2;
suppose v1 = u;
hence thesis by A34;
suppose v1 = v;
hence thesis by A34;
end;
hence thesis;
end;
A39: Sum L = 1 * u + 1 * v by A33,A34,RLVECT_2:51
.= u + 1 * v by RLVECT_1:def 9
.= u + v by RLVECT_1:def 9;
{u,v} c= M by A32,ZFMISC_1:38;
then reconsider L as Linear_Combination of M by RLVECT_2:33;
Sum L in M by A24,A35,A36;
hence thesis by A39;
suppose
A40: u = v;
(1+1)*u in M by A25,A32;
then 1*u + 1*u in M by RLVECT_1:def 9;
then u + 1*u in M by RLVECT_1:def 9;
hence thesis by A40,RLVECT_1:def 9;
end;
hence thesis;
end;
hence thesis by A31,Th7;
end;
hence thesis by A1;
end;
theorem
for V being non empty RLSStruct, 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;
let M,N be Subset of V;
assume that
A1:M is cone and
A2:N is cone;
let r be Real;
let v be VECTOR of V;
assume
A3:r > 0 & v in M /\ N;
then A4:v in M & v in N by XBOOLE_0:def 3;
then A5:r*v in M by A1,A3,Def3;
r*v in N by A2,A3,A4,Def3;
hence thesis by A5,XBOOLE_0:def 3;
end;