:: Convex Hull, Set of Convex Combinations and Convex Cone
:: by Noboru Endou and Yasunari Shidama
::
:: Received June 16, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, RLVECT_1, CONVEX2, FUNCT_2, STRUCT_0, XBOOLE_0,
SUBSET_1, CARD_3, RLVECT_2, FUNCT_1, FINSEQ_1, RELAT_1, VALUED_1, TARSKI,
NAT_1, XXREAL_0, CARD_1, ARYTM_3, ORDINAL4, CONVEX1, REAL_1, ARYTM_1,
RFINSEQ, PARTFUN1, FINSET_1, SUPINF_2, CONVEX3, FUNCT_7, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, XCMPLX_0, XREAL_0, XXREAL_0,
REAL_1, RELAT_1, FUNCT_1, FINSET_1, ORDINAL1, DOMAIN_1, PARTFUN1,
NUMBERS, STRUCT_0, ALGSTR_0, FUNCT_2, FINSEQ_1, RLVECT_1, RLVECT_2,
RVSUM_1, CONVEX1, RFINSEQ, CONVEX2;
constructors DOMAIN_1, REAL_1, FINSOP_1, RVSUM_1, RFINSEQ, CONVEX1, BINOP_2,
RELSET_1, NUMBERS;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XXREAL_0,
XREAL_0, NAT_1, STRUCT_0, RLVECT_1, VALUED_0, CARD_1, RLVECT_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities RVSUM_1;
expansions TARSKI;
theorems RLVECT_1, RVSUM_1, FUNCT_1, FINSEQ_1, TARSKI, ZFMISC_1, XBOOLE_0,
XBOOLE_1, RLVECT_2, CARD_1, FINSEQ_3, FINSEQ_4, ENUMSET1, CONVEX1,
FUNCT_2, NAT_1, RFINSEQ, CONVEX2, RLVECT_3, CARD_2, FINSEQ_5, PARTFUN2,
GRAPH_5, RELAT_1, XCMPLX_1, XREAL_1, XXREAL_0, FINSOP_1, ORDINAL1,
PARTFUN1, VALUED_1, RLVECT_4, XREAL_0;
schemes NAT_1, XBOOLE_0, FINSEQ_1, CLASSES1;
begin :: Equality of Convex Hull and Set of Convex Combinations
definition
let V be RealLinearSpace;
defpred P[object] means $1 is Convex_Combination of V;
func ConvexComb(V) -> set means
:Def1:
for L being object holds L in it iff L is Convex_Combination of V;
existence
proof
consider A being set such that
A1: for x being object holds x in A iff x in Funcs(the carrier of V, REAL
) & P[x] from XBOOLE_0:sch 1;
take A;
let L be object;
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 object holds x in X1 iff P[x]) & (
for x being object holds x in X2 iff P[x]) holds X1 = X2
from XBOOLE_0:sch 3;
end;
end;
definition
let V be RealLinearSpace, M be non empty Subset of V;
defpred P[object] means $1 is Convex_Combination of M;
func ConvexComb(M) -> set means
for L being object holds L in it iff L is Convex_Combination of M;
existence
proof
consider A being set such that
A1: for x being object holds x in A iff x in Funcs(the carrier of V, REAL
) & P[x] from XBOOLE_0:sch 1;
take A;
let L be object;
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 object holds x in X1 iff P[x]) & (
for x being object holds x in X2 iff P[x]) holds X1 = X2
from XBOOLE_0:sch 3;
end;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
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 = jj 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 F(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 = F(n) from
FINSEQ_1:sch 2;
A6: 1 in REAL by XREAL_0:def 1;
A7: len F = 1 by A3,A2,FINSEQ_3:96;
then 1 in dom f by A5,FINSEQ_3:25;
then
A8: f.1 = L.(F.1) by A5;
then f = <*1*> by A1,A5,A7,A4,FINSEQ_1:40;
then rng f = {1} by FINSEQ_1:38;
then rng f c= REAL by ZFMISC_1:31,A6;
then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;
A9: for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
proof
let n be Nat;
assume
A10: n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A1,A5,A7,A8,A4,A10,FINSEQ_1:2,TARSKI:def 1;
end;
f = <*1*> by A1,A5,A7,A8,A4,FINSEQ_1:40;
then Sum(f) = jj by FINSOP_1:11;
then reconsider L as Convex_Combination of V by A2,A5,A9,CONVEX1:def 3;
A11: for A being non empty Subset of V st v in A holds L is
Convex_Combination of A by A3,RLVECT_2:def 6,ZFMISC_1:31;
take L;
Sum(L) = 1 * v by A1,A3,RLVECT_2:35;
hence thesis by A11,RLVECT_1:def 8;
end;
reconsider jd=1/2, jt=1/3 as Element of REAL by XREAL_0:def 1;
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 = jj/2 & L.v2 = jj/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 F(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 = F(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
per cases by A1,A5,A3,FINSEQ_3:99;
suppose
F = <*v1,v2*>;
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 = <*jd*>^<*jd*> by FINSEQ_1:def 9;
then rng f = rng <*1/2*> \/ rng <*jd*> by FINSEQ_1:31
.= {jd} by FINSEQ_1:38;
then reconsider 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;
assume
A11: n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A2,A4,A6,A8,A7,A9,A11,FINSEQ_1:2,TARSKI:def 2;
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 as Convex_Combination of V by A3,A4,A10,CONVEX1:def 3;
take L;
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 thesis;
end;
suppose
F = <*v2,v1*>;
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 = <*jd*>^<*jd*> by FINSEQ_1:def 9;
then rng f = rng <*1/2*> \/ rng <*jd*> by FINSEQ_1:31
.= {jd} by FINSEQ_1:38;
then reconsider 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;
assume
A14: n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A2,A4,A6,A8,A7,A12,A14,FINSEQ_1:2,TARSKI:def 2;
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 as Convex_Combination of V by A3,A4,A13,CONVEX1:def 3;
take L;
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 thesis;
end;
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 = jj/3 & L.v2 = jj/3 & L.v3 = jj/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 F(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 = F(n) from
FINSEQ_1:sch 2;
for x being object st x in {v1,v2,v3} holds x in Carrier(L)
proof
let x be object;
assume
A7: x in {v1,v2,v3};
then reconsider x as VECTOR of V;
x = v1 or x = v2 or x = v3 by A7,ENUMSET1:def 1;
hence thesis by A4,RLVECT_2:19;
end;
then Carrier(L) c= {v1,v2,v3} & {v1,v2,v3} c= Carrier(L) by RLVECT_2:def 6;
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
per cases by A1,A2,A3,A8,A5,CONVEX1:31;
suppose
A13: F = <*v1,v2,v3*>;
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 = <*jt*>^<*jt*>^<*jt*> by FINSEQ_1:def 10;
then rng f = rng (<*jt*>^<*jt*>) \/ rng <*1/3*> by FINSEQ_1:31
.= rng <*1/3*> \/ rng <*jt*> \/ rng <*jt*> by FINSEQ_1:31
.= {jt} by FINSEQ_1:38;
then reconsider 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;
assume
A17: n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A4,A6,A9,A12,A10,A11,A15,A14,A17,ENUMSET1:def 1
,FINSEQ_3:1;
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 as Convex_Combination of V by A5,A6,A16,CONVEX1:def 3;
take L;
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 thesis;
end;
suppose
A18: F = <* v1,v3,v2*>;
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 = <*jt*>^<*jt*>^<*jt*> by FINSEQ_1:def 10;
then rng f = rng (<*jt*>^<*jt*>) \/ rng <*jt*> by FINSEQ_1:31
.= rng <*jt*> \/ rng <*jt*> \/ rng <*jt*> by FINSEQ_1:31
.= {jt} by FINSEQ_1:38;
then reconsider 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;
assume
A22: n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A4,A6,A9,A12,A10,A11,A20,A19,A22,ENUMSET1:def 1
,FINSEQ_3:1;
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 as Convex_Combination of V by A5,A6,A21,CONVEX1:def 3;
take L;
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 thesis;
end;
suppose
A23: F = <*v2,v1,v3*>;
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 = <*jt*>^<*jt*>^<*jt*> by FINSEQ_1:def 10;
then rng f = rng (<*jt*>^<*jt*>) \/ rng <*jt*> by FINSEQ_1:31
.= rng <*jt*> \/ rng <*jt*> \/ rng <*jt*> by FINSEQ_1:31
.= {jt} by FINSEQ_1:38;
then reconsider 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;
assume
A27: n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A4,A6,A9,A12,A10,A11,A25,A24,A27,ENUMSET1:def 1
,FINSEQ_3:1;
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 as Convex_Combination of V by A5,A6,A26,CONVEX1:def 3;
take L;
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 thesis;
end;
suppose
A28: F = <* v2,v3,v1*>;
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 = <*jt*>^<*jt*>^<*jt*> by FINSEQ_1:def 10;
then rng f = rng (<*jt*>^<*jt*>) \/ rng <*jt*> by FINSEQ_1:31
.= rng <*jt*> \/ rng <*jt*> \/ rng <*jt*> by FINSEQ_1:31
.= {jt} by FINSEQ_1:38;
then reconsider 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;
assume
A32: n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A4,A6,A9,A12,A10,A11,A30,A29,A32,ENUMSET1:def 1
,FINSEQ_3:1;
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 as Convex_Combination of V by A5,A6,A31,CONVEX1:def 3;
take L;
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 thesis;
end;
suppose
A33: F = <* v3,v1,v2*>;
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 = <*jt*>^<*jt*>^<*jt*> by FINSEQ_1:def 10;
then rng f = rng (<*jt*>^<*jt*>) \/ rng <*jt*> by FINSEQ_1:31
.= rng <*jt*> \/ rng <*jt*> \/ rng <*jt*> by FINSEQ_1:31
.= {jt} by FINSEQ_1:38;
then reconsider 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;
assume
A37: n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A4,A6,A9,A12,A10,A11,A35,A34,A37,ENUMSET1:def 1
,FINSEQ_3:1;
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 as Convex_Combination of V by A5,A6,A36,CONVEX1:def 3;
take L;
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 thesis;
end;
suppose
A38: F = <* v3,v2,v1*>;
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 = <*jt*>^<*jt*>^<*jt*> by FINSEQ_1:def 10;
then rng f = rng (<*jt*>^<*jt*>) \/ rng <*jt*> by FINSEQ_1:31
.= rng <*jt*> \/ rng <*jt*> \/ rng <*jt*> by FINSEQ_1:31
.= {jt} by FINSEQ_1:38;
then reconsider 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;
assume
A42: n in dom f;
then n in Seg len f by FINSEQ_1:def 3;
hence thesis by A4,A6,A9,A12,A10,A11,A40,A39,A42,ENUMSET1:def 1
,FINSEQ_3:1;
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 as Convex_Combination of V by A5,A6,A41,CONVEX1:def 3;
take L;
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 thesis;
end;
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
set S = {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)};
let u,v be VECTOR of V;
let r be Real;
assume that
A2: 0 < r & r < 1 and
A3: u in M and
A4: 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 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 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;
reconsider r as Real;
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 S by A9,A10;
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;
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 Nat st 1 <= n & n < m & m <= len F holds F.n <>
F.m
proof
let n,m be Nat;
assume that
A5: 1 <= n and
A6: n < m and
A7: m <= len F;
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;
hence contradiction by A1,A6,A8,A9,FUNCT_1:def 4;
end;
assume
A10: card Carrier(L) >= 2;
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 as VECTOR of V by A15;
A16: F.(len F) in rng F by A14,FUNCT_1:3;
reconsider 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;
assume
A25: k in dom(f|i);
f|i = f|Seg i by FINSEQ_1:def 16;
then (f|i).k = f.k by A25,FUNCT_1:47;
hence thesis by A19,A25,A24;
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 16;
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 16;
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;
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;
assume that
A33: n in dom(F|i) and
A34: m in dom(F|i) and
A35: (F|i)/.n = (F|i)/.m;
F/.n = (F|i)/.n by A33,FINSEQ_4:70
.= F/.m by A34,A35,FINSEQ_4:70;
hence thesis by A1,A33,A34,A32,PARTFUN2:10;
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 P[object,object] means
($1 in (rng F \ {v}) implies $2 = r9*(L.$1)) & (not
($1 in (rng F \ {v})) implies $2 = 0);
A39: for x being object st x in the carrier of V
ex y being object st P[x,y]
proof
let x be object;
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
A40: dom L2 = the carrier of V &
for x being object st x in the carrier of
V holds P[x,L2.x] from CLASSES1:sch 1(A39);
for y being object st y in rng L2 holds y in REAL
proof
let y be object;
assume y in rng L2;
then consider x being object such that
A41: x in dom L2 and
A42: y = L2.x by FUNCT_1:def 3;
per cases;
suppose
A43: x in (rng F \ {v});
then x in rng F;
then reconsider x as VECTOR of V by A2;
y = r9*L.x by A40,A42,A43
.= (r9*L).x by RLVECT_2:def 11;
hence thesis;
end;
suppose
not x in (rng F \ {v});
then y = In(0,REAL) by A40,A41,A42;
hence thesis;
end;
end;
then rng L2 c= REAL;
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;
thus thesis by A2,A40;
end;
then reconsider L2 as Linear_Combination of V by A44,RLVECT_2:def 3;
for u being object st u in Carrier(L2) holds u in Carrier(L) \ {v}
proof
let u be object;
assume
A45: u in Carrier(L2);
then reconsider u as Element of V;
L2.u <> 0 by A45,RLVECT_2:19;
hence thesis by A2,A40;
end;
then
A46: Carrier(L2) c= Carrier(L) \ {v};
f/^i = <*f.(len f)*> by A17,A12,FINSEQ_5:30;
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: r9 > 0 by A18,A47,A29,XREAL_1:139;
for u being object st u in Carrier(L) \ {v} holds u in Carrier(L2)
proof
let u be object;
assume
A50: u in Carrier(L) \ {v};
then reconsider 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 = r9*L.u by A2,A40,A50;
then L2.u <> 0 by A49,A51,XCMPLX_1:6;
hence thesis by RLVECT_2:19;
end;
then Carrier(L) \ {v} c= Carrier(L2);
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;
then reconsider L2 as Linear_Combination of M by RLVECT_2:def 6;
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 dom f2 holds f2.k = F(
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 object st y in rng f2 holds y in REAL
proof
let y be object;
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;
then consider x being object 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 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 thesis by A53,A56,A57;
end;
then rng f2 c= REAL;
then reconsider 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 = (r9*(f|i)).k &
f2.k >= 0
proof
let k be Element of NAT;
assume
A63: k in dom f2;
then
A64: f2.k = L2.((F|i).k) by A53;
k in dom (f|Seg i) by A60,A63,FINSEQ_1:def 16;
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 16;
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};
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;
end;
f|i = f|(Seg i) by FINSEQ_1:def 16;
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;
per cases;
suppose
A75: w in (rng F \ {v});
f.k >= 0 by A19,A65;
then
A76: r9*(f|i).k >= 0 by A18,A47,A29,A72;
L2.w = r9*(L.w) by A40,A75
.= r9*(f|i).k by A73,A66,A67,FUNCT_1:47
.= (r9*(f|i)).k by RVSUM_1:44;
hence thesis by A64,A76,RVSUM_1:44;
end;
suppose
A77: not w in (rng F \ {v});
then not w in rng F by A69,XBOOLE_0:def 5;
then L.w = 0 by A2,RLVECT_2:19;
then
A78: r9*(f|i).k = 0 by A74;
f2.k = 0 by A40,A64,A77;
hence thesis by A78,RVSUM_1:44;
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;
then
A80: Sum(f) = Sum(f|i) + r by A38,RVSUM_1:74;
F/^i = <*F.(len F)*> by A12,FINSEQ_5:30;
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 = (r9*(f|i)).k by A62;
dom f2 = dom (r9*(f|i)) by A60,VALUED_1:def 5;
then f2 = r9*(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 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 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;
A88: (r*L1 +(1-r)*L2).u = (r*L1).u +((1-r)*L2).u by RLVECT_2:def 10;
per cases;
suppose
A89: u in Carrier L;
per cases;
suppose
A90: u = v;
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,27;
then
A92: r*L1.u = r;
L.u = r + 0 by A17,A19,A30,A90;
hence thesis by A88,A92,A91,RLVECT_2:def 11;
end;
suppose
u <> v;
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 = r9*(L.u) by A2,A40,A46;
then (1-r)*L2.u = ((1-r)*r9)*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 thesis by A88,A94,RLVECT_2:def 11;
end;
end;
suppose
A95: not u in Carrier L;
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 thesis by A88,A96,A97,RLVECT_2:def 11;
end;
end;
take L1,L2,r;
f.(len f) = L.(F.(len f)) by A19,A30;
then r <> 0 by A2,A17,A16,RLVECT_2:19;
hence thesis by A19,A30,A48,A86,A87,A84,CARD_1:30,CONVEX1:21,RLVECT_2:def 9;
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;
set S = {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)};
assume
A1: M is convex;
let v be object;
assume v in S;
then consider L being Convex_Combination of M such that
A2: v = Sum(L) and
L in ConvexComb(V);
reconsider v as VECTOR of V by A2;
per cases;
suppose
A3: card Carrier(L) < 2;
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 object such that
A5: Carrier(L) = {x} by CARD_2:42;
x in Carrier(L) by A5,TARSKI:def 1;
then reconsider 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 thesis by A6,ZFMISC_1:31;
end;
suppose
A7: 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;
A8: P[1]
proof
let LL be Convex_Combination of M;
assume that
A9: card Carrier LL = 1 + 1 and
A10: 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
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 object such that
A15: Carrier(L2) = {x2} by A9,A14,CARD_2:42;
x2 in Carrier(L2) by A15,TARSKI:def 1;
then reconsider 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 object such that
A18: Carrier(L1) = {x1} by A13,CARD_2:42;
x1 in Carrier(L1) by A18,TARSKI:def 1;
then reconsider 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 thesis by A1,A11,A20,A17,CONVEX1:def 2;
end;
consider k being Nat such that
A21: card Carrier L = k + 1 by A7,NAT_1:6;
reconsider k as non zero 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, 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 zero Nat st P[k] holds P[k+1]
proof
let k being non zero Nat;
assume
A25: P[k];
let LL be Convex_Combination of M;
assume that
A26: card Carrier LL = 1 + (k+1) and
A27: 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
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 be Convex_Combination of M, rr be 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 object such that
A33: Carrier(L1) = {x1} by A30,CARD_2:42;
x1 in Carrier(L1) by A33,TARSKI:def 1;
then reconsider 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 thesis by A1,A28,A35,A32,CONVEX1:def 2;
end;
for k being non zero Nat holds P[k] from NAT_1:sch 10(A8,A24);
hence thesis by A2,A22,A23;
end;
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;
consider m being object such that
A1: m in M by XBOOLE_0:def 1;
reconsider 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 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 object st x in N holds x in the carrier of V
proof
let x be object;
assume x in N;
then ex L being Convex_Combination of M st x = Sum L & L in ConvexComb(V);
hence thesis;
end;
then reconsider N as Subset of V by TARSKI:def 3;
for x being object 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 object;
assume
x in {Sum(L) where L is Convex_Combination of M : L in ConvexComb( V)};
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 thesis by A4,CONVEX2:6;
end;
then
A5: {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)} c= conv
(M);
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 that
A6: 0 < r & r < 1 and
A7: u in N and
A8: 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 r as Real;
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 thesis by A10,A9,A11;
end;
then
A12: N is convex by CONVEX1:def 2;
for v being object st v in M holds v in N
proof
let v be object;
assume
A13: v in M;
then reconsider 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 as Convex_Combination of M by A13,A15;
LL in ConvexComb(V) by Def1;
hence thesis by A14;
end;
then M c= N;
then conv(M) c= N by A12,CONVEX1:30;
hence thesis by A5,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;
registration
let V be non empty RLSStruct;
cluster cone for Subset of V;
existence
proof
{}V is cone;
hence thesis;
end;
end;
registration
let V be non empty RLSStruct;
cluster empty cone for Subset of V;
existence
proof
set M = {};
reconsider M as Subset of V by XBOOLE_1:2;
reconsider M as cone Subset of V by Th6;
take M;
thus thesis;
end;
end;
registration
let V be RealLinearSpace;
cluster non empty cone for 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 that
r > 0 and
A1: v in M;
v = 0.V by A1,TARSKI:def 1;
then r*v = 0.V;
hence thesis by TARSKI:def 1;
end;
then reconsider M as cone Subset of V by Def3;
take M;
thus thesis;
end;
end;
theorem Th7:
for V being non empty RLSStruct, M being cone Subset of V st V is
vector-distributive scalar-distributive scalar-associative 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;
let M be cone Subset of V;
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;
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
A3: 0 < r and
A4: r < 1 and
A5: u in M and
A6: v in M;
reconsider r as Real;
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 thesis by A2,A7;
end;
hence thesis by CONVEX1:def 2;
end;
assume
A8: V is vector-distributive scalar-distributive scalar-associative
scalar-unital;
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;
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 A9,CONVEX1:def 2;
then
A10: 2*(jd*u + jd*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 thesis by A8,A10,RLVECT_1:def 8;
end;
hence thesis;
end;
hence thesis by A1;
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 Carrier L <> {};
then consider u being object 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 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;
then reconsider 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;
assume v in Carrier L1;
then v = u by A3,TARSKI:def 1;
hence thesis by A2;
end;
defpred P[object,object] means
($1 in (Carrier L \ {u}) implies $2 = L.$1) & (not
($1 in (Carrier L \ {u})) implies $2 = 0);
A5: for x being object st x in the carrier of V
ex y being object st P[x,y]
proof
let x be object;
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
A6: dom L2 = the carrier of V &
for x being object st x in the carrier of
V holds P[x,L2.x] from CLASSES1:sch 1(A5);
for y being object st y in rng L2 holds y in REAL
proof
let y be object;
assume y in rng L2;
then consider x being object such that
A7: x in dom L2 and
A8: y = L2.x by FUNCT_1:def 3;
per cases;
suppose
A9: x in (Carrier L \ {u});
then reconsider x as VECTOR of V;
y = L.x by A6,A8,A9;
hence thesis;
end;
suppose
not x in (Carrier L \ {u});
then y = In(0,REAL) by A6,A7,A8;
hence thesis;
end;
end;
then rng L2 c= REAL;
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 as finite Subset of V;
take T;
thus thesis by A6;
end;
then reconsider L2 as Linear_Combination of V by A10,RLVECT_2:def 3;
for x being object st x in Carrier L2 holds x in M
proof
let x be object;
assume
A11: x in Carrier L2;
then reconsider 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 thesis by A12;
end;
then Carrier L2 c= M;
then reconsider L2 as Linear_Combination of M by RLVECT_2:def 6;
for x being object st x in Carrier L2 holds x in Carrier L \ {u}
proof
let x be object;
assume
A13: x in Carrier L2;
then reconsider x as VECTOR of V;
L2.x <> 0 by A13,RLVECT_2:19;
hence thesis by A6;
end;
then
A14: Carrier L2 c= Carrier L \ {u};
for v being VECTOR of V holds L.v = (L1 + L2).v
proof
let v be VECTOR of V;
per cases;
suppose
A15: v in Carrier L;
per cases;
suppose
A16: v = u;
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 thesis;
end;
suppose
A18: v <> u;
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 thesis;
end;
end;
suppose
A21: not v in Carrier L;
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 thesis by A21,RLVECT_2:19;
end;
end;
then
A24: L = L1 + L2 by RLVECT_2:def 9;
for x being object st x in Carrier L \ {u} holds x in Carrier L2
proof
let x be object;
assume
A25: x in Carrier L \ {u};
then reconsider 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 thesis by A26,RLVECT_2:19;
end;
then Carrier L \ {u} c= Carrier L2;
then
A27: Carrier L2 = Carrier L \ {u} by A14,XBOOLE_0:def 10;
take L1,L2;
A28: Carrier L \ {u} c= Carrier L by XBOOLE_1:36;
Carrier L1 <> {}
proof
assume Carrier L1 = {};
then L.u = 0 by A2,RLVECT_2:19;
hence contradiction by A1,RLVECT_2:19;
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 thesis by A1,A4,A6,A29,A14,A24,A28,CARD_1:30,RLVECT_3:1,ZFMISC_1:31;
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: (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;
A3: 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 that
A4: r > 0 and
A5: v in M;
reconsider r as Real;
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;
A8: Carrier L c= {v} by RLVECT_2:def 6;
assume u in Carrier L;
hence thesis by A4,A6,A8,TARSKI:def 1;
end;
A9: v in Carrier L by A4,A6,RLVECT_2:19;
{v} c= M by A5,ZFMISC_1:31;
then reconsider L as Linear_Combination of M by RLVECT_2:21;
Sum L in M by A2,A9,A7;
hence thesis by A6,RLVECT_2:32;
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;
assume that
A11: u in M and
A12: v in M;
per cases;
suppose
A13: u <> v;
consider L being Linear_Combination of {u,v} such that
A14: L.u = jj & L.v = jj 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;
A18: Carrier L c= {u,v} by RLVECT_2:def 6;
assume
A19: v1 in Carrier L;
per cases by A19,A18,TARSKI:def 2;
suppose
v1 = u;
hence thesis by A14;
end;
suppose
v1 = v;
hence thesis by A14;
end;
end;
{u,v} c= M by A11,A12,ZFMISC_1:32;
then reconsider L as Linear_Combination of M by RLVECT_2:21;
Sum L in M by A2,A16,A17;
hence thesis by A15;
end;
suppose
A20: u = v;
(jj+jj)*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 thesis by A20,RLVECT_1:def 8;
end;
end;
M is cone by A3;
hence thesis by A10,Th7;
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 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;
assume that
A21: M is convex and
A22: M is cone;
A23: P[1]
proof
let LL be Linear_Combination of 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;
consider x being object 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 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 thesis by A22,A27,A28;
end;
A29: for k being non zero Nat st P[k] holds P[k+1]
proof
let k be non zero Nat;
assume
A30: P[k];
let LL be Linear_Combination of 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;
consider L1,L2 be 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;
assume
A42: u in Carrier L1;
then L1.u = LL.u by A39;
hence thesis by A32,A37,A42;
end;
A43: for u being VECTOR of V st u in Carrier L2 holds L2.u > 0
proof
let u be VECTOR of V;
assume
A44: u in Carrier L2;
then L2.u = LL.u by A40;
hence thesis by A32,A38,A44;
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 thesis by A21,A22,A34,A45,Th7;
end;
A46: for k being non zero Nat holds P[k] from NAT_1:sch 10(A23,A29);
let L be Linear_Combination of M;
assume that
A47: Carrier L <> {} and
A48: for v being VECTOR of V st v in Carrier L holds L.v > 0;
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 thesis by A47,A48,A46;
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 that
A3: r > 0 and
A4: v in M /\ N;
v in N by A4,XBOOLE_0:def 4;
then
A5: r*v in N by A2,A3;
v in M by A4,XBOOLE_0:def 4;
then r*v in M by A1,A3;
hence thesis by A5,XBOOLE_0:def 4;
end;