:: Convex Sets and Convex Combinations
:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received November 5, 2002
:: Copyright (c) 2002-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, XBOOLE_0, RLVECT_1, SUBSET_1, REAL_1, RELAT_1, CARD_1,
ARYTM_3, ARYTM_1, TARSKI, SUPINF_2, ALGSTR_0, RUSUB_4, RLSUB_1, STRUCT_0,
XXREAL_0, SETFAM_1, BHSP_1, PROB_2, RLVECT_2, FINSEQ_1, FUNCT_1, CARD_3,
NAT_1, PARTFUN1, VALUED_1, CONVEX1;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, DOMAIN_1, STRUCT_0,
ALGSTR_0, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, FUNCT_1, NAT_1,
REAL_1, PARTFUN1, FINSEQ_1, RLVECT_1, RLSUB_1, RLVECT_2, RVSUM_1, BHSP_1,
RUSUB_4, RUSUB_5, XXREAL_0;
constructors SETFAM_1, DOMAIN_1, XXREAL_0, REAL_1, PARTFUN1, BINOP_2,
FINSEQ_4, FINSOP_1, RVSUM_1, RLVECT_2, RUSUB_5, RELSET_1;
registrations SUBSET_1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, STRUCT_0,
RLVECT_1, RUSUB_4, VALUED_0, FINSEQ_1, CARD_1, ORDINAL1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities XBOOLE_0, RLVECT_1, RVSUM_1;
expansions TARSKI, XBOOLE_0;
theorems BHSP_1, RLVECT_1, RVSUM_1, FUNCT_1, FINSEQ_1, TARSKI, ZFMISC_1,
XBOOLE_0, SETFAM_1, RLSUB_1, RUSUB_4, RUSUB_5, RLVECT_2, CARD_1,
FINSEQ_3, FINSEQ_4, CARD_2, ENUMSET1, XCMPLX_1, XREAL_1, FINSOP_1,
PARTFUN1;
schemes DOMAIN_1, SUBSET_1;
begin :: Convex Sets
definition
let V be non empty RLSStruct, M be Subset of V, r be Real;
func r*M -> Subset of V equals
{r * v where v is Element of V: v in M};
coherence
proof
deffunc F(Element of V) = r * $1;
defpred P[set] means $1 in M;
{F(v) where v is Element of V: P[v]} is Subset of V from DOMAIN_1:sch
8;
hence thesis;
end;
end;
definition
let V be non empty RLSStruct, M be Subset of V;
attr M is convex means
:Def2:
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;
end;
theorem
for V being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct, M being Subset
of V, r being Real st M is convex holds r*M is convex
proof
let V be vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct;
let M be Subset of V;
let r be Real;
assume
A1: M is convex;
for u,v being VECTOR of V, p being Real
st 0 < p & p < 1 & u in r*M & v
in r*M holds p*u + (1-p)*v in r*M
proof
let u,v be VECTOR of V;
let p be Real;
assume that
A2: 0 < p & p < 1 and
A3: u in r*M and
A4: v in r*M;
consider v9 be Element of V such that
A5: v = r*v9 and
A6: v9 in M by A4;
consider u9 be Element of V such that
A7: u = r * u9 and
A8: u9 in M by A3;
A9: p*u + (1-p)*v = r*p*u9 + (1-p)*(r*v9) by A7,A5,RLVECT_1:def 7
.= r*p*u9 + r*(1-p)*v9 by RLVECT_1:def 7
.= r*(p*u9) + r*(1-p)*v9 by RLVECT_1:def 7
.= r*(p*u9) + r*((1-p)*v9) by RLVECT_1:def 7
.= r*(p*u9 + (1-p)*v9) by RLVECT_1:def 5;
p*u9 + (1-p)*v9 in M by A1,A2,A8,A6;
hence thesis by A9;
end;
hence thesis;
end;
theorem
for V being Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty
RLSStruct, M,N being Subset of V st M is convex & N is convex holds M + N is
convex
proof
let V be Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty RLSStruct;
let M,N be Subset of V;
assume
A1: M is convex & N is convex;
for u,v being VECTOR of V, r being Real
st 0 < r & r < 1 & u in M+N & v
in M+N holds r*u + (1-r)*v in M+N
proof
let u,v be VECTOR of V;
let r be Real;
assume that
A2: 0 < r & r < 1 and
A3: u in M+N and
A4: v in M+N;
v in {x + y where x,y is Element of V : x in M & y in N} by A4,
RUSUB_4:def 9;
then consider x2,y2 being Element of V such that
A5: v = x2 + y2 and
A6: x2 in M & y2 in N;
u in {x + y where x,y is Element of V : x in M & y in N} by A3,
RUSUB_4:def 9;
then consider x1,y1 being Element of V such that
A7: u = x1 + y1 and
A8: x1 in M & y1 in N;
A9: r*u + (1-r)*v = r*x1 + r*y1 + (1-r)*(x2+y2) by A7,A5,RLVECT_1:def 5
.= r*x1 + r*y1 + ((1-r)*x2 + (1-r)*y2) by RLVECT_1:def 5
.= r*x1 + r*y1 + (1-r)*x2 + (1-r)*y2 by RLVECT_1:def 3
.= r*x1 + (1-r)*x2 + r*y1 + (1-r)*y2 by RLVECT_1:def 3
.= (r*x1 + (1-r)*x2) + (r*y1 + (1-r)*y2) by RLVECT_1:def 3;
r*x1 + (1-r)*x2 in M & r*y1 + (1-r)*y2 in N by A1,A2,A8,A6;
then r*u + (1-r)*v in {x + y where x,y is Element of V : x in M & y in N}
by A9;
hence thesis by RUSUB_4:def 9;
end;
hence thesis;
end;
theorem
for V being RealLinearSpace, M,N being Subset of V st M is convex & N
is convex holds M - N is convex
proof
let V be RealLinearSpace;
let M,N be Subset of V;
assume
A1: M is convex & N is convex;
for u,v being VECTOR of V, r being Real
st 0 < r & r < 1 & u in M-N & v
in M-N holds r*u + (1-r)*v in M-N
proof
let u,v be VECTOR of V;
let r be Real;
assume that
A2: 0 < r & r < 1 and
A3: u in M-N and
A4: v in M-N;
v in {x - y where x,y is Element of V : x in M & y in N} by A4,
RUSUB_5:def 2;
then consider x2,y2 being Element of V such that
A5: v = x2 - y2 and
A6: x2 in M & y2 in N;
u in {x - y where x,y is Element of V : x in M & y in N} by A3,
RUSUB_5:def 2;
then consider x1,y1 being Element of V such that
A7: u = x1 - y1 and
A8: x1 in M & y1 in N;
A9: r*u + (1-r)*v = r*x1 - r*y1 + (1-r)*(x2-y2) by A7,A5,RLVECT_1:34
.= r*x1 - r*y1 + ((1-r)*x2 - (1-r)*y2) by RLVECT_1:34
.= r*x1 - r*y1 + (1-r)*x2 - (1-r)*y2 by RLVECT_1:def 3
.= r*x1 - (r*y1 - (1-r)*x2) - (1-r)*y2 by RLVECT_1:29
.= r*x1 + ((1-r)*x2 + (- r*y1)) - (1-r)*y2 by RLVECT_1:33
.= r*x1 + (1-r)*x2 + (- r*y1) - (1-r)*y2 by RLVECT_1:def 3
.= r*x1 + (1-r)*x2 + ((- r*y1) - (1-r)*y2) by RLVECT_1:def 3
.= (r*x1 + (1-r)*x2) - (r*y1 + (1-r)*y2) by RLVECT_1:30;
r*x1 + (1-r)*x2 in M & r*y1 + (1-r)*y2 in N by A1,A2,A8,A6;
then r*u + (1-r)*v in {x - y where x,y is Element of V : x in M & y in N}
by A9;
hence thesis by RUSUB_5:def 2;
end;
hence thesis;
end;
theorem Th4:
for V being non empty RLSStruct, M being Subset of V holds M is
convex iff for r being Real
st 0 < r & r < 1 holds r*M + (1-r)*M c= M
proof
let V be non empty RLSStruct;
let M be Subset of V;
thus M is convex implies for r being Real
st 0 < r & r < 1 holds r*M + (1-r)*
M c= M
proof
assume
A1: M is convex;
let r be Real;
assume
A2: 0 < r & r < 1;
for x being Element of V st x in r*M + (1-r)*M holds x in M
proof
let x be Element of V;
assume x in r*M + (1-r)*M;
then
x in {u + v where u,v is Element of V : u in r*M & v in (1-r)*M} by
RUSUB_4:def 9;
then consider u,v be Element of V such that
A3: x = u + v and
A4: u in r*M & v in (1-r)*M;
(ex w1 be Element of V st u = r * w1 & w1 in M )& ex w2 be Element
of V st v = (1-r)*w2 & w2 in M by A4;
hence thesis by A1,A2,A3;
end;
hence thesis;
end;
assume
A5: for r being Real st 0 < r & r < 1 holds r*M + (1-r)*M c= M;
let u,v be VECTOR of V;
let r be Real;
assume 0 < r & r < 1;
then
A6: r*M + (1-r)*M c= M by A5;
assume u in M & v in M;
then r*u in r*M & (1-r)*v in {(1-r)*w where w is Element of V: w in M};
then
r*u + (1-r)*v in {p+q where p,q is Element of V: p in r*M & q in (1-r )*M};
then r*u + (1-r)*v in r*M + (1-r)*M by RUSUB_4:def 9;
hence thesis by A6;
end;
theorem
for V being Abelian non empty RLSStruct, M being Subset of V st M is
convex
for r being Real st 0 < r & r < 1 holds (1-r)*M + r*M c= M
proof
let V be Abelian non empty RLSStruct;
let M be Subset of V;
assume
A1: M is convex;
let r be Real;
assume
A2: 0 < r & r < 1;
for x being Element of V st x in (1-r)*M + r*M holds x in M
proof
let x be Element of V;
assume x in (1-r)*M + r*M;
then x in {u + v where u,v is Element of V : u in (1-r)*M & v in r*M} by
RUSUB_4:def 9;
then consider u,v be Element of V such that
A3: x = u + v and
A4: u in (1-r)*M & v in r*M;
(ex w1 be Element of V st u = (1-r) * w1 & w1 in M )& ex w2 be
Element of V st v = r*w2 & w2 in M by A4;
hence thesis by A1,A2,A3;
end;
hence thesis;
end;
theorem
for V being Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty
RLSStruct, M,N being Subset of V st M is convex & N is convex holds for r
being Real holds r*M + (1-r)*N is convex
proof
let V be Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty RLSStruct;
let M,N be Subset of V;
assume that
A1: M is convex and
A2: N is convex;
let r be Real;
let u,v be VECTOR of V;
let p be Real;
assume that
A3: 0 < p & p < 1 and
A4: u in r*M + (1-r)*N and
A5: v in r*M + (1-r)*N;
A6: u in {x1 + y1 where x1,y1 is VECTOR of V : x1 in r*M & y1 in (1-r)*N} by A4
,RUSUB_4:def 9;
v in {x2 + y2 where x2,y2 is VECTOR of V : x2 in r*M & y2 in (1-r)*N}
by A5,RUSUB_4:def 9;
then consider x2,y2 be VECTOR of V such that
A7: v = x2 + y2 and
A8: x2 in r*M and
A9: y2 in (1-r)*N;
consider x1,y1 be VECTOR of V such that
A10: u = x1 + y1 and
A11: x1 in r*M and
A12: y1 in (1-r)*N by A6;
consider mx2 be VECTOR of V such that
A13: x2 = r*mx2 and
A14: mx2 in M by A8;
consider mx1 be VECTOR of V such that
A15: x1 = r*mx1 and
A16: mx1 in M by A11;
A17: p*x1 + (1-p)*x2 = p*r*mx1 + (1-p)*(r*mx2) by A15,A13,RLVECT_1:def 7
.= p*r*mx1 + (1-p)*r*mx2 by RLVECT_1:def 7
.= r*(p*mx1) + (1-p)*r*mx2 by RLVECT_1:def 7
.= r*(p*mx1) + r*((1-p)*mx2) by RLVECT_1:def 7
.= r*(p*mx1 + (1-p)*mx2) by RLVECT_1:def 5;
consider ny2 be VECTOR of V such that
A18: y2 = (1-r)*ny2 and
A19: ny2 in N by A9;
consider ny1 be VECTOR of V such that
A20: y1 = (1-r)*ny1 and
A21: ny1 in N by A12;
A22: p*y1 + (1-p)*y2 = p*(1-r)*ny1 + (1-p)*((1-r)*ny2) by A20,A18,
RLVECT_1:def 7
.= p*(1-r)*ny1 + (1-p)*(1-r)*ny2 by RLVECT_1:def 7
.= (1-r)*(p*ny1) + (1-p)*(1-r)*ny2 by RLVECT_1:def 7
.= (1-r)*(p*ny1) + (1-r)*((1-p)*ny2) by RLVECT_1:def 7
.= (1-r)*(p*ny1 + (1-p)*ny2) by RLVECT_1:def 5;
p*ny1 + (1-p)*ny2 in N by A2,A3,A21,A19;
then
A23: p*y1 + (1-p)*y2 in (1-r)*N by A22;
p*mx1 + (1-p)*mx2 in M by A1,A3,A16,A14;
then
A24: p*x1 + (1-p)*x2 in {r*w where w is VECTOR of V : w in M} by A17;
p*u + (1-p)*v = p*x1 + p*y1 + (1-p)*(x2 + y2) by A10,A7,RLVECT_1:def 5
.= p*x1 + p*y1 + ((1-p)*x2 + (1-p)*y2) by RLVECT_1:def 5
.= p*x1 + p*y1 + (1-p)*x2 + (1-p)*y2 by RLVECT_1:def 3
.= p*x1 + (1-p)*x2 + p*y1 + (1-p)*y2 by RLVECT_1:def 3
.= (p*x1 + (1-p)*x2) + (p*y1 + (1-p)*y2) by RLVECT_1:def 3;
then p*u + (1-p)*v in {w1 + w2 where w1,w2 is VECTOR of V : w1 in r*M & w2
in (1-r)*N} by A24,A23;
hence thesis by RUSUB_4:def 9;
end;
Lm1: for V being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct, M be Subset of V
holds 1*M = M
proof
let V be vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct;
let M be Subset of V;
for v being Element of V st v in M holds v in 1*M
proof
let v be Element of V;
A1: v = 1*v by RLVECT_1:def 8;
assume v in M;
hence thesis by A1;
end;
then
A2: M c= 1*M;
for v being Element of V st v in 1*M holds v in M
proof
let v be Element of V;
assume v in 1*M;
then ex x be Element of V st v = 1*x & x in M;
hence thesis by RLVECT_1:def 8;
end;
then 1*M c= M;
hence thesis by A2;
end;
Lm2: for V being RealLinearSpace, M be non empty Subset of V holds 0 * M = {0.
V}
proof
let V be RealLinearSpace;
let M be non empty Subset of V;
for v being Element of V st v in {0.V} holds v in 0 * M
proof
let v be Element of V;
consider x be object such that
A1: x in M by XBOOLE_0:def 1;
reconsider x as Element of V by A1;
assume v in {0.V};
then v = 0.V by TARSKI:def 1;
then v = 0 * x by RLVECT_1:10;
hence thesis by A1;
end;
then
A2: {0.V} c= 0 * M;
for v being Element of V st v in 0 * M holds v in {0.V}
proof
let v be Element of V;
assume v in 0 * M;
then ex x be Element of V st v = 0 * x & x in M;
then v = 0.V by RLVECT_1:10;
hence thesis by TARSKI:def 1;
end;
then 0 * M c= {0.V};
hence thesis by A2;
end;
Lm3: for V be add-associative non empty addLoopStr, M1,M2,M3 be Subset of V
holds (M1 + M2) + M3 = M1 + (M2 + M3)
proof
let V be add-associative non empty addLoopStr;
let M1,M2,M3 be Subset of V;
for x being Element of V st x in M1 + (M2 + M3) holds x in (M1 + M2) + M3
proof
let x be Element of V;
assume x in M1 + (M2 + M3);
then x in {u + v where u,v is Element of V : u in M1 & v in M2 + M3} by
RUSUB_4:def 9;
then consider x1,x9 be Element of V such that
A1: x = x1 + x9 and
A2: x1 in M1 and
A3: x9 in M2+M3;
x9 in {u + v where u,v is Element of V : u in M2 & v in M3} by A3,
RUSUB_4:def 9;
then consider x2,x3 be Element of V such that
A4: x9 = x2 + x3 and
A5: x2 in M2 and
A6: x3 in M3;
x1 + x2 in {u + v where u,v is Element of V : u in M1 & v in M2} by A2,A5;
then
A7: x1 + x2 in M1 + M2 by RUSUB_4:def 9;
x= (x1 + x2) + x3 by A1,A4,RLVECT_1:def 3;
then
x in {u + v where u,v is Element of V : u in M1+M2 & v in M3} by A6,A7;
hence thesis by RUSUB_4:def 9;
end;
then
A8: M1 + (M2 + M3) c= (M1 + M2) + M3;
for x being Element of V st x in (M1 + M2) + M3 holds x in M1 + (M2 + M3 )
proof
let x be Element of V;
assume x in (M1 + M2) + M3;
then x in {u + v where u,v is Element of V : u in M1 + M2 & v in M3} by
RUSUB_4:def 9;
then consider x9,x3 be Element of V such that
A9: x = x9 + x3 and
A10: x9 in M1 + M2 and
A11: x3 in M3;
x9 in {u + v where u,v is Element of V : u in M1 & v in M2} by A10,
RUSUB_4:def 9;
then consider x1,x2 be Element of V such that
A12: x9 = x1 + x2 and
A13: x1 in M1 and
A14: x2 in M2;
x2 + x3 in {u + v where u,v is Element of V : u in M2 & v in M3} by A11,A14
;
then
A15: x2 + x3 in M2 + M3 by RUSUB_4:def 9;
x = x1 + (x2 + x3) by A9,A12,RLVECT_1:def 3;
then
x in {u + v where u,v is Element of V : u in M1 & v in M2 + M3} by A13,A15;
hence thesis by RUSUB_4:def 9;
end;
then (M1 + M2) + M3 c= M1 + (M2 + M3);
hence thesis by A8;
end;
Lm4: for V being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct, M being Subset of
V, r1,r2 being Real holds r1*(r2*M) = (r1*r2)*M
proof
let V be vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct;
let M be Subset of V;
let r1,r2 be Real;
for x being VECTOR of V st x in r1*(r2*M) holds x in (r1*r2)*M
proof
let x be VECTOR of V;
assume x in r1*(r2*M);
then consider w1 be VECTOR of V such that
A1: x = r1*w1 and
A2: w1 in r2*M;
consider w2 be VECTOR of V such that
A3: w1 = r2*w2 and
A4: w2 in M by A2;
x = (r1*r2)*w2 by A1,A3,RLVECT_1:def 7;
hence thesis by A4;
end;
then
A5: r1*(r2*M) c= (r1*r2)*M;
for x being VECTOR of V st x in (r1*r2)*M holds x in r1*(r2*M)
proof
let x be VECTOR of V;
assume x in (r1*r2)*M;
then consider w1 be VECTOR of V such that
A6: x = (r1*r2)*w1 & w1 in M;
x = r1*(r2*w1) & r2*w1 in r2*M by A6,RLVECT_1:def 7;
hence thesis;
end;
then (r1*r2)*M c= r1*(r2*M);
hence thesis by A5;
end;
Lm5: for V being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct, M1,M2 being
Subset of V, r being Real holds r*(M1 + M2) = r*M1 + r*M2
proof
let V be vector-distributive scalar-distributive scalar-associative
scalar-unital
non empty RLSStruct;
let M1,M2 be Subset of V;
let r be Real;
for x being VECTOR of V st x in r*M1 + r*M2 holds x in r*(M1+M2)
proof
let x be VECTOR of V;
assume x in r*M1 + r*M2;
then x in {u + v where u,v is VECTOR of V : u in r*M1 & v in r*M2} by
RUSUB_4:def 9;
then consider w1,w2 be VECTOR of V such that
A1: x = w1 + w2 and
A2: w1 in r*M1 and
A3: w2 in r*M2;
consider v2 be VECTOR of V such that
A4: w2 = r * v2 and
A5: v2 in M2 by A3;
consider v1 be VECTOR of V such that
A6: w1 = r * v1 and
A7: v1 in M1 by A2;
v1 + v2 in {u + v where u,v is VECTOR of V : u in M1 & v in M2} by A7,A5;
then
A8: v1 + v2 in M1 + M2 by RUSUB_4:def 9;
x = r*(v1 + v2) by A1,A6,A4,RLVECT_1:def 5;
hence thesis by A8;
end;
then
A9: r*M1 + r*M2 c= r*(M1+M2);
for x being VECTOR of V st x in r*(M1+M2) holds x in r*M1 + r*M2
proof
let x be VECTOR of V;
assume x in r*(M1+M2);
then consider w9 be VECTOR of V such that
A10: x = r*w9 and
A11: w9 in M1 + M2;
w9 in {u + v where u,v is VECTOR of V : u in M1 & v in M2} by A11,
RUSUB_4:def 9;
then consider w1,w2 be VECTOR of V such that
A12: w9 = w1 + w2 and
A13: w1 in M1 & w2 in M2;
A14: r*w1 in r*M1 & r*w2 in {r*w where w is VECTOR of V : w in M2} by A13;
x = r*w1 + r*w2 by A10,A12,RLVECT_1:def 5;
then x in {u + v where u,v is VECTOR of V : u in r*M1 & v in r*M2} by A14;
hence thesis by RUSUB_4:def 9;
end;
then r*(M1 + M2) c= r*M1 + r*M2;
hence thesis by A9;
end;
theorem
for V being RealLinearSpace, M being Subset of V, v being VECTOR of V
holds M is convex iff v + M is convex
proof
let V be RealLinearSpace;
let M be Subset of V;
let v be VECTOR of V;
A1: v + M is convex implies M is convex
proof
assume
A2: v + M is convex;
let w1,w2 be VECTOR of V;
let r be Real;
assume that
A3: 0 < r & r < 1 and
A4: w1 in M and
A5: w2 in M;
set x2 = v + w2;
x2 in {v + w where w is VECTOR of V : w in M} by A5;
then
A6: x2 in v + M by RUSUB_4:def 8;
set x1 = v + w1;
A7: r*x1 + (1-r)*x2 = r*v + r*w1 + (1-r)*(v + w2) by RLVECT_1:def 5
.= r*v + r*w1 + ((1-r)*v + (1-r)*w2) by RLVECT_1:def 5
.= r*v + r*w1 + (1-r)*v + (1-r)*w2 by RLVECT_1:def 3
.= r*v + (1-r)*v + r*w1 + (1-r)*w2 by RLVECT_1:def 3
.= (r+(1-r))*v + r*w1 + (1-r)*w2 by RLVECT_1:def 6
.= v + r*w1 + (1-r)*w2 by RLVECT_1:def 8
.= v + (r*w1 + (1-r)*w2) by RLVECT_1:def 3;
x1 in {v + w where w is VECTOR of V : w in M} by A4;
then x1 in v + M by RUSUB_4:def 8;
then r*x1 + (1-r)*x2 in v + M by A2,A3,A6;
then v + (r*w1 + (1-r)*w2) in {v + w where w is VECTOR of V : w in M} by A7
,RUSUB_4:def 8;
then ex w be VECTOR of V st v + (r*w1 + (1-r)*w2) = v + w & w in M;
hence thesis by RLVECT_1:8;
end;
M is convex implies v + M is convex
proof
assume
A8: M is convex;
let w1,w2 be VECTOR of V;
let r be Real;
assume that
A9: 0 < r & r < 1 and
A10: w1 in v + M and
A11: w2 in v + M;
w2 in {v + w where w is VECTOR of V : w in M} by A11,RUSUB_4:def 8;
then consider x2 be VECTOR of V such that
A12: w2 = v + x2 and
A13: x2 in M;
w1 in {v + w where w is VECTOR of V : w in M} by A10,RUSUB_4:def 8;
then consider x1 be VECTOR of V such that
A14: w1 = v + x1 and
A15: x1 in M;
A16: r*w1 + (1-r)*w2 = r*v + r*x1 + (1-r)*(v+x2) by A14,A12,RLVECT_1:def 5
.= r*v + r*x1 + ((1-r)*v + (1-r)*x2) by RLVECT_1:def 5
.= r*v + r*x1 + (1-r)*v + (1-r)*x2 by RLVECT_1:def 3
.= r*v + (1-r)*v + r*x1 + (1-r)*x2 by RLVECT_1:def 3
.= (r+(1-r))*v + r*x1 + (1-r)*x2 by RLVECT_1:def 6
.= v + r*x1 + (1-r)*x2 by RLVECT_1:def 8
.= v + (r*x1 + (1-r)*x2) by RLVECT_1:def 3;
r*x1 + (1-r)*x2 in M by A8,A9,A15,A13;
then r*w1 + (1-r)*w2 in {v + w where w is VECTOR of V : w in M} by A16;
hence thesis by RUSUB_4:def 8;
end;
hence thesis by A1;
end;
theorem
for V being RealLinearSpace holds Up((0).V) is convex
proof
let V be RealLinearSpace;
let u,v be VECTOR of V;
let r be Real;
assume that
0 < r and
r < 1 and
A1: u in Up((0).V) and
A2: v in Up((0).V);
v in the carrier of (0).V by A2,RUSUB_4:def 5;
then v in {0.V} by RLSUB_1:def 3;
then
A3: v = 0.V by TARSKI:def 1;
u in the carrier of (0).V by A1,RUSUB_4:def 5;
then u in {0.V} by RLSUB_1:def 3;
then u = 0.V by TARSKI:def 1;
then r * u + (1-r) * v = 0.V + (1-r) * 0.V by A3
.= 0.V + 0.V
.= 0.V;
then r * u + (1-r) * v in {0.V} by TARSKI:def 1;
then r * u + (1-r) * v in the carrier of (0).V by RLSUB_1:def 3;
hence thesis by RUSUB_4:def 5;
end;
theorem Th9:
for V being RealLinearSpace holds Up((Omega).V) is convex
proof
let V be RealLinearSpace;
let u,v be VECTOR of V;
let r be Real;
(Omega).V = the RLSStruct of V by RLSUB_1:def 4;
then r * u + (1-r) * v in the carrier of (Omega).V;
hence thesis by RUSUB_4:def 5;
end;
theorem
for V being non empty RLSStruct, M being Subset of V st M = {}
holds M is convex;
theorem Th11:
for V being Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non
empty RLSStruct, M1,M2 being Subset of V, r1,r2 being Real
st M1 is convex & M2 is convex holds r1*M1 + r2*M2 is convex
proof
let V be Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty RLSStruct;
let M1,M2 be Subset of V;
let r1,r2 be Real;
assume that
A1: M1 is convex and
A2: M2 is convex;
let u,v be VECTOR of V;
let p be Real;
assume that
A3: 0 < p & p < 1 and
A4: u in r1*M1 + r2*M2 and
A5: v in r1*M1 + r2*M2;
v in {x+y where x,y is VECTOR of V : x in r1*M1 & y in r2*M2} by A5,
RUSUB_4:def 9;
then consider v1,v2 be VECTOR of V such that
A6: v = v1 + v2 and
A7: v1 in r1*M1 and
A8: v2 in r2*M2;
u in {x+y where x,y is VECTOR of V : x in r1*M1 & y in r2*M2} by A4,
RUSUB_4:def 9;
then consider u1,u2 be VECTOR of V such that
A9: u = u1 + u2 and
A10: u1 in r1*M1 and
A11: u2 in r2*M2;
consider y1 be VECTOR of V such that
A12: v1 = r1*y1 and
A13: y1 in M1 by A7;
consider x1 be VECTOR of V such that
A14: u1 = r1*x1 and
A15: x1 in M1 by A10;
A16: p*u1 + (1-p)*v1 = r1*p*x1 + (1-p)*(r1*y1) by A14,A12,RLVECT_1:def 7
.= r1*p*x1 + r1*(1-p)*y1 by RLVECT_1:def 7
.= r1*(p*x1) + r1*(1-p)*y1 by RLVECT_1:def 7
.= r1*(p*x1) + r1*((1-p)*y1) by RLVECT_1:def 7
.= r1*(p*x1 + (1-p)*y1) by RLVECT_1:def 5;
consider y2 be VECTOR of V such that
A17: v2 = r2*y2 and
A18: y2 in M2 by A8;
consider x2 be VECTOR of V such that
A19: u2 = r2*x2 and
A20: x2 in M2 by A11;
A21: p*u2 + (1-p)*v2 = r2*p*x2 + (1-p)*(r2*y2) by A19,A17,RLVECT_1:def 7
.= r2*p*x2 + r2*(1-p)*y2 by RLVECT_1:def 7
.= r2*(p*x2) + r2*(1-p)*y2 by RLVECT_1:def 7
.= r2*(p*x2) + r2*((1-p)*y2) by RLVECT_1:def 7
.= r2*(p*x2 + (1-p)*y2) by RLVECT_1:def 5;
p*x2 + (1-p)*y2 in M2 by A2,A3,A20,A18;
then
A22: p*u2 + (1-p)*v2 in r2*M2 by A21;
p*x1 + (1-p)*y1 in M1 by A1,A3,A15,A13;
then
A23: p*u1 + (1-p)*v1 in {r1*x where x is VECTOR of V: x in M1} by A16;
p*(u1+u2) + (1-p)*(v1+v2) = p*u1 + p*u2 + (1-p)*(v1+v2) by RLVECT_1:def 5
.= p*u1 + p*u2 + ((1-p)*v1 + (1-p)*v2) by RLVECT_1:def 5
.= p*u1 + p*u2 + (1-p)*v1 + (1-p)*v2 by RLVECT_1:def 3
.= p*u1 + (1-p)*v1 + p*u2 + (1-p)*v2 by RLVECT_1:def 3
.= p*u1 + (1-p)*v1 + (p*u2 + (1-p)*v2) by RLVECT_1:def 3;
then p*(u1+u2) + (1-p)*(v1+v2) in {x+y where x,y is VECTOR of V: x in r1*M1
& y in r2*M2} by A23,A22;
hence thesis by A9,A6,RUSUB_4:def 9;
end;
theorem Th12:
for V being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct, M being
Subset of V, r1,r2 being Real holds (r1 + r2)*M c= r1*M + r2*M
proof
let V be vector-distributive scalar-distributive scalar-associative
scalar-unital
non empty RLSStruct;
let M be Subset of V;
let r1,r2 be Real;
for x being VECTOR of V st x in (r1+r2)*M holds x in r1*M + r2*M
proof
let x be VECTOR of V;
assume x in (r1+r2)*M;
then consider w be VECTOR of V such that
A1: x = (r1 + r2)*w and
A2: w in M;
A3: r2*w in {r2*u where u is VECTOR of V : u in M} by A2;
x = r1*w + r2*w & r1*w in r1*M by A1,A2,RLVECT_1:def 6;
then x in {u + v where u,v is VECTOR of V : u in r1*M & v in r2*M} by A3;
hence thesis by RUSUB_4:def 9;
end;
hence thesis;
end;
Lm6: for V being non empty RLSStruct, M,N being Subset of V,
r being Real st M c= N holds r*M c= r*N
proof
let V be non empty RLSStruct;
let M,N be Subset of V;
let r be Real;
assume
A1: M c= N;
for x being VECTOR of V st x in r*M holds x in r*N
proof
let x be VECTOR of V;
assume x in r*M;
then ex w be VECTOR of V st x = r*w & w in M;
hence thesis by A1;
end;
hence thesis;
end;
Lm7: for V being non empty RLSStruct, M being empty Subset of V,
r being Real
holds r * M = {}
proof
let V be non empty RLSStruct;
let M be empty Subset of V;
let r be Real;
for x being VECTOR of V st x in r * M holds x in {}
proof
let x be VECTOR of V;
assume x in r * M;
then ex v be VECTOR of V st x = r * v & v in {};
hence thesis;
end;
then r * M c= {};
hence thesis;
end;
Lm8: for V being non empty addLoopStr, M being empty Subset of V, N being
Subset of V holds M + N = {}
proof
let V be non empty addLoopStr;
let M be empty Subset of V;
let N be Subset of V;
A1: M + N = {u + v where u,v is Element of V : u in {} & v in N} by
RUSUB_4:def 9;
for x being Element of V st x in M + N holds x in {}
proof
let x be Element of V;
assume x in M+N;
then ex u,v be Element of V st x = u + v & u in {} & v in N by A1;
hence thesis;
end;
then M + N c= {};
hence thesis;
end;
Lm9: for V being right_zeroed non empty addLoopStr, M being Subset of V
holds M + {0.V} = M
proof
let V be right_zeroed non empty addLoopStr;
let M be Subset of V;
for x being Element of V st x in M + {0.V} holds x in M
proof
let x be Element of V;
assume x in M + {0.V};
then x in {u + v where u,v is Element of V : u in M & v in {0.V}} by
RUSUB_4:def 9;
then consider u,v be Element of V such that
A1: x = u + v & u in M and
A2: v in {0.V};
v = 0.V by A2,TARSKI:def 1;
hence thesis by A1,RLVECT_1:def 4;
end;
then
A3: M + {0.V} c= M;
for x being Element of V st x in M holds x in M + {0.V}
proof
let x be Element of V;
A4: x = x + 0.V & 0.V in {0.V} by RLVECT_1:def 4,TARSKI:def 1;
assume x in M;
then x in {u + v where u,v is Element of V : u in M & v in {0.V}} by A4;
hence thesis by RUSUB_4:def 9;
end;
then M c= M + {0.V};
hence thesis by A3;
end;
Lm10: for V being RealLinearSpace, M being Subset of V,
r1,r2 being Real st r1
>= 0 & r2 >= 0 & M is convex holds r1*M + r2*M c= (r1 + r2)*M
proof
let V be RealLinearSpace;
let M be Subset of V;
let r1,r2 be Real;
assume that
A1: r1 >= 0 and
A2: r2 >= 0 and
A3: M is convex;
per cases;
suppose
M is empty;
then r1*M = {} & (r1+r2)*M = {} by Lm7;
hence thesis by Lm8;
end;
suppose
A4: M is non empty;
per cases;
suppose
A5: r1 = 0;
then r1*M = {0.V} by A4,Lm2;
hence thesis by A5,Lm9;
end;
suppose
A6: r2 = 0;
then r2*M = {0.V} by A4,Lm2;
hence thesis by A6,Lm9;
end;
suppose
A7: r1 <> 0 & r2 <> 0;
then r1 + r2 > r1 by A2,XREAL_1:29;
then
A8: r1/(r1+r2) < 1 by A1,XREAL_1:189;
0 < r1/(r1+r2) by A1,A2,A7,XREAL_1:139;
then r1/(r1+r2) * M + (1 - r1/(r1+r2)) * M c= M by A3,A8,Th4;
then
A9: (r1+r2)*(r1/(r1+r2)*M + (1-r1/(r1+r2))*M) c= (r1+r2)*M by Lm6;
1-r1/(r1+r2) = (r1+r2)/(r1+r2) - r1/(r1+r2) by A1,A2,A7,XCMPLX_1:60
.= (r1+r2-r1)/(r1+r2) by XCMPLX_1:120
.= r2/(r1+r2);
then
A10: (r1+r2)*((1-r1/(r1+r2))*M) = r2/(r1+r2)*(r1+r2)*M by Lm4
.= r2*M by A1,A2,A7,XCMPLX_1:87;
(r1+r2)*(r1/(r1+r2)*M) = (r1/(r1+r2))*(r1+r2)*M by Lm4
.= r1*M by A1,A2,A7,XCMPLX_1:87;
hence thesis by A9,A10,Lm5;
end;
end;
end;
theorem
for V being RealLinearSpace, M being Subset of V,
r1,r2 being Real st
r1 >= 0 & r2 >= 0 & M is convex holds r1*M + r2*M = (r1 + r2)*M
by Lm10,Th12;
theorem
for V being Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty
RLSStruct, M1,M2,M3 being Subset of V,
r1,r2,r3 being Real st M1 is convex &
M2 is convex & M3 is convex holds r1*M1 + r2*M2 + r3*M3 is convex
proof
let V be Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty RLSStruct;
let M1,M2,M3 be Subset of V;
let r1,r2,r3 be Real;
assume that
A1: M1 is convex & M2 is convex and
A2: M3 is convex;
r1*M1 + r2*M2 is convex by A1,Th11;
then 1*(r1*M1 + r2*M2) + r3*M3 is convex by A2,Th11;
hence thesis by Lm1;
end;
theorem Th15:
for V being non empty RLSStruct, F being Subset-Family of V st (
for M being Subset of V st M in F holds M is convex) holds meet F is convex
proof
let V be non empty RLSStruct;
let F be Subset-Family of V;
assume
A1: for M being Subset of V st M in F holds M is convex;
per cases;
suppose
F = {};
then meet F = {} by SETFAM_1:def 1;
hence thesis;
end;
suppose
A2: F <> {};
meet F is convex
proof
let u,v be VECTOR of V;
let r be Real;
assume that
A3: 0 < r & r < 1 and
A4: u in meet F and
A5: v in meet F;
for M being set st M in F holds r*u + (1-r)*v in M
proof
let M be set;
assume
A6: M in F;
then reconsider M as Subset of V;
A7: v in M by A5,A6,SETFAM_1:def 1;
M is convex & u in M by A1,A4,A6,SETFAM_1:def 1;
hence thesis by A3,A7;
end;
hence thesis by A2,SETFAM_1:def 1;
end;
hence thesis;
end;
end;
theorem Th16:
for V being non empty RLSStruct, M being Subset of V st M is
Affine holds M is convex
proof
let V be non empty RLSStruct;
let M be Subset of V;
assume
A1: M is Affine;
let u,v be VECTOR of V;
let r be Real;
assume that
0 < r and
r < 1 and
A2: u in M & v in M;
set p = 1-r;
1-p = r;
hence thesis by A1,A2,RUSUB_4:def 4;
end;
registration
let V be non empty RLSStruct;
cluster non empty convex for Subset of V;
existence
proof
set M = the non empty Affine Subset of V;
M is convex by Th16;
hence thesis;
end;
end;
registration
let V be non empty RLSStruct;
cluster empty convex for Subset of V;
existence
proof
{}V is convex;
hence thesis;
end;
end;
theorem
for V being RealUnitarySpace-like non empty UNITSTR, M being Subset
of V, v being VECTOR of V, r being Real
st M = {u where u is VECTOR of V : u .|. v >= r} holds M is convex
proof
let V be RealUnitarySpace-like non empty UNITSTR;
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : u.|.v >= r};
let x,y be VECTOR of V;
let p be Real;
assume that
A2: 0 < p and
A3: p < 1 and
A4: x in M and
A5: y in M;
0 + p < 1 by A3;
then
A6: 0 < 1-p by XREAL_1:20;
consider u2 be VECTOR of V such that
A7: y = u2 and
A8: u2.|.v >= r by A1,A5;
((1-p)*y).|.v = (1-p)*(u2.|.v) by A7,BHSP_1:def 2;
then
A9: ((1-p)*y).|.v >= (1-p)*r by A8,A6,XREAL_1:64;
consider u1 be VECTOR of V such that
A10: x = u1 and
A11: u1.|.v >= r by A1,A4;
(p*x).|.v = p*(u1.|.v) by A10,BHSP_1:def 2;
then
A12: (p*x).|.v >= p*r by A2,A11,XREAL_1:64;
(p*x + (1-p)*y).|.v = (p*x).|.v + ((1-p)*y).|.v by BHSP_1:def 2;
then (p*x + (1-p)*y).|.v >= p*r + (1-p)*r by A12,A9,XREAL_1:7;
hence thesis by A1;
end;
theorem
for V being RealUnitarySpace-like non empty UNITSTR, M being Subset
of V, v being VECTOR of V, r being Real
st M = {u where u is VECTOR of V : u .|. v > r} holds M is convex
proof
let V be RealUnitarySpace-like non empty UNITSTR;
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : u.|.v > r};
let x,y be VECTOR of V;
let p be Real;
assume that
A2: 0 < p and
A3: p < 1 and
A4: x in M and
A5: y in M;
0 + p < 1 by A3;
then
A6: 0 < 1-p by XREAL_1:20;
consider u2 be VECTOR of V such that
A7: y = u2 and
A8: u2.|.v > r by A1,A5;
((1-p)*y).|.v = (1-p)*(u2.|.v) by A7,BHSP_1:def 2;
then
A9: ((1-p)*y).|.v > (1-p)*r by A8,A6,XREAL_1:68;
consider u1 be VECTOR of V such that
A10: x = u1 and
A11: u1.|.v > r by A1,A4;
(p*x).|.v = p*(u1.|.v) by A10,BHSP_1:def 2;
then
A12: (p*x).|.v > p*r by A2,A11,XREAL_1:68;
(p*x + (1-p)*y).|.v = (p*x).|.v + ((1-p)*y).|.v by BHSP_1:def 2;
then (p*x + (1-p)*y).|.v > p*r + (1-p)*r by A12,A9,XREAL_1:8;
hence thesis by A1;
end;
theorem
for V being RealUnitarySpace-like non empty UNITSTR, M being Subset
of V, v being VECTOR of V, r being Real
st M = {u where u is VECTOR of V : u .|. v <= r} holds M is convex
proof
let V be RealUnitarySpace-like non empty UNITSTR;
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : u.|.v <= r};
let x,y be VECTOR of V;
let p be Real;
assume that
A2: 0 < p and
A3: p < 1 and
A4: x in M and
A5: y in M;
0 + p < 1 by A3;
then
A6: 0 < 1-p by XREAL_1:20;
consider u2 be VECTOR of V such that
A7: y = u2 and
A8: u2.|.v <= r by A1,A5;
((1-p)*y).|.v = (1-p)*(u2.|.v) by A7,BHSP_1:def 2;
then
A9: ((1-p)*y).|.v <= (1-p)*r by A8,A6,XREAL_1:64;
consider u1 be VECTOR of V such that
A10: x = u1 and
A11: u1.|.v <= r by A1,A4;
(p*x).|.v = p*(u1.|.v) by A10,BHSP_1:def 2;
then
A12: (p*x).|.v <= p*r by A2,A11,XREAL_1:64;
(p*x + (1-p)*y).|.v = (p*x).|.v + ((1-p)*y).|.v by BHSP_1:def 2;
then (p*x + (1-p)*y).|.v <= p*r + (1-p)*r by A12,A9,XREAL_1:7;
hence thesis by A1;
end;
theorem
for V being RealUnitarySpace-like non empty UNITSTR, M being Subset
of V, v being VECTOR of V, r being Real
st M = {u where u is VECTOR of V : u .|. v < r} holds M is convex
proof
let V be RealUnitarySpace-like non empty UNITSTR;
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : u.|.v < r};
let x,y be VECTOR of V;
let p be Real;
assume that
A2: 0 < p and
A3: p < 1 and
A4: x in M and
A5: y in M;
0 + p < 1 by A3;
then
A6: 0 < 1-p by XREAL_1:20;
consider u2 be VECTOR of V such that
A7: y = u2 and
A8: u2.|.v < r by A1,A5;
((1-p)*y).|.v = (1-p)*(u2.|.v) by A7,BHSP_1:def 2;
then
A9: ((1-p)*y).|.v < (1-p)*r by A8,A6,XREAL_1:68;
consider u1 be VECTOR of V such that
A10: x = u1 and
A11: u1.|.v < r by A1,A4;
(p*x).|.v = p*(u1.|.v) by A10,BHSP_1:def 2;
then
A12: (p*x).|.v < p*r by A2,A11,XREAL_1:68;
(p*x + (1-p)*y).|.v = (p*x).|.v + ((1-p)*y).|.v by BHSP_1:def 2;
then (p*x + (1-p)*y).|.v < p*r + (1-p)*r by A12,A9,XREAL_1:8;
hence thesis by A1;
end;
begin :: Convex Combinations
definition
let V be RealLinearSpace, L be Linear_Combination of V;
attr L is convex means
ex F being FinSequence of the carrier of V st
F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st len f =
len F & Sum(f) = 1 & for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >=
0;
end;
theorem Th21:
for V being RealLinearSpace, L being Linear_Combination of V st
L is convex holds Carrier(L) <> {}
proof
let V be RealLinearSpace;
let L be Linear_Combination of V;
assume L is convex;
then consider F being FinSequence of the carrier of V such that
A1: F is one-to-one & rng F = Carrier L and
A2: 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;
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;
assume Carrier(L) = {};
then len F = 0 by A1,CARD_1:27,FINSEQ_4:62;
then f = <*>REAL by A3;
hence contradiction by A3,RVSUM_1:72;
end;
theorem
for V being RealLinearSpace, L being Linear_Combination of V, v being
VECTOR of V st L is convex & L.v <= 0 holds not v in Carrier(L)
proof
let V be RealLinearSpace;
let L be Linear_Combination of V;
let v be VECTOR of V;
assume that
A1: L is convex and
A2: L.v <= 0;
per cases by A2;
suppose
L.v = 0;
hence thesis by RLVECT_2:19;
end;
suppose
A3: L.v < 0;
now
consider F being FinSequence of the carrier of V such that
F is one-to-one and
A4: rng F = Carrier L and
A5: 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 A1;
assume v in Carrier(L);
then consider n be object such that
A6: n in dom F and
A7: F.n = v by A4,FUNCT_1:def 3;
reconsider n as Element of NAT by A6;
consider f being FinSequence of REAL such that
A8: len f = len F and
Sum(f) = 1 and
A9: for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A5;
n in Seg len F by A6,FINSEQ_1:def 3;
then
A10: n in dom f by A8,FINSEQ_1:def 3;
then L.v = f.n by A9,A7;
hence contradiction by A3,A9,A10;
end;
hence thesis;
end;
end;
theorem
for V being RealLinearSpace, L being Linear_Combination of V st L is
convex holds L <> ZeroLC(V)
by Th21,RLVECT_2:def 5;
Lm11: for V being RealLinearSpace, v being VECTOR of V, L being
Linear_Combination of V st L is convex & Carrier(L) = {v} holds L.v = 1 & Sum(L
) = L.v * v
proof
let V be RealLinearSpace;
let v be VECTOR of V;
let L be Linear_Combination of V;
assume that
A1: L is convex and
A2: Carrier(L) = {v};
reconsider L as Linear_Combination of {v} by A2,RLVECT_2:def 6;
consider F being FinSequence of the carrier of V such that
A3: F is one-to-one & rng F = Carrier L and
A4: 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 A1;
A5: F = <*v*> by A2,A3,FINSEQ_3:97;
consider f be FinSequence of REAL such that
A6: len f = len F and
A7: Sum(f) = 1 and
A8: for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A4;
reconsider r = f/.1 as Element of REAL;
card Carrier(L) = 1 by A2,CARD_1:30;
then len F = 1 by A3,FINSEQ_4:62;
then
A9: dom f = Seg 1 by A6,FINSEQ_1:def 3;
then
A10: 1 in dom f by FINSEQ_1:2,TARSKI:def 1;
then
A11: f.1 = f/.1 by PARTFUN1:def 6;
then f = <* r *> by A9,FINSEQ_1:def 8;
then
A12: Sum f = r by FINSOP_1:11;
f.1 = L.(F.1) by A8,A10;
hence thesis by A7,A11,A12,A5,RLVECT_2:32;
end;
Lm12: for V being RealLinearSpace, v1,v2 being VECTOR of V, L being
Linear_Combination of V st L is convex & Carrier(L) = {v1,v2} & v1 <> v2 holds
L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 & Sum(L) = L.v1 * v1 + L.v2 * v2
proof
let V be RealLinearSpace;
let v1,v2 be VECTOR of V;
let L be Linear_Combination of V;
assume that
A1: L is convex and
A2: Carrier(L) = {v1,v2} and
A3: v1 <> v2;
reconsider L as Linear_Combination of {v1,v2} by A2,RLVECT_2:def 6;
consider F being FinSequence of the carrier of V such that
A4: F is one-to-one & rng F = Carrier L and
A5: 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 A1;
consider f be FinSequence of REAL such that
A6: len f = len F and
A7: Sum(f) = 1 and
A8: for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A5;
len F = card {v1,v2} by A2,A4,FINSEQ_4:62;
then
A9: len f = 2 by A3,A6,CARD_2:57;
then
A10: dom f = {1,2} by FINSEQ_1:2,def 3;
then
A11: 1 in dom f by TARSKI:def 2;
then
A12: f.1 = L.(F.1) by A8;
then f/.1 = L.(F.1) by A11,PARTFUN1:def 6;
then reconsider r1 = L.(F.1) as Element of REAL;
A13: 2 in dom f by A10,TARSKI:def 2;
then
A14: f.2 = L.(F.2) by A8;
then f/.2 = L.(F.2) by A13,PARTFUN1:def 6;
then reconsider r2 = L.(F.2) as Element of REAL;
A15: f = <*r1,r2*> by A9,A12,A14,FINSEQ_1:44;
now
per cases by A2,A3,A4,FINSEQ_3:99;
suppose
F = <*v1,v2*>;
then F.1 = v1 & F.2 = v2;
hence L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 by A7,A8,A11,A13,A12,A14
,A15,RVSUM_1:77;
end;
suppose
F = <*v2,v1*>;
then F.1 = v2 & F.2 = v1;
hence L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 by A7,A8,A11,A13,A12,A14
,A15,RVSUM_1:77;
end;
end;
hence thesis by A3,RLVECT_2:33;
end;
Lm13: for p being FinSequence, x,y,z being object st
p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x holds
p = <* x,y,z *> or p = <* x,z,y *> or p = <* y,x,z *> or
p = <* y,z,x *> or p = <* z,x,y *> or p = <* z,y,x *>
proof
let p be FinSequence;
let x,y,z be object;
assume that
A1: p is one-to-one and
A2: rng p = {x,y,z} and
A3: x <> y & y <> z & z <> x;
A4: len p = 3 by A1,A2,A3,FINSEQ_3:101;
then
A5: dom p = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
then
A6: 2 in dom p by ENUMSET1:def 1;
then
A7: p.2 in rng p by FUNCT_1:def 3;
A8: 3 in dom p by A5,ENUMSET1:def 1;
then
A9: p.3 in rng p by FUNCT_1:def 3;
A10: 1 in dom p by A5,ENUMSET1:def 1;
then p.1 in rng p by FUNCT_1:def 3;
then
p.1 = x & p.2 = x & p.3 = x or p.1 = x & p.2 = x & p.3 = y or p.1 = x &
p.2 = x & p.3 = z or p.1 = x & p.2 = y & p.3 = x or p.1 = x & p.2 = y & p.3 = y
or p.1 = x & p.2 = y & p.3 = z or p.1 = x & p.2 = z & p.3 = x or p.1 = x & p.2
= z & p.3 = y or p.1 = x & p.2 = z & p.3 = z or p.1 = y & p.2 = x & p.3 = x or
p.1 = y & p.2 = x & p.3 = y or p.1 = y & p.2 = x & p.3 = z or p.1 = y & p.2 = y
& p.3 = x or p.1 = y & p.2 = y & p.3 = y or p.1 = y & p.2 = y & p.3 = z or p.1
= y & p.2 = z & p.3 = x or p.1 = y & p.2 = z & p.3 = y or p.1 = y & p.2 = z & p
.3 = z or p.1 = z & p.2 = x & p.3 = x or p.1 = z & p.2 = x & p.3 = y or p.1 = z
& p.2 = x & p.3 = z or p.1 = z & p.2 = y & p.3 = x or p.1 = z & p.2 = y & p.3 =
y or p.1 = z & p.2 = y & p.3 = z or p.1 = z & p.2 = z & p.3 = x or p.1 = z & p.
2 = z & p.3 = y or p.1 = z & p.2 = z & p.3 = z by A2,A7,A9,ENUMSET1:def 1;
hence thesis by A1,A4,A10,A6,A8,FINSEQ_1:45,FUNCT_1:def 4;
end;
Lm14: for V being RealLinearSpace, v1,v2,v3 being VECTOR of V, L being
Linear_Combination of {v1,v2,v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 holds Sum(L)
= L.v1 * v1 + L.v2 * v2 + L.v3 * v3
proof
let V be RealLinearSpace;
let v1,v2,v3 be VECTOR of V;
let L be Linear_Combination of {v1,v2,v3};
assume that
A1: v1 <> v2 and
A2: v2 <> v3 and
A3: v3 <> v1;
A4: Carrier(L) c= {v1,v2,v3} by RLVECT_2:def 6;
per cases by A4,ZFMISC_1:118;
suppose
Carrier(L) = {};
then
A5: L = ZeroLC(V) by RLVECT_2:def 5;
then Sum(L) = 0.V by RLVECT_2:30
.= 0.V + 0.V
.= 0.V + 0.V + 0.V
.= 0 * v1 + 0.V + 0.V by RLVECT_1:10
.= 0 * v1 + 0 * v2 + 0.V by RLVECT_1:10
.= 0 * v1 + 0 * v2 + 0 * v3 by RLVECT_1:10
.= L.v1 * v1 + 0 * v2 + 0 * v3 by A5,RLVECT_2:20
.= L.v1 * v1 + L.v2 * v2 + 0 * v3 by A5,RLVECT_2:20
.= L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by A5,RLVECT_2:20;
hence thesis;
end;
suppose
A6: Carrier(L) = {v1};
then reconsider L as Linear_Combination of {v1} by RLVECT_2:def 6;
A7: not v2 in Carrier(L) by A1,A6,TARSKI:def 1;
A8: not v3 in Carrier(L) by A3,A6,TARSKI:def 1;
Sum(L) = L.v1 * v1 by RLVECT_2:32
.= L.v1 * v1 + 0.V
.= L.v1 * v1 + 0.V + 0.V
.= L.v1 * v1 + 0 * v2 + 0.V by RLVECT_1:10
.= L.v1 * v1 + 0 * v2 + 0 * v3 by RLVECT_1:10
.= L.v1 * v1 + L.v2 * v2 + 0 * v3 by A7,RLVECT_2:19
.= L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by A8,RLVECT_2:19;
hence thesis;
end;
suppose
A9: Carrier(L) = {v2};
then reconsider L as Linear_Combination of {v2} by RLVECT_2:def 6;
A10: not v1 in Carrier(L) by A1,A9,TARSKI:def 1;
A11: not v3 in Carrier(L) by A2,A9,TARSKI:def 1;
Sum(L) = L.v2 * v2 by RLVECT_2:32
.= 0.V + L.v2 * v2
.= 0.V + L.v2 * v2 + 0.V
.= 0 * v1 + L.v2 * v2 + 0.V by RLVECT_1:10
.= 0 * v1 + L.v2 * v2 + 0 * v3 by RLVECT_1:10
.= L.v1 * v1 + L.v2 * v2 + 0 * v3 by A10,RLVECT_2:19
.= L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by A11,RLVECT_2:19;
hence thesis;
end;
suppose
A12: Carrier(L) = {v3};
then reconsider L as Linear_Combination of {v3} by RLVECT_2:def 6;
A13: not v1 in Carrier(L) by A3,A12,TARSKI:def 1;
A14: not v2 in Carrier(L) by A2,A12,TARSKI:def 1;
Sum(L) = L.v3 * v3 by RLVECT_2:32
.= 0.V + L.v3 * v3
.= 0.V + 0.V + L.v3 * v3
.= 0 * v1 + 0.V + L.v3 * v3 by RLVECT_1:10
.= 0 * v1 + 0 * v2 + L.v3 * v3 by RLVECT_1:10
.= L.v1 * v1 + 0 * v2 + L.v3 * v3 by A13,RLVECT_2:19
.= L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by A14,RLVECT_2:19;
hence thesis;
end;
suppose
A15: Carrier(L) = {v1,v2};
then
A16: Sum(L) = L.v1 * v1 + L.v2 * v2 by A1,RLVECT_2:36
.= L.v1 * v1 + L.v2 * v2 + 0.V
.= L.v1 * v1 + L.v2 * v2 + 0 * v3 by RLVECT_1:10;
not v3 in Carrier(L) by A2,A3,A15,TARSKI:def 2;
hence thesis by A16,RLVECT_2:19;
end;
suppose
A17: Carrier(L) = {v1,v3};
then
A18: Sum(L) = L.v1 * v1 + L.v3 * v3 by A3,RLVECT_2:36
.= L.v1 * v1 + 0.V + L.v3 * v3
.= L.v1 * v1 + 0 * v2 + L.v3 * v3 by RLVECT_1:10;
not v2 in Carrier(L) by A1,A2,A17,TARSKI:def 2;
hence thesis by A18,RLVECT_2:19;
end;
suppose
A19: Carrier(L) = {v2,v3};
then
A20: Sum(L) = L.v2 * v2 + L.v3 * v3 by A2,RLVECT_2:36
.= 0.V + L.v2 * v2 + L.v3 * v3
.= 0 * v1 + L.v2 * v2 + L.v3 * v3 by RLVECT_1:10;
not v1 in Carrier(L) by A1,A3,A19,TARSKI:def 2;
hence thesis by A20,RLVECT_2:19;
end;
suppose
Carrier(L) = {v1,v2,v3};
then consider F be FinSequence of the carrier of V such that
A21: F is one-to-one & rng F = {v1,v2,v3} and
A22: Sum(L) = Sum(L (#) F) by RLVECT_2:def 8;
F = <* v1,v2,v3 *> or F = <* v1,v3,v2 *> or F = <* v2,v1,v3 *> or F =
<* v2,v3,v1 *> or F = <* v3,v1,v2 *> or F = <* v3,v2,v1 *> by A1,A2,A3,A21,Lm13
;
then L (#) F = <* L.v1 * v1, L.v2 * v2, L.v3 * v3 *> or L (#) F = <* L.v1
* v1, L.v3 * v3, L.v2 * v2 *> or L (#) F = <* L.v2 * v2, L.v1 * v1, L.v3 * v3
*> or L (#) F = <* L.v2 * v2, L.v3 * v3, L.v1 * v1 *> or L (#) F = <* L.v3 * v3
, L.v1 * v1, L.v2 * v2 *> or L (#) F = <* L.v3 * v3, L.v2 * v2, L.v1 * v1 *>
by RLVECT_2:28;
then
Sum(L) = L.v1 * v1 + L.v2 * v2 + L.v3 * v3 or Sum(L) = L.v1 * v1 + (L
.v2 * v2 + L.v3 * v3) or Sum(L) = L.v2 * v2 + (L.v1 * v1 + L.v3 * v3) by A22,
RLVECT_1:46;
hence thesis by RLVECT_1:def 3;
end;
end;
Lm15: for V being RealLinearSpace, v1,v2,v3 being VECTOR of V, L being
Linear_Combination of V st L is convex & Carrier(L) = {v1,v2,v3} & v1 <> v2 &
v2 <> v3 & v3 <> v1 holds L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3
>= 0 & Sum(L) = L.v1 * v1 + L.v2 * v2 + L.v3 * v3
proof
let V be RealLinearSpace;
let v1,v2,v3 be VECTOR of V;
let L be Linear_Combination of V;
assume that
A1: L is convex and
A2: Carrier(L) = {v1,v2,v3} and
A3: v1 <> v2 & v2 <> v3 & v3 <> v1;
reconsider L as Linear_Combination of {v1,v2,v3} by A2,RLVECT_2:def 6;
consider F being FinSequence of the carrier of V such that
A4: F is one-to-one & rng F = Carrier L and
A5: 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 A1;
consider f be FinSequence of REAL such that
A6: len f = len F and
A7: Sum(f) = 1 and
A8: for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A5;
len F = card {v1,v2,v3} by A2,A4,FINSEQ_4:62;
then
A9: len f = 3 by A3,A6,CARD_2:58;
then
A10: dom f = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
then
A11: 1 in dom f by ENUMSET1:def 1;
then
A12: f.1 = L.(F.1) by A8;
then f/.1 = L.(F.1) by A11,PARTFUN1:def 6;
then reconsider r1 = L.(F.1) as Element of REAL;
A13: 3 in dom f by A10,ENUMSET1:def 1;
then
A14: f.3 = L.(F.3) by A8;
then f/.3 = L.(F.3) by A13,PARTFUN1:def 6;
then reconsider r3 = L.(F.3) as Element of REAL;
A15: 2 in dom f by A10,ENUMSET1:def 1;
then
A16: f.2 = L.(F.2) by A8;
then f/.2 = L.(F.2) by A15,PARTFUN1:def 6;
then reconsider r2 = L.(F.2) as Element of REAL;
A17: f = <*r1,r2,r3*> by A9,A12,A16,A14,FINSEQ_1:45;
then
A18: L.(F.1) + L.(F.2) + L.(F.3) = 1 by A7,RVSUM_1:78;
now
per cases by A2,A3,A4,Lm13;
suppose
A19: F = <*v1,v2,v3*>;
then
A20: F.3 = v3;
F.1 = v1 & F.2 = v2 by A19;
hence L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 by A7,A8
,A11,A15,A13,A12,A16,A14,A17,A20,RVSUM_1:78;
end;
suppose
A21: F = <*v1,v3,v2*>;
then
A22: F.3 = v2;
F.1 = v1 & F.2 = v3 by A21;
hence L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 by A8
,A11,A15,A13,A12,A16,A14,A18,A22;
end;
suppose
A23: F = <*v2,v1,v3*>;
then
A24: F.3 = v3;
F.1 = v2 & F.2 = v1 by A23;
hence L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 by A7,A8
,A11,A15,A13,A12,A16,A14,A17,A24,RVSUM_1:78;
end;
suppose
A25: F = <*v2,v3,v1*>;
then
A26: F.3 = v1;
F.1 = v2 & F.2 = v3 by A25;
hence L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 by A8
,A11,A15,A13,A12,A16,A14,A18,A26;
end;
suppose
A27: F = <*v3,v1,v2*>;
then
A28: F.3 = v2;
F.1 = v3 & F.2 = v1 by A27;
hence L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 by A8
,A11,A15,A13,A12,A16,A14,A18,A28;
end;
suppose
A29: F = <*v3,v2,v1*>;
then
A30: F.3 = v1;
F.1 = v3 & F.2 = v2 by A29;
hence L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 by A8
,A11,A15,A13,A12,A16,A14,A18,A30;
end;
end;
hence thesis by A3,Lm14;
end;
theorem
for V being RealLinearSpace, v being VECTOR of V, L being
Linear_Combination of {v} st L is convex holds L.v = 1 & Sum(L) = L.v * v
proof
let V be RealLinearSpace;
let v be VECTOR of V;
let L be Linear_Combination of {v};
Carrier(L) c= {v} by RLVECT_2:def 6;
then
A1: Carrier(L) = {} or Carrier(L) = {v} by ZFMISC_1:33;
assume L is convex;
hence thesis by A1,Lm11,Th21;
end;
theorem
for V being RealLinearSpace, v1,v2 being VECTOR of V, L being
Linear_Combination of {v1,v2} st v1 <> v2 & L is convex holds L.v1 + L.v2 = 1 &
L.v1 >= 0 & L.v2 >= 0 & Sum(L) = L.v1 * v1 + L.v2 * v2
proof
let V be RealLinearSpace;
let v1,v2 be VECTOR of V;
let L be Linear_Combination of {v1,v2};
assume that
A1: v1 <> v2 and
A2: L is convex;
A3: Carrier(L) c= {v1,v2} & Carrier(L) <> {} by A2,Th21,RLVECT_2:def 6;
now
per cases by A3,ZFMISC_1:36;
suppose
A4: Carrier(L) = {v1};
then not v2 in Carrier(L) by A1,TARSKI:def 1;
then not v2 in {v where v is Element of V : L.v <> 0} by RLVECT_2:def 4;
then L.v2 = 0;
hence L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 by A2,A4,Lm11;
end;
suppose
A5: Carrier(L) = {v2};
then not v1 in Carrier(L) by A1,TARSKI:def 1;
then not v1 in {v where v is Element of V : L.v <> 0} by RLVECT_2:def 4;
then L.v1 = 0;
hence L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 by A2,A5,Lm11;
end;
suppose
Carrier(L) = {v1,v2};
hence L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 by A1,A2,Lm12;
end;
end;
hence thesis by A1,RLVECT_2:33;
end;
theorem
for V being RealLinearSpace, v1,v2,v3 being VECTOR of V, L being
Linear_Combination of {v1,v2,v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 & L is
convex holds L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 & Sum(L
) = L.v1 * v1 + L.v2 * v2 + L.v3 * v3
proof
let V be RealLinearSpace, v1,v2,v3 be VECTOR of V, L be Linear_Combination
of {v1,v2,v3};
assume that
A1: v1 <> v2 and
A2: v2 <> v3 and
A3: v3 <> v1 and
A4: L is convex;
A5: Carrier(L) c= {v1,v2,v3} & Carrier(L) <> {} by A4,Th21,RLVECT_2:def 6;
now
per cases by A5,ZFMISC_1:118;
suppose
A6: Carrier(L) = {v1};
then not v3 in Carrier(L) by A3,TARSKI:def 1;
then not v3 in {v where v is Element of V : L.v <> 0} by RLVECT_2:def 4;
then
A7: L.v3 = 0;
not v2 in Carrier(L) by A1,A6,TARSKI:def 1;
then not v2 in {v where v is Element of V : L.v <> 0} by RLVECT_2:def 4;
then L.v2 = 0;
hence
L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 by A4,A6,A7
,Lm11;
end;
suppose
A8: Carrier(L) = {v2};
then not v3 in Carrier(L) by A2,TARSKI:def 1;
then not v3 in {v where v is Element of V : L.v <> 0} by RLVECT_2:def 4;
then
A9: L.v3 = 0;
not v1 in Carrier(L) by A1,A8,TARSKI:def 1;
then not v1 in {v where v is Element of V : L.v <> 0} by RLVECT_2:def 4;
then L.v1 = 0;
hence L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 by A4,A8
,A9,Lm11;
end;
suppose
A10: Carrier(L) = {v3};
then not v2 in Carrier(L) by A2,TARSKI:def 1;
then not v2 in {v where v is Element of V : L.v <> 0} by RLVECT_2:def 4;
then
A11: L.v2 = 0;
not v1 in Carrier(L) by A3,A10,TARSKI:def 1;
then not v1 in {v where v is Element of V : L.v <> 0} by RLVECT_2:def 4;
then L.v1 = 0;
hence L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 by A4
,A10,A11,Lm11;
end;
suppose
A12: Carrier(L) = {v1,v2};
then not v3 in Carrier(L) by A2,A3,TARSKI:def 2;
then not v3 in {v where v is Element of V : L.v <> 0} by RLVECT_2:def 4;
then L.v3 = 0;
hence
L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 by A1,A4,A12
,Lm12;
end;
suppose
A13: Carrier(L) = {v2,v3};
then not v1 in Carrier(L) by A1,A3,TARSKI:def 2;
then not v1 in {v where v is Element of V : L.v <> 0} by RLVECT_2:def 4;
then L.v1 = 0;
hence
L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 by A2,A4,A13
,Lm12;
end;
suppose
A14: Carrier(L) = {v1,v3};
then not v2 in Carrier(L) by A1,A2,TARSKI:def 2;
then not v2 in {v where v is Element of V : L.v <> 0} by RLVECT_2:def 4;
then L.v2 = 0;
hence
L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 by A3,A4,A14
,Lm12;
end;
suppose
Carrier(L) = {v1,v2,v3};
hence
L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 by A1,A2,A3,A4
,Lm15;
end;
end;
hence thesis by A1,A2,A3,Lm14;
end;
theorem
for V being RealLinearSpace, v being VECTOR of V, L being
Linear_Combination of V st L is convex & Carrier(L) = {v} holds L.v = 1 by Lm11
;
theorem
for V being RealLinearSpace, v1,v2 being VECTOR of V, L being
Linear_Combination of V st L is convex & Carrier(L) = {v1,v2} & v1 <> v2 holds
L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 by Lm12;
theorem
for V being RealLinearSpace, v1,v2,v3 being VECTOR of V, L being
Linear_Combination of V st L is convex & Carrier(L) = {v1,v2,v3} & v1 <> v2 &
v2 <> v3 & v3 <> v1 holds L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3
>= 0 & Sum(L) = L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by Lm15;
begin :: Convex Hull
definition
let V be non empty RLSStruct, M be Subset of V;
func Convex-Family M -> Subset-Family of V means
:Def4:
for N being Subset of V holds N in it iff N is convex & M c= N;
existence
proof
defpred P[Subset of V] means $1 is convex & M c= $1;
thus ex F be Subset-Family of V st for N being Subset of V holds N in F
iff P[N] from SUBSET_1:sch 3;
end;
uniqueness
proof
let SF,SG be Subset-Family of V;
assume that
A1: for N being Subset of V holds N in SF iff N is convex & M c= N and
A2: for N being Subset of V holds N in SG iff N is convex & M c= N;
for Y being Subset of V holds Y in SF iff Y in SG
proof
let Y be Subset of V;
hereby
assume Y in SF;
then Y is convex & M c= Y by A1;
hence Y in SG by A2;
end;
assume Y in SG;
then Y is convex & M c= Y by A2;
hence thesis by A1;
end;
hence thesis by SETFAM_1:31;
end;
end;
definition
let V be non empty RLSStruct, M be Subset of V;
func conv(M) -> convex Subset of V equals
meet (Convex-Family M);
coherence
proof
for N being Subset of V st N in Convex-Family M holds N is convex by Def4;
hence thesis by Th15;
end;
end;
theorem
for V being non empty RLSStruct, M being Subset of V, N being convex
Subset of V st M c= N holds conv(M) c= N
proof
let V be non empty RLSStruct;
let M be Subset of V;
let N be convex Subset of V;
assume M c= N;
then N in Convex-Family M by Def4;
hence thesis by SETFAM_1:3;
end;
begin :: Miscellaneous
theorem
for p being FinSequence, x,y,z being object st
p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x holds
p = <* x,y,z *> or p = <* x,z,y *> or p = <* y,x,z *> or
p = <* y,z,x *> or p = <* z,x,y *> or p = <* z,y,x *> by Lm13;
theorem
for V being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct, M being Subset
of V holds 1*M = M by Lm1;
theorem
for V being non empty RLSStruct, M being empty Subset of V, r being
Real holds r * M = {} by Lm7;
theorem
for V being RealLinearSpace, M be non empty Subset of V holds 0 * M =
{0.V} by Lm2;
theorem
for V being right_zeroed non empty addLoopStr, M being Subset of V
holds M + {0.V} = M by Lm9;
theorem
for V be add-associative non empty addLoopStr, M1,M2,M3 be Subset of
V holds (M1 + M2) + M3 = M1 + (M2 + M3) by Lm3;
theorem
for V being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct, M being Subset
of V, r1,r2 being Real holds r1*(r2*M) = (r1*r2)*M by Lm4;
theorem
for V being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct, M1,M2 being
Subset of V, r being Real holds r*(M1 + M2) = r*M1 + r*M2 by Lm5;
theorem
for V being non empty RLSStruct, M,N being Subset of V,
r being Real
st M c= N holds r*M c= r*N by Lm6;
theorem
for V being non empty addLoopStr, M being empty Subset of V, N being
Subset of V holds M + N = {} by Lm8;
begin ::Addenda
:: from CONVEX2, 2008.07.07, A.T.
registration
let V be non empty RLSStruct, M,N be convex Subset of V;
cluster M /\ N -> convex for Subset of V;
coherence
proof
now
let x,y be VECTOR of V;
let r be Real;
assume that
A1: 0 < r & r < 1 and
A2: x in M /\ N & y in M /\ N;
x in N & y in N by A2,XBOOLE_0:def 4;
then
A3: r * x + (1-r) * y in N by A1,Def2;
x in M & y in M by A2,XBOOLE_0:def 4;
then r * x + (1-r) * y in M by A1,Def2;
hence r*x + (1-r)*y in M /\ N by A3,XBOOLE_0:def 4;
end;
hence thesis;
end;
end;
registration
let V be RealLinearSpace, M be Subset of V;
cluster Convex-Family M -> non empty;
coherence
proof
A1: M c= Up((Omega).V)
proof
let x be object;
assume x in M;
then reconsider x as Element of V;
x in the carrier of (the RLSStruct of V);
then x in the carrier of (Omega).V by RLSUB_1:def 4;
hence thesis by RUSUB_4:def 5;
end;
Up((Omega).V) is convex by Th9;
hence thesis by A1,Def4;
end;
end;
theorem
for V being RealLinearSpace, M being Subset of V holds M c= conv(M)
proof
let V be RealLinearSpace;
let M be Subset of V;
let v be object;
assume
A1: v in M;
for Y being set holds Y in Convex-Family M implies v in Y
proof
let Y be set;
assume
A2: Y in Convex-Family M;
then reconsider Y as Subset of V;
M c= Y by A2,Def4;
hence thesis by A1;
end;
hence thesis by SETFAM_1:def 1;
end;