:: CONVEX1 semantic presentation
begin
definition
let V be non empty RLSStruct ;
let M be Subset of V;
let r be Real;
funcr * M -> Subset of V equals :: CONVEX1:def 1
{ (r * v) where v is Element of V : v in M } ;
coherence
{ (r * v) where v is Element of V : v in M } is Subset of V
proof
deffunc H1( Element of V) -> Element of the carrier of V = r * $1;
defpred S1[ set ] means $1 in M;
{ H1(v) where v is Element of V : S1[v] } is Subset of V from DOMAIN_1:sch_8();
hence { (r * v) where v is Element of V : v in M } is Subset of V ; ::_thesis: verum
end;
end;
:: deftheorem defines * CONVEX1:def_1_:_
for V being non empty RLSStruct
for M being Subset of V
for r being Real holds r * M = { (r * v) where v is Element of V : v in M } ;
definition
let V be non empty RLSStruct ;
let M be Subset of V;
attrM is convex means :Def2: :: CONVEX1:def 2
for u, v being VECTOR of V
for r being Real st 0 < r & r < 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M;
end;
:: deftheorem Def2 defines convex CONVEX1:def_2_:_
for V being non empty RLSStruct
for M being Subset of V holds
( M is convex iff for u, v being VECTOR of V
for r being Real st 0 < r & r < 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M );
theorem :: CONVEX1:1
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V
for r being Real st M is convex holds
r * M is convex
proof
let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M being Subset of V
for r being Real st M is convex holds
r * M is convex
let M be Subset of V; ::_thesis: for r being Real st M is convex holds
r * M is convex
let r be Real; ::_thesis: ( M is convex implies r * M is convex )
assume A1: M is convex ; ::_thesis: r * M is convex
for u, v being VECTOR of V
for 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; ::_thesis: for 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
let p be Real; ::_thesis: ( 0 < p & p < 1 & u in r * M & v in r * M implies (p * u) + ((1 - p) * v) in r * M )
assume that
A2: ( 0 < p & p < 1 ) and
A3: u in r * M and
A4: v in r * M ; ::_thesis: (p * u) + ((1 - p) * v) in r * M
consider v9 being Element of V such that
A5: v = r * v9 and
A6: v9 in M by A4;
consider u9 being 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, Def2;
hence (p * u) + ((1 - p) * v) in r * M by A9; ::_thesis: verum
end;
hence r * M is convex by Def2; ::_thesis: verum
end;
theorem :: CONVEX1:2
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M, N being Subset of V st M is convex & N is convex holds
M + N is convex
proof
let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M, N being Subset of V st M is convex & N is convex holds
M + N is convex
let M, N be Subset of V; ::_thesis: ( M is convex & N is convex implies M + N is convex )
assume A1: ( M is convex & N is convex ) ; ::_thesis: M + N is convex
for u, v being VECTOR of V
for 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; ::_thesis: for 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
let r be Real; ::_thesis: ( 0 < r & r < 1 & u in M + N & v in M + N implies (r * u) + ((1 - r) * v) in M + N )
assume that
A2: ( 0 < r & r < 1 ) and
A3: u in M + N and
A4: v in M + N ; ::_thesis: (r * u) + ((1 - r) * 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, Def2;
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 (r * u) + ((1 - r) * v) in M + N by RUSUB_4:def_9; ::_thesis: verum
end;
hence M + N is convex by Def2; ::_thesis: verum
end;
theorem :: CONVEX1:3
for V being RealLinearSpace
for M, N being Subset of V st M is convex & N is convex holds
M - N is convex
proof
let V be RealLinearSpace; ::_thesis: for M, N being Subset of V st M is convex & N is convex holds
M - N is convex
let M, N be Subset of V; ::_thesis: ( M is convex & N is convex implies M - N is convex )
assume A1: ( M is convex & N is convex ) ; ::_thesis: M - N is convex
for u, v being VECTOR of V
for 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; ::_thesis: for 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
let r be Real; ::_thesis: ( 0 < r & r < 1 & u in M - N & v in M - N implies (r * u) + ((1 - r) * v) in M - N )
assume that
A2: ( 0 < r & r < 1 ) and
A3: u in M - N and
A4: v in M - N ; ::_thesis: (r * u) + ((1 - r) * 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, Def2;
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 (r * u) + ((1 - r) * v) in M - N by RUSUB_5:def_2; ::_thesis: verum
end;
hence M - N is convex by Def2; ::_thesis: verum
end;
theorem Th4: :: CONVEX1:4
for V being non empty RLSStruct
for 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 ; ::_thesis: for 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 )
let M be Subset of V; ::_thesis: ( M is convex iff for r being Real st 0 < r & r < 1 holds
(r * M) + ((1 - r) * M) c= M )
A1: ( M is convex implies for r being Real st 0 < r & r < 1 holds
(r * M) + ((1 - r) * M) c= M )
proof
assume A2: M is convex ; ::_thesis: for r being Real st 0 < r & r < 1 holds
(r * M) + ((1 - r) * M) c= M
let r be Real; ::_thesis: ( 0 < r & r < 1 implies (r * M) + ((1 - r) * M) c= M )
assume A3: ( 0 < r & r < 1 ) ; ::_thesis: (r * M) + ((1 - r) * M) c= M
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; ::_thesis: ( x in (r * M) + ((1 - r) * M) implies x in M )
assume x in (r * M) + ((1 - r) * M) ; ::_thesis: x in 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 being Element of V such that
A4: x = u + v and
A5: ( u in r * M & v in (1 - r) * M ) ;
( ex w1 being Element of V st
( u = r * w1 & w1 in M ) & ex w2 being Element of V st
( v = (1 - r) * w2 & w2 in M ) ) by A5;
hence x in M by A2, A3, A4, Def2; ::_thesis: verum
end;
hence (r * M) + ((1 - r) * M) c= M by SUBSET_1:2; ::_thesis: verum
end;
( ( for r being Real st 0 < r & r < 1 holds
(r * M) + ((1 - r) * M) c= M ) implies M is convex )
proof
assume A6: for r being Real st 0 < r & r < 1 holds
(r * M) + ((1 - r) * M) c= M ; ::_thesis: M is convex
let u, v be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M
let r be Real; ::_thesis: ( 0 < r & r < 1 & u in M & v in M implies (r * u) + ((1 - r) * v) in M )
assume ( 0 < r & r < 1 ) ; ::_thesis: ( not u in M or not v in M or (r * u) + ((1 - r) * v) in M )
then A7: (r * M) + ((1 - r) * M) c= M by A6;
assume ( u in M & v in M ) ; ::_thesis: (r * u) + ((1 - r) * 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 (r * u) + ((1 - r) * v) in M by A7; ::_thesis: verum
end;
hence ( M is convex iff for r being Real st 0 < r & r < 1 holds
(r * M) + ((1 - r) * M) c= M ) by A1; ::_thesis: verum
end;
theorem :: CONVEX1:5
for V being non empty Abelian RLSStruct
for M being Subset of V st M is convex holds
for r being Real st 0 < r & r < 1 holds
((1 - r) * M) + (r * M) c= M
proof
let V be non empty Abelian RLSStruct ; ::_thesis: for M being Subset of V st M is convex holds
for r being Real st 0 < r & r < 1 holds
((1 - r) * M) + (r * M) c= M
let M be Subset of V; ::_thesis: ( M is convex implies for r being Real st 0 < r & r < 1 holds
((1 - r) * M) + (r * M) c= M )
assume A1: M is convex ; ::_thesis: for r being Real st 0 < r & r < 1 holds
((1 - r) * M) + (r * M) c= M
let r be Real; ::_thesis: ( 0 < r & r < 1 implies ((1 - r) * M) + (r * M) c= M )
assume A2: ( 0 < r & r < 1 ) ; ::_thesis: ((1 - r) * M) + (r * M) c= M
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; ::_thesis: ( x in ((1 - r) * M) + (r * M) implies x in M )
assume x in ((1 - r) * M) + (r * M) ; ::_thesis: x in 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 being Element of V such that
A3: x = u + v and
A4: ( u in (1 - r) * M & v in r * M ) ;
( ex w1 being Element of V st
( u = (1 - r) * w1 & w1 in M ) & ex w2 being Element of V st
( v = r * w2 & w2 in M ) ) by A4;
hence x in M by A1, A2, A3, Def2; ::_thesis: verum
end;
hence ((1 - r) * M) + (r * M) c= M by SUBSET_1:2; ::_thesis: verum
end;
theorem :: CONVEX1:6
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for 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 non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for 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
let M, N be Subset of V; ::_thesis: ( M is convex & N is convex implies for r being Real holds (r * M) + ((1 - r) * N) is convex )
assume that
A1: M is convex and
A2: N is convex ; ::_thesis: for r being Real holds (r * M) + ((1 - r) * N) is convex
let r be Real; ::_thesis: (r * M) + ((1 - r) * N) is convex
let u, v be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & u in (r * M) + ((1 - r) * N) & v in (r * M) + ((1 - r) * N) holds
(r * u) + ((1 - r) * v) in (r * M) + ((1 - r) * N)
let p be Real; ::_thesis: ( 0 < p & p < 1 & u in (r * M) + ((1 - r) * N) & v in (r * M) + ((1 - r) * N) implies (p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N) )
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) ; ::_thesis: (p * u) + ((1 - p) * 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 being 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 being 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 being VECTOR of V such that
A13: x2 = r * mx2 and
A14: mx2 in M by A8;
consider mx1 being 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 being VECTOR of V such that
A18: y2 = (1 - r) * ny2 and
A19: ny2 in N by A9;
consider ny1 being 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, Def2;
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, Def2;
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 (p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N) by RUSUB_4:def_9; ::_thesis: verum
end;
Lm1: for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V holds 1 * M = M
proof
let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M being Subset of V holds 1 * M = M
let M be Subset of V; ::_thesis: 1 * M = M
for v being Element of V st v in M holds
v in 1 * M
proof
let v be Element of V; ::_thesis: ( v in M implies v in 1 * M )
A1: v = 1 * v by RLVECT_1:def_8;
assume v in M ; ::_thesis: v in 1 * M
hence v in 1 * M by A1; ::_thesis: verum
end;
then A2: M c= 1 * M by SUBSET_1:2;
for v being Element of V st v in 1 * M holds
v in M
proof
let v be Element of V; ::_thesis: ( v in 1 * M implies v in M )
assume v in 1 * M ; ::_thesis: v in M
then ex x being Element of V st
( v = 1 * x & x in M ) ;
hence v in M by RLVECT_1:def_8; ::_thesis: verum
end;
then 1 * M c= M by SUBSET_1:2;
hence 1 * M = M by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm2: for V being RealLinearSpace
for M being non empty Subset of V holds 0 * M = {(0. V)}
proof
let V be RealLinearSpace; ::_thesis: for M being non empty Subset of V holds 0 * M = {(0. V)}
let M be non empty Subset of V; ::_thesis: 0 * M = {(0. V)}
for v being Element of V st v in {(0. V)} holds
v in 0 * M
proof
let v be Element of V; ::_thesis: ( v in {(0. V)} implies v in 0 * M )
consider x being set such that
A1: x in M by XBOOLE_0:def_1;
reconsider x = x as Element of V by A1;
assume v in {(0. V)} ; ::_thesis: v in 0 * M
then v = 0. V by TARSKI:def_1;
then v = 0 * x by RLVECT_1:10;
hence v in 0 * M by A1; ::_thesis: verum
end;
then A2: {(0. V)} c= 0 * M by SUBSET_1:2;
for v being Element of V st v in 0 * M holds
v in {(0. V)}
proof
let v be Element of V; ::_thesis: ( v in 0 * M implies v in {(0. V)} )
assume v in 0 * M ; ::_thesis: v in {(0. V)}
then ex x being Element of V st
( v = 0 * x & x in M ) ;
then v = 0. V by RLVECT_1:10;
hence v in {(0. V)} by TARSKI:def_1; ::_thesis: verum
end;
then 0 * M c= {(0. V)} by SUBSET_1:2;
hence 0 * M = {(0. V)} by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm3: for V being non empty add-associative addLoopStr
for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3)
proof
let V be non empty add-associative addLoopStr ; ::_thesis: for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3)
let M1, M2, M3 be Subset of V; ::_thesis: (M1 + M2) + M3 = 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; ::_thesis: ( x in M1 + (M2 + M3) implies x in (M1 + M2) + M3 )
assume x in M1 + (M2 + M3) ; ::_thesis: 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 being 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 being 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 x in (M1 + M2) + M3 by RUSUB_4:def_9; ::_thesis: verum
end;
then A8: M1 + (M2 + M3) c= (M1 + M2) + M3 by SUBSET_1:2;
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; ::_thesis: ( x in (M1 + M2) + M3 implies x in M1 + (M2 + M3) )
assume x in (M1 + M2) + M3 ; ::_thesis: 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 being 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 being 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 x in M1 + (M2 + M3) by RUSUB_4:def_9; ::_thesis: verum
end;
then (M1 + M2) + M3 c= M1 + (M2 + M3) by SUBSET_1:2;
hence (M1 + M2) + M3 = M1 + (M2 + M3) by A8, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm4: for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V
for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M
proof
let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M being Subset of V
for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M
let M be Subset of V; ::_thesis: for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M
let r1, r2 be Real; ::_thesis: r1 * (r2 * M) = (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; ::_thesis: ( x in r1 * (r2 * M) implies x in (r1 * r2) * M )
assume x in r1 * (r2 * M) ; ::_thesis: x in (r1 * r2) * M
then consider w1 being VECTOR of V such that
A1: x = r1 * w1 and
A2: w1 in r2 * M ;
consider w2 being 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 x in (r1 * r2) * M by A4; ::_thesis: verum
end;
then A5: r1 * (r2 * M) c= (r1 * r2) * M by SUBSET_1:2;
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; ::_thesis: ( x in (r1 * r2) * M implies x in r1 * (r2 * M) )
assume x in (r1 * r2) * M ; ::_thesis: x in r1 * (r2 * M)
then consider w1 being 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 x in r1 * (r2 * M) ; ::_thesis: verum
end;
then (r1 * r2) * M c= r1 * (r2 * M) by SUBSET_1:2;
hence r1 * (r2 * M) = (r1 * r2) * M by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm5: for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M1, M2 being Subset of V
for r being Real holds r * (M1 + M2) = (r * M1) + (r * M2)
proof
let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M1, M2 being Subset of V
for r being Real holds r * (M1 + M2) = (r * M1) + (r * M2)
let M1, M2 be Subset of V; ::_thesis: for r being Real holds r * (M1 + M2) = (r * M1) + (r * M2)
let r be Real; ::_thesis: r * (M1 + M2) = (r * M1) + (r * M2)
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; ::_thesis: ( x in (r * M1) + (r * M2) implies x in r * (M1 + M2) )
assume x in (r * M1) + (r * M2) ; ::_thesis: x in r * (M1 + 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 being VECTOR of V such that
A1: x = w1 + w2 and
A2: w1 in r * M1 and
A3: w2 in r * M2 ;
consider v2 being VECTOR of V such that
A4: w2 = r * v2 and
A5: v2 in M2 by A3;
consider v1 being 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 x in r * (M1 + M2) by A8; ::_thesis: verum
end;
then A9: (r * M1) + (r * M2) c= r * (M1 + M2) by SUBSET_1:2;
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; ::_thesis: ( x in r * (M1 + M2) implies x in (r * M1) + (r * M2) )
assume x in r * (M1 + M2) ; ::_thesis: x in (r * M1) + (r * M2)
then consider w9 being 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 being 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 x in (r * M1) + (r * M2) by RUSUB_4:def_9; ::_thesis: verum
end;
then r * (M1 + M2) c= (r * M1) + (r * M2) by SUBSET_1:2;
hence r * (M1 + M2) = (r * M1) + (r * M2) by A9, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: CONVEX1:7
for V being RealLinearSpace
for M being Subset of V
for v being VECTOR of V holds
( M is convex iff v + M is convex )
proof
let V be RealLinearSpace; ::_thesis: for M being Subset of V
for v being VECTOR of V holds
( M is convex iff v + M is convex )
let M be Subset of V; ::_thesis: for v being VECTOR of V holds
( M is convex iff v + M is convex )
let v be VECTOR of V; ::_thesis: ( M is convex iff v + M is convex )
A1: ( v + M is convex implies M is convex )
proof
assume A2: v + M is convex ; ::_thesis: M is convex
let w1, w2 be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & w1 in M & w2 in M holds
(r * w1) + ((1 - r) * w2) in M
let r be Real; ::_thesis: ( 0 < r & r < 1 & w1 in M & w2 in M implies (r * w1) + ((1 - r) * w2) in M )
assume that
A3: ( 0 < r & r < 1 ) and
A4: w1 in M and
A5: w2 in M ; ::_thesis: (r * w1) + ((1 - r) * w2) in M
set x2 = v + w2;
v + w2 in { (v + w) where w is VECTOR of V : w in M } by A5;
then A6: v + w2 in v + M by RUSUB_4:def_8;
set x1 = v + w1;
A7: (r * (v + w1)) + ((1 - r) * (v + w2)) = ((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 ;
v + w1 in { (v + w) where w is VECTOR of V : w in M } by A4;
then v + w1 in v + M by RUSUB_4:def_8;
then (r * (v + w1)) + ((1 - r) * (v + w2)) in v + M by A2, A3, A6, Def2;
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 being VECTOR of V st
( v + ((r * w1) + ((1 - r) * w2)) = v + w & w in M ) ;
hence (r * w1) + ((1 - r) * w2) in M by RLVECT_1:8; ::_thesis: verum
end;
( M is convex implies v + M is convex )
proof
assume A8: M is convex ; ::_thesis: v + M is convex
let w1, w2 be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & w1 in v + M & w2 in v + M holds
(r * w1) + ((1 - r) * w2) in v + M
let r be Real; ::_thesis: ( 0 < r & r < 1 & w1 in v + M & w2 in v + M implies (r * w1) + ((1 - r) * w2) in v + M )
assume that
A9: ( 0 < r & r < 1 ) and
A10: w1 in v + M and
A11: w2 in v + M ; ::_thesis: (r * w1) + ((1 - r) * 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 being 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 being 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, Def2;
then (r * w1) + ((1 - r) * w2) in { (v + w) where w is VECTOR of V : w in M } by A16;
hence (r * w1) + ((1 - r) * w2) in v + M by RUSUB_4:def_8; ::_thesis: verum
end;
hence ( M is convex iff v + M is convex ) by A1; ::_thesis: verum
end;
theorem :: CONVEX1:8
for V being RealLinearSpace holds Up ((0). V) is convex
proof
let V be RealLinearSpace; ::_thesis: Up ((0). V) is convex
let u, v be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & u in Up ((0). V) & v in Up ((0). V) holds
(r * u) + ((1 - r) * v) in Up ((0). V)
let r be Real; ::_thesis: ( 0 < r & r < 1 & u in Up ((0). V) & v in Up ((0). V) implies (r * u) + ((1 - r) * v) in Up ((0). V) )
assume that
0 < r and
r < 1 and
A1: u in Up ((0). V) and
A2: v in Up ((0). V) ; ::_thesis: (r * u) + ((1 - r) * 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, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
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 (r * u) + ((1 - r) * v) in Up ((0). V) by RUSUB_4:def_5; ::_thesis: verum
end;
theorem Th9: :: CONVEX1:9
for V being RealLinearSpace holds Up ((Omega). V) is convex
proof
let V be RealLinearSpace; ::_thesis: Up ((Omega). V) is convex
let u, v be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & u in Up ((Omega). V) & v in Up ((Omega). V) holds
(r * u) + ((1 - r) * v) in Up ((Omega). V)
let r be Real; ::_thesis: ( 0 < r & r < 1 & u in Up ((Omega). V) & v in Up ((Omega). V) implies (r * u) + ((1 - r) * v) in Up ((Omega). V) )
(Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by RLSUB_1:def_4;
then (r * u) + ((1 - r) * v) in the carrier of ((Omega). V) ;
hence ( 0 < r & r < 1 & u in Up ((Omega). V) & v in Up ((Omega). V) implies (r * u) + ((1 - r) * v) in Up ((Omega). V) ) by RUSUB_4:def_5; ::_thesis: verum
end;
theorem Th10: :: CONVEX1:10
for V being non empty RLSStruct
for M being Subset of V st M = {} holds
M is convex
proof
let V be non empty RLSStruct ; ::_thesis: for M being Subset of V st M = {} holds
M is convex
let M be Subset of V; ::_thesis: ( M = {} implies M is convex )
A1: for u, v being VECTOR of V
for r being Real st 0 < r & r < 1 & u in {} & v in {} holds
(r * u) + ((1 - r) * v) in {} ;
assume M = {} ; ::_thesis: M is convex
hence M is convex by A1, Def2; ::_thesis: verum
end;
theorem Th11: :: CONVEX1:11
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M1, M2 being Subset of V
for r1, r2 being Real st M1 is convex & M2 is convex holds
(r1 * M1) + (r2 * M2) is convex
proof
let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M1, M2 being Subset of V
for r1, r2 being Real st M1 is convex & M2 is convex holds
(r1 * M1) + (r2 * M2) is convex
let M1, M2 be Subset of V; ::_thesis: for r1, r2 being Real st M1 is convex & M2 is convex holds
(r1 * M1) + (r2 * M2) is convex
let r1, r2 be Real; ::_thesis: ( M1 is convex & M2 is convex implies (r1 * M1) + (r2 * M2) is convex )
assume that
A1: M1 is convex and
A2: M2 is convex ; ::_thesis: (r1 * M1) + (r2 * M2) is convex
let u, v be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & u in (r1 * M1) + (r2 * M2) & v in (r1 * M1) + (r2 * M2) holds
(r * u) + ((1 - r) * v) in (r1 * M1) + (r2 * M2)
let p be Real; ::_thesis: ( 0 < p & p < 1 & u in (r1 * M1) + (r2 * M2) & v in (r1 * M1) + (r2 * M2) implies (p * u) + ((1 - p) * v) in (r1 * M1) + (r2 * M2) )
assume that
A3: ( 0 < p & p < 1 ) and
A4: u in (r1 * M1) + (r2 * M2) and
A5: v in (r1 * M1) + (r2 * M2) ; ::_thesis: (p * u) + ((1 - p) * 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 being 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 being VECTOR of V such that
A9: u = u1 + u2 and
A10: u1 in r1 * M1 and
A11: u2 in r2 * M2 ;
consider y1 being VECTOR of V such that
A12: v1 = r1 * y1 and
A13: y1 in M1 by A7;
consider x1 being 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 being VECTOR of V such that
A17: v2 = r2 * y2 and
A18: y2 in M2 by A8;
consider x2 being 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, Def2;
then A22: (p * u2) + ((1 - p) * v2) in r2 * M2 by A21;
(p * x1) + ((1 - p) * y1) in M1 by A1, A3, A15, A13, Def2;
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 (p * u) + ((1 - p) * v) in (r1 * M1) + (r2 * M2) by A9, A6, RUSUB_4:def_9; ::_thesis: verum
end;
theorem Th12: :: CONVEX1:12
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V
for r1, r2 being Real holds (r1 + r2) * M c= (r1 * M) + (r2 * M)
proof
let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M being Subset of V
for r1, r2 being Real holds (r1 + r2) * M c= (r1 * M) + (r2 * M)
let M be Subset of V; ::_thesis: for r1, r2 being Real holds (r1 + r2) * M c= (r1 * M) + (r2 * M)
let r1, r2 be Real; ::_thesis: (r1 + r2) * M c= (r1 * M) + (r2 * M)
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; ::_thesis: ( x in (r1 + r2) * M implies x in (r1 * M) + (r2 * M) )
assume x in (r1 + r2) * M ; ::_thesis: x in (r1 * M) + (r2 * M)
then consider w being 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 x in (r1 * M) + (r2 * M) by RUSUB_4:def_9; ::_thesis: verum
end;
hence (r1 + r2) * M c= (r1 * M) + (r2 * M) by SUBSET_1:2; ::_thesis: verum
end;
Lm6: for V being non empty RLSStruct
for M, N being Subset of V
for r being Real st M c= N holds
r * M c= r * N
proof
let V be non empty RLSStruct ; ::_thesis: for M, N being Subset of V
for r being Real st M c= N holds
r * M c= r * N
let M, N be Subset of V; ::_thesis: for r being Real st M c= N holds
r * M c= r * N
let r be Real; ::_thesis: ( M c= N implies r * M c= r * N )
assume A1: M c= N ; ::_thesis: r * M c= r * N
for x being VECTOR of V st x in r * M holds
x in r * N
proof
let x be VECTOR of V; ::_thesis: ( x in r * M implies x in r * N )
assume x in r * M ; ::_thesis: x in r * N
then ex w being VECTOR of V st
( x = r * w & w in M ) ;
hence x in r * N by A1; ::_thesis: verum
end;
hence r * M c= r * N by SUBSET_1:2; ::_thesis: verum
end;
Lm7: for V being non empty RLSStruct
for M being empty Subset of V
for r being Real holds r * M = {}
proof
let V be non empty RLSStruct ; ::_thesis: for M being empty Subset of V
for r being Real holds r * M = {}
let M be empty Subset of V; ::_thesis: for r being Real holds r * M = {}
let r be Real; ::_thesis: r * M = {}
for x being VECTOR of V st x in r * M holds
x in {}
proof
let x be VECTOR of V; ::_thesis: ( x in r * M implies x in {} )
assume x in r * M ; ::_thesis: x in {}
then ex v being VECTOR of V st
( x = r * v & v in {} ) ;
hence x in {} ; ::_thesis: verum
end;
then r * M c= {} by SUBSET_1:2;
hence r * M = {} ; ::_thesis: verum
end;
Lm8: for V being non empty addLoopStr
for M being empty Subset of V
for N being Subset of V holds M + N = {}
proof
let V be non empty addLoopStr ; ::_thesis: for M being empty Subset of V
for N being Subset of V holds M + N = {}
let M be empty Subset of V; ::_thesis: for N being Subset of V holds M + N = {}
let N be Subset of V; ::_thesis: M + N = {}
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; ::_thesis: ( x in M + N implies x in {} )
assume x in M + N ; ::_thesis: x in {}
then ex u, v being Element of V st
( x = u + v & u in {} & v in N ) by A1;
hence x in {} ; ::_thesis: verum
end;
then M + N c= {} by SUBSET_1:2;
hence M + N = {} ; ::_thesis: verum
end;
Lm9: for V being non empty right_zeroed addLoopStr
for M being Subset of V holds M + {(0. V)} = M
proof
let V be non empty right_zeroed addLoopStr ; ::_thesis: for M being Subset of V holds M + {(0. V)} = M
let M be Subset of V; ::_thesis: M + {(0. V)} = M
for x being Element of V st x in M + {(0. V)} holds
x in M
proof
let x be Element of V; ::_thesis: ( x in M + {(0. V)} implies x in M )
assume x in M + {(0. V)} ; ::_thesis: x in M
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 being 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 x in M by A1, RLVECT_1:def_4; ::_thesis: verum
end;
then A3: M + {(0. V)} c= M by SUBSET_1:2;
for x being Element of V st x in M holds
x in M + {(0. V)}
proof
let x be Element of V; ::_thesis: ( x in M implies x in M + {(0. V)} )
A4: ( x = x + (0. V) & 0. V in {(0. V)} ) by RLVECT_1:def_4, TARSKI:def_1;
assume x in M ; ::_thesis: 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 A4;
hence x in M + {(0. V)} by RUSUB_4:def_9; ::_thesis: verum
end;
then M c= M + {(0. V)} by SUBSET_1:2;
hence M + {(0. V)} = M by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm10: for V being RealLinearSpace
for M being Subset of V
for 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; ::_thesis: for M being Subset of V
for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds
(r1 * M) + (r2 * M) c= (r1 + r2) * M
let M be Subset of V; ::_thesis: for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds
(r1 * M) + (r2 * M) c= (r1 + r2) * M
let r1, r2 be Real; ::_thesis: ( r1 >= 0 & r2 >= 0 & M is convex implies (r1 * M) + (r2 * M) c= (r1 + r2) * M )
assume that
A1: r1 >= 0 and
A2: r2 >= 0 and
A3: M is convex ; ::_thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M
percases ( M is empty or not M is empty ) ;
suppose M is empty ; ::_thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M
then ( r1 * M = {} & (r1 + r2) * M = {} ) by Lm7;
hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by Lm8; ::_thesis: verum
end;
supposeA4: not M is empty ; ::_thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M
percases ( r1 = 0 or r2 = 0 or ( r1 <> 0 & r2 <> 0 ) ) ;
supposeA5: r1 = 0 ; ::_thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M
then r1 * M = {(0. V)} by A4, Lm2;
hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by A5, Lm9; ::_thesis: verum
end;
supposeA6: r2 = 0 ; ::_thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M
then r2 * M = {(0. V)} by A4, Lm2;
hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by A6, Lm9; ::_thesis: verum
end;
supposeA7: ( r1 <> 0 & r2 <> 0 ) ; ::_thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M
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 (r1 * M) + (r2 * M) c= (r1 + r2) * M by A9, A10, Lm5; ::_thesis: verum
end;
end;
end;
end;
end;
theorem :: CONVEX1:13
for V being RealLinearSpace
for M being Subset of V
for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds
(r1 * M) + (r2 * M) = (r1 + r2) * M
proof
let V be RealLinearSpace; ::_thesis: for M being Subset of V
for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds
(r1 * M) + (r2 * M) = (r1 + r2) * M
let M be Subset of V; ::_thesis: for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds
(r1 * M) + (r2 * M) = (r1 + r2) * M
let r1, r2 be Real; ::_thesis: ( r1 >= 0 & r2 >= 0 & M is convex implies (r1 * M) + (r2 * M) = (r1 + r2) * M )
assume ( r1 >= 0 & r2 >= 0 & M is convex ) ; ::_thesis: (r1 * M) + (r2 * M) = (r1 + r2) * M
hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by Lm10; :: according to XBOOLE_0:def_10 ::_thesis: (r1 + r2) * M c= (r1 * M) + (r2 * M)
thus (r1 + r2) * M c= (r1 * M) + (r2 * M) by Th12; ::_thesis: verum
end;
theorem :: CONVEX1:14
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M1, M2, M3 being Subset of V
for 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 non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M1, M2, M3 being Subset of V
for r1, r2, r3 being Real st M1 is convex & M2 is convex & M3 is convex holds
((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex
let M1, M2, M3 be Subset of V; ::_thesis: for r1, r2, r3 being Real st M1 is convex & M2 is convex & M3 is convex holds
((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex
let r1, r2, r3 be Real; ::_thesis: ( M1 is convex & M2 is convex & M3 is convex implies ((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex )
assume that
A1: ( M1 is convex & M2 is convex ) and
A2: M3 is convex ; ::_thesis: ((r1 * M1) + (r2 * M2)) + (r3 * 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 ((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex by Lm1; ::_thesis: verum
end;
theorem Th15: :: CONVEX1:15
for V being non empty RLSStruct
for 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 ; ::_thesis: for 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
let F be Subset-Family of V; ::_thesis: ( ( for M being Subset of V st M in F holds
M is convex ) implies meet F is convex )
assume A1: for M being Subset of V st M in F holds
M is convex ; ::_thesis: meet F is convex
percases ( F = {} or F <> {} ) ;
suppose F = {} ; ::_thesis: meet F is convex
then meet F = {} by SETFAM_1:def_1;
hence meet F is convex by Th10; ::_thesis: verum
end;
supposeA2: F <> {} ; ::_thesis: meet F is convex
meet F is convex
proof
let u, v be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & u in meet F & v in meet F holds
(r * u) + ((1 - r) * v) in meet F
let r be Real; ::_thesis: ( 0 < r & r < 1 & u in meet F & v in meet F implies (r * u) + ((1 - r) * v) in meet F )
assume that
A3: ( 0 < r & r < 1 ) and
A4: u in meet F and
A5: v in meet F ; ::_thesis: (r * u) + ((1 - r) * 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 ; ::_thesis: ( M in F implies (r * u) + ((1 - r) * v) in M )
assume A6: M in F ; ::_thesis: (r * u) + ((1 - r) * v) in M
then reconsider M = 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 (r * u) + ((1 - r) * v) in M by A3, A7, Def2; ::_thesis: verum
end;
hence (r * u) + ((1 - r) * v) in meet F by A2, SETFAM_1:def_1; ::_thesis: verum
end;
hence meet F is convex ; ::_thesis: verum
end;
end;
end;
theorem Th16: :: CONVEX1:16
for V being non empty RLSStruct
for M being Subset of V st M is Affine holds
M is convex
proof
let V be non empty RLSStruct ; ::_thesis: for M being Subset of V st M is Affine holds
M is convex
let M be Subset of V; ::_thesis: ( M is Affine implies M is convex )
assume A1: M is Affine ; ::_thesis: M is convex
let u, v be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M
let r be Real; ::_thesis: ( 0 < r & r < 1 & u in M & v in M implies (r * u) + ((1 - r) * v) in M )
assume that
0 < r and
r < 1 and
A2: ( u in M & v in M ) ; ::_thesis: (r * u) + ((1 - r) * v) in M
set p = 1 - r;
1 - (1 - r) = r ;
hence (r * u) + ((1 - r) * v) in M by A1, A2, RUSUB_4:def_4; ::_thesis: verum
end;
registration
let V be non empty RLSStruct ;
cluster non empty convex for Element of K10( the carrier of V);
existence
ex b1 being Subset of V st
( not b1 is empty & b1 is convex )
proof
set M = the non empty Affine Subset of V;
the non empty Affine Subset of V is convex by Th16;
hence ex b1 being Subset of V st
( not b1 is empty & b1 is convex ) ; ::_thesis: verum
end;
end;
registration
let V be non empty RLSStruct ;
cluster empty convex for Element of K10( the carrier of V);
existence
ex b1 being Subset of V st
( b1 is empty & b1 is convex )
proof
{} V is convex by Th10;
hence ex b1 being Subset of V st
( b1 is empty & b1 is convex ) ; ::_thesis: verum
end;
end;
theorem :: CONVEX1:17
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M = { u where u is VECTOR of V : u .|. v >= r } holds
M is convex
proof
let V be non empty RealUnitarySpace-like UNITSTR ; ::_thesis: for M being Subset of V
for v being VECTOR of V
for r being Real st M = { u where u is VECTOR of V : u .|. v >= r } holds
M is convex
let M be Subset of V; ::_thesis: for v being VECTOR of V
for r being Real st M = { u where u is VECTOR of V : u .|. v >= r } holds
M is convex
let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : u .|. v >= r } holds
M is convex
let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : u .|. v >= r } implies M is convex )
assume A1: M = { u where u is VECTOR of V : u .|. v >= r } ; ::_thesis: M is convex
let x, y be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & x in M & y in M holds
(r * x) + ((1 - r) * y) in M
let p be Real; ::_thesis: ( 0 < p & p < 1 & x in M & y in M implies (p * x) + ((1 - p) * y) in M )
assume that
A2: 0 < p and
A3: p < 1 and
A4: x in M and
A5: y in M ; ::_thesis: (p * x) + ((1 - p) * y) in M
0 + p < 1 by A3;
then A6: 0 < 1 - p by XREAL_1:20;
consider u2 being 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 being 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 (p * x) + ((1 - p) * y) in M by A1; ::_thesis: verum
end;
theorem :: CONVEX1:18
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M = { u where u is VECTOR of V : u .|. v > r } holds
M is convex
proof
let V be non empty RealUnitarySpace-like UNITSTR ; ::_thesis: for M being Subset of V
for v being VECTOR of V
for r being Real st M = { u where u is VECTOR of V : u .|. v > r } holds
M is convex
let M be Subset of V; ::_thesis: for v being VECTOR of V
for r being Real st M = { u where u is VECTOR of V : u .|. v > r } holds
M is convex
let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : u .|. v > r } holds
M is convex
let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : u .|. v > r } implies M is convex )
assume A1: M = { u where u is VECTOR of V : u .|. v > r } ; ::_thesis: M is convex
let x, y be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & x in M & y in M holds
(r * x) + ((1 - r) * y) in M
let p be Real; ::_thesis: ( 0 < p & p < 1 & x in M & y in M implies (p * x) + ((1 - p) * y) in M )
assume that
A2: 0 < p and
A3: p < 1 and
A4: x in M and
A5: y in M ; ::_thesis: (p * x) + ((1 - p) * y) in M
0 + p < 1 by A3;
then A6: 0 < 1 - p by XREAL_1:20;
consider u2 being 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 being 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 (p * x) + ((1 - p) * y) in M by A1; ::_thesis: verum
end;
theorem :: CONVEX1:19
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M = { u where u is VECTOR of V : u .|. v <= r } holds
M is convex
proof
let V be non empty RealUnitarySpace-like UNITSTR ; ::_thesis: for M being Subset of V
for v being VECTOR of V
for r being Real st M = { u where u is VECTOR of V : u .|. v <= r } holds
M is convex
let M be Subset of V; ::_thesis: for v being VECTOR of V
for r being Real st M = { u where u is VECTOR of V : u .|. v <= r } holds
M is convex
let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : u .|. v <= r } holds
M is convex
let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : u .|. v <= r } implies M is convex )
assume A1: M = { u where u is VECTOR of V : u .|. v <= r } ; ::_thesis: M is convex
let x, y be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & x in M & y in M holds
(r * x) + ((1 - r) * y) in M
let p be Real; ::_thesis: ( 0 < p & p < 1 & x in M & y in M implies (p * x) + ((1 - p) * y) in M )
assume that
A2: 0 < p and
A3: p < 1 and
A4: x in M and
A5: y in M ; ::_thesis: (p * x) + ((1 - p) * y) in M
0 + p < 1 by A3;
then A6: 0 < 1 - p by XREAL_1:20;
consider u2 being 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 being 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 (p * x) + ((1 - p) * y) in M by A1; ::_thesis: verum
end;
theorem :: CONVEX1:20
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M = { u where u is VECTOR of V : u .|. v < r } holds
M is convex
proof
let V be non empty RealUnitarySpace-like UNITSTR ; ::_thesis: for M being Subset of V
for v being VECTOR of V
for r being Real st M = { u where u is VECTOR of V : u .|. v < r } holds
M is convex
let M be Subset of V; ::_thesis: for v being VECTOR of V
for r being Real st M = { u where u is VECTOR of V : u .|. v < r } holds
M is convex
let v be VECTOR of V; ::_thesis: for r being Real st M = { u where u is VECTOR of V : u .|. v < r } holds
M is convex
let r be Real; ::_thesis: ( M = { u where u is VECTOR of V : u .|. v < r } implies M is convex )
assume A1: M = { u where u is VECTOR of V : u .|. v < r } ; ::_thesis: M is convex
let x, y be VECTOR of V; :: according to CONVEX1:def_2 ::_thesis: for r being Real st 0 < r & r < 1 & x in M & y in M holds
(r * x) + ((1 - r) * y) in M
let p be Real; ::_thesis: ( 0 < p & p < 1 & x in M & y in M implies (p * x) + ((1 - p) * y) in M )
assume that
A2: 0 < p and
A3: p < 1 and
A4: x in M and
A5: y in M ; ::_thesis: (p * x) + ((1 - p) * y) in M
0 + p < 1 by A3;
then A6: 0 < 1 - p by XREAL_1:20;
consider u2 being 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 being 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 (p * x) + ((1 - p) * y) in M by A1; ::_thesis: verum
end;
begin
definition
let V be RealLinearSpace;
let L be Linear_Combination of V;
attrL is convex means :Def3: :: CONVEX1:def 3
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;
:: deftheorem Def3 defines convex CONVEX1:def_3_:_
for V being RealLinearSpace
for L being Linear_Combination of V holds
( L is convex iff 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 ) ) ) ) );
theorem Th21: :: CONVEX1:21
for V being RealLinearSpace
for L being Linear_Combination of V st L is convex holds
Carrier L <> {}
proof
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V st L is convex holds
Carrier L <> {}
let L be Linear_Combination of V; ::_thesis: ( L is convex implies Carrier L <> {} )
assume L is convex ; ::_thesis: Carrier L <> {}
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 ) ) ) by Def3;
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 = {} ; ::_thesis: contradiction
then len F = 0 by A1, CARD_1:27, FINSEQ_4:62;
then f = <*> REAL by A3;
hence contradiction by A3, RVSUM_1:72; ::_thesis: verum
end;
theorem :: CONVEX1:22
for V being RealLinearSpace
for L being Linear_Combination of V
for v being VECTOR of V st L is convex & L . v <= 0 holds
not v in Carrier L
proof
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V
for v being VECTOR of V st L is convex & L . v <= 0 holds
not v in Carrier L
let L be Linear_Combination of V; ::_thesis: for v being VECTOR of V st L is convex & L . v <= 0 holds
not v in Carrier L
let v be VECTOR of V; ::_thesis: ( L is convex & L . v <= 0 implies not v in Carrier L )
assume that
A1: L is convex and
A2: L . v <= 0 ; ::_thesis: not v in Carrier L
percases ( L . v = 0 or L . v < 0 ) by A2;
suppose L . v = 0 ; ::_thesis: not v in Carrier L
hence not v in Carrier L by RLVECT_2:19; ::_thesis: verum
end;
supposeA3: L . v < 0 ; ::_thesis: not v in Carrier L
now__::_thesis:_not_v_in_Carrier_L
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, Def3;
assume v in Carrier L ; ::_thesis: contradiction
then consider n being set such that
A6: n in dom F and
A7: F . n = v by A4, FUNCT_1:def_3;
reconsider n = 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; ::_thesis: verum
end;
hence not v in Carrier L ; ::_thesis: verum
end;
end;
end;
theorem :: CONVEX1:23
for V being RealLinearSpace
for L being Linear_Combination of V st L is convex holds
L <> ZeroLC V
proof
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V st L is convex holds
L <> ZeroLC V
let L be Linear_Combination of V; ::_thesis: ( L is convex implies L <> ZeroLC V )
assume L is convex ; ::_thesis: L <> ZeroLC V
then A1: Carrier L <> {} by Th21;
assume L = ZeroLC V ; ::_thesis: contradiction
hence contradiction by A1, RLVECT_2:def_5; ::_thesis: verum
end;
Lm11: for V being RealLinearSpace
for v being VECTOR of V
for 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; ::_thesis: for v being VECTOR of V
for L being Linear_Combination of V st L is convex & Carrier L = {v} holds
( L . v = 1 & Sum L = (L . v) * v )
let v be VECTOR of V; ::_thesis: for L being Linear_Combination of V st L is convex & Carrier L = {v} holds
( L . v = 1 & Sum L = (L . v) * v )
let L be Linear_Combination of V; ::_thesis: ( L is convex & Carrier L = {v} implies ( L . v = 1 & Sum L = (L . v) * v ) )
assume that
A1: L is convex and
A2: Carrier L = {v} ; ::_thesis: ( L . v = 1 & Sum L = (L . v) * v )
reconsider L = 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, Def3;
A5: F = <*v*> by A2, A3, FINSEQ_3:97;
consider f being 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 ( L . v = 1 & Sum L = (L . v) * v ) by A7, A11, A12, A5, FINSEQ_1:def_8, RLVECT_2:32; ::_thesis: verum
end;
Lm12: for V being RealLinearSpace
for v1, v2 being VECTOR of V
for 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; ::_thesis: for v1, v2 being VECTOR of V
for 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) )
let v1, v2 be VECTOR of V; ::_thesis: for 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) )
let L be Linear_Combination of V; ::_thesis: ( L is convex & Carrier L = {v1,v2} & v1 <> v2 implies ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) )
assume that
A1: L is convex and
A2: Carrier L = {v1,v2} and
A3: v1 <> v2 ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
reconsider L = 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, Def3;
consider f being 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, FINSEQ_1: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__::_thesis:_(_(L_._v1)_+_(L_._v2)_=_1_&_L_._v1_>=_0_&_L_._v2_>=_0_)
percases ( F = <*v1,v2*> or F = <*v2,v1*> ) by A2, A3, A4, FINSEQ_3:99;
suppose F = <*v1,v2*> ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 )
then ( F . 1 = v1 & F . 2 = v2 ) by FINSEQ_1:44;
hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by A7, A8, A11, A13, A12, A14, A15, RVSUM_1:77; ::_thesis: verum
end;
suppose F = <*v2,v1*> ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 )
then ( F . 1 = v2 & F . 2 = v1 ) by FINSEQ_1:44;
hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by A7, A8, A11, A13, A12, A14, A15, RVSUM_1:77; ::_thesis: verum
end;
end;
end;
hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) by A3, RLVECT_2:33; ::_thesis: verum
end;
Lm13: for p being FinSequence
for x, y, z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x & not p = <*x,y,z*> & not p = <*x,z,y*> & not p = <*y,x,z*> & not p = <*y,z,x*> & not p = <*z,x,y*> holds
p = <*z,y,x*>
proof
let p be FinSequence; ::_thesis: for x, y, z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x & not p = <*x,y,z*> & not p = <*x,z,y*> & not p = <*y,x,z*> & not p = <*y,z,x*> & not p = <*z,x,y*> holds
p = <*z,y,x*>
let x, y, z be set ; ::_thesis: ( p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x & not p = <*x,y,z*> & not p = <*x,z,y*> & not p = <*y,x,z*> & not p = <*y,z,x*> & not p = <*z,x,y*> implies p = <*z,y,x*> )
assume that
A1: p is one-to-one and
A2: rng p = {x,y,z} and
A3: ( x <> y & y <> z & z <> x ) ; ::_thesis: ( 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*> )
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 ( 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 A1, A4, A10, A6, A8, FINSEQ_1:45, FUNCT_1:def_4; ::_thesis: verum
end;
Lm14: for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for 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; ::_thesis: for v1, v2, v3 being VECTOR of V
for 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)
let v1, v2, v3 be VECTOR of V; ::_thesis: for 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)
let L be Linear_Combination of {v1,v2,v3}; ::_thesis: ( v1 <> v2 & v2 <> v3 & v3 <> v1 implies Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )
assume that
A1: v1 <> v2 and
A2: v2 <> v3 and
A3: v3 <> v1 ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
A4: Carrier L c= {v1,v2,v3} by RLVECT_2:def_6;
percases ( Carrier L = {} or Carrier L = {v1} or Carrier L = {v2} or Carrier L = {v3} or Carrier L = {v1,v2} or Carrier L = {v1,v3} or Carrier L = {v2,v3} or Carrier L = {v1,v2,v3} ) by A4, ZFMISC_1:118;
suppose Carrier L = {} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
then A5: L = ZeroLC V by RLVECT_2:def_5;
then Sum L = 0. V by RLVECT_2:30
.= (0. V) + (0. V) by RLVECT_1:4
.= ((0. V) + (0. V)) + (0. V) by RLVECT_1:4
.= ((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 Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; ::_thesis: verum
end;
supposeA6: Carrier L = {v1} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
then reconsider L = 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) by RLVECT_1:4
.= (((L . v1) * v1) + (0. V)) + (0. V) by RLVECT_1:4
.= (((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 Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; ::_thesis: verum
end;
supposeA9: Carrier L = {v2} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
then reconsider L = 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) by RLVECT_1:4
.= ((0. V) + ((L . v2) * v2)) + (0. V) by RLVECT_1:4
.= ((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 Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; ::_thesis: verum
end;
supposeA12: Carrier L = {v3} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
then reconsider L = 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) by RLVECT_1:4
.= ((0. V) + (0. V)) + ((L . v3) * v3) by RLVECT_1:4
.= ((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 Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; ::_thesis: verum
end;
supposeA15: Carrier L = {v1,v2} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
then A16: Sum L = ((L . v1) * v1) + ((L . v2) * v2) by A1, RLVECT_2:36
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0. V) by RLVECT_1:4
.= (((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 Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A16, RLVECT_2:19; ::_thesis: verum
end;
supposeA17: Carrier L = {v1,v3} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
then A18: Sum L = ((L . v1) * v1) + ((L . v3) * v3) by A3, RLVECT_2:36
.= (((L . v1) * v1) + (0. V)) + ((L . v3) * v3) by RLVECT_1:4
.= (((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 Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A18, RLVECT_2:19; ::_thesis: verum
end;
supposeA19: Carrier L = {v2,v3} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
then A20: Sum L = ((L . v2) * v2) + ((L . v3) * v3) by A2, RLVECT_2:36
.= ((0. V) + ((L . v2) * v2)) + ((L . v3) * v3) by RLVECT_1:4
.= ((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 Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A20, RLVECT_2:19; ::_thesis: verum
end;
suppose Carrier L = {v1,v2,v3} ; ::_thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
then consider F being 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 Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by RLVECT_1:def_3; ::_thesis: verum
end;
end;
end;
Lm15: for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for 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; ::_thesis: for v1, v2, v3 being VECTOR of V
for 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) )
let v1, v2, v3 be VECTOR of V; ::_thesis: for 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) )
let L be Linear_Combination of V; ::_thesis: ( L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 implies ( ((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) ) )
assume that
A1: L is convex and
A2: Carrier L = {v1,v2,v3} and
A3: ( v1 <> v2 & v2 <> v3 & v3 <> v1 ) ; ::_thesis: ( ((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) )
reconsider L = 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, Def3;
consider f being 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__::_thesis:_(_((L_._v1)_+_(L_._v2))_+_(L_._v3)_=_1_&_L_._v1_>=_0_&_L_._v2_>=_0_&_L_._v3_>=_0_)
percases ( F = <*v1,v2,v3*> or F = <*v1,v3,v2*> or F = <*v2,v1,v3*> or F = <*v2,v3,v1*> or F = <*v3,v1,v2*> or F = <*v3,v2,v1*> ) by A2, A3, A4, Lm13;
supposeA19: F = <*v1,v2,v3*> ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )
then A20: F . 3 = v3 by FINSEQ_1:45;
( F . 1 = v1 & F . 2 = v2 ) by A19, FINSEQ_1:45;
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; ::_thesis: verum
end;
supposeA21: F = <*v1,v3,v2*> ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )
then A22: F . 3 = v2 by FINSEQ_1:45;
( F . 1 = v1 & F . 2 = v3 ) by A21, FINSEQ_1:45;
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; ::_thesis: verum
end;
supposeA23: F = <*v2,v1,v3*> ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )
then A24: F . 3 = v3 by FINSEQ_1:45;
( F . 1 = v2 & F . 2 = v1 ) by A23, FINSEQ_1:45;
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; ::_thesis: verum
end;
supposeA25: F = <*v2,v3,v1*> ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )
then A26: F . 3 = v1 by FINSEQ_1:45;
( F . 1 = v2 & F . 2 = v3 ) by A25, FINSEQ_1:45;
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; ::_thesis: verum
end;
supposeA27: F = <*v3,v1,v2*> ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )
then A28: F . 3 = v2 by FINSEQ_1:45;
( F . 1 = v3 & F . 2 = v1 ) by A27, FINSEQ_1:45;
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; ::_thesis: verum
end;
supposeA29: F = <*v3,v2,v1*> ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )
then A30: F . 3 = v1 by FINSEQ_1:45;
( F . 1 = v3 & F . 2 = v2 ) by A29, FINSEQ_1:45;
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; ::_thesis: verum
end;
end;
end;
hence ( ((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 A3, Lm14; ::_thesis: verum
end;
theorem :: CONVEX1:24
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of {v} st L is convex holds
( L . v = 1 & Sum L = (L . v) * v )
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for L being Linear_Combination of {v} st L is convex holds
( L . v = 1 & Sum L = (L . v) * v )
let v be VECTOR of V; ::_thesis: for L being Linear_Combination of {v} st L is convex holds
( L . v = 1 & Sum L = (L . v) * v )
let L be Linear_Combination of {v}; ::_thesis: ( L is convex implies ( L . v = 1 & Sum L = (L . v) * 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 ; ::_thesis: ( L . v = 1 & Sum L = (L . v) * v )
hence ( L . v = 1 & Sum L = (L . v) * v ) by A1, Lm11, Th21; ::_thesis: verum
end;
theorem :: CONVEX1:25
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for 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; ::_thesis: for v1, v2 being VECTOR of V
for 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) )
let v1, v2 be VECTOR of V; ::_thesis: for 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) )
let L be Linear_Combination of {v1,v2}; ::_thesis: ( v1 <> v2 & L is convex implies ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) )
assume that
A1: v1 <> v2 and
A2: L is convex ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
A3: ( Carrier L c= {v1,v2} & Carrier L <> {} ) by A2, Th21, RLVECT_2:def_6;
now__::_thesis:_(_(L_._v1)_+_(L_._v2)_=_1_&_L_._v1_>=_0_&_L_._v2_>=_0_)
percases ( Carrier L = {v1} or Carrier L = {v2} or Carrier L = {v1,v2} ) by A3, ZFMISC_1:36;
supposeA4: Carrier L = {v1} ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 )
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; ::_thesis: verum
end;
supposeA5: Carrier L = {v2} ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 )
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; ::_thesis: verum
end;
suppose Carrier L = {v1,v2} ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 )
hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by A1, A2, Lm12; ::_thesis: verum
end;
end;
end;
hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) by A1, RLVECT_2:33; ::_thesis: verum
end;
theorem :: CONVEX1:26
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for 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; ::_thesis: for v1, v2, v3 being VECTOR of V
for 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) )
let v1, v2, v3 be VECTOR of V; ::_thesis: for 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) )
let L be Linear_Combination of {v1,v2,v3}; ::_thesis: ( v1 <> v2 & v2 <> v3 & v3 <> v1 & L is convex implies ( ((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) ) )
assume that
A1: v1 <> v2 and
A2: v2 <> v3 and
A3: v3 <> v1 and
A4: L is convex ; ::_thesis: ( ((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) )
A5: ( Carrier L c= {v1,v2,v3} & Carrier L <> {} ) by A4, Th21, RLVECT_2:def_6;
now__::_thesis:_(_((L_._v1)_+_(L_._v2))_+_(L_._v3)_=_1_&_L_._v1_>=_0_&_L_._v2_>=_0_&_L_._v3_>=_0_)
percases ( Carrier L = {v1} or Carrier L = {v2} or Carrier L = {v3} or Carrier L = {v1,v2} or Carrier L = {v2,v3} or Carrier L = {v1,v3} or Carrier L = {v1,v2,v3} ) by A5, ZFMISC_1:118;
supposeA6: Carrier L = {v1} ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )
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; ::_thesis: verum
end;
supposeA8: Carrier L = {v2} ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )
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; ::_thesis: verum
end;
supposeA10: Carrier L = {v3} ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )
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; ::_thesis: verum
end;
supposeA12: Carrier L = {v1,v2} ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )
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; ::_thesis: verum
end;
supposeA13: Carrier L = {v2,v3} ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )
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; ::_thesis: verum
end;
supposeA14: Carrier L = {v1,v3} ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )
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; ::_thesis: verum
end;
suppose Carrier L = {v1,v2,v3} ; ::_thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )
hence ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) by A1, A2, A3, A4, Lm15; ::_thesis: verum
end;
end;
end;
hence ( ((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 A1, A2, A3, Lm14; ::_thesis: verum
end;
theorem :: CONVEX1:27
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V st L is convex & Carrier L = {v} holds
L . v = 1 by Lm11;
theorem :: CONVEX1:28
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for 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 :: CONVEX1:29
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for 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
definition
let V be non empty RLSStruct ;
let M be Subset of V;
func Convex-Family M -> Subset-Family of V means :Def4: :: CONVEX1:def 4
for N being Subset of V holds
( N in it iff ( N is convex & M c= N ) );
existence
ex b1 being Subset-Family of V st
for N being Subset of V holds
( N in b1 iff ( N is convex & M c= N ) )
proof
defpred S1[ Subset of V] means ( $1 is convex & M c= $1 );
thus ex F being Subset-Family of V st
for N being Subset of V holds
( N in F iff S1[N] ) from SUBSET_1:sch_3(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset-Family of V st ( for N being Subset of V holds
( N in b1 iff ( N is convex & M c= N ) ) ) & ( for N being Subset of V holds
( N in b2 iff ( N is convex & M c= N ) ) ) holds
b1 = b2
proof
let SF, SG be Subset-Family of V; ::_thesis: ( ( for N being Subset of V holds
( N in SF iff ( N is convex & M c= N ) ) ) & ( for N being Subset of V holds
( N in SG iff ( N is convex & M c= N ) ) ) implies SF = SG )
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 ) ) ; ::_thesis: SF = SG
for Y being Subset of V holds
( Y in SF iff Y in SG )
proof
let Y be Subset of V; ::_thesis: ( Y in SF iff Y in SG )
hereby ::_thesis: ( Y in SG implies Y in SF )
assume Y in SF ; ::_thesis: Y in SG
then ( Y is convex & M c= Y ) by A1;
hence Y in SG by A2; ::_thesis: verum
end;
assume Y in SG ; ::_thesis: Y in SF
then ( Y is convex & M c= Y ) by A2;
hence Y in SF by A1; ::_thesis: verum
end;
hence SF = SG by SETFAM_1:31; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines Convex-Family CONVEX1:def_4_:_
for V being non empty RLSStruct
for M being Subset of V
for b3 being Subset-Family of V holds
( b3 = Convex-Family M iff for N being Subset of V holds
( N in b3 iff ( N is convex & M c= N ) ) );
definition
let V be non empty RLSStruct ;
let M be Subset of V;
func conv M -> convex Subset of V equals :: CONVEX1:def 5
meet (Convex-Family M);
coherence
meet (Convex-Family M) is convex Subset of V
proof
for N being Subset of V st N in Convex-Family M holds
N is convex by Def4;
hence meet (Convex-Family M) is convex Subset of V by Th15; ::_thesis: verum
end;
end;
:: deftheorem defines conv CONVEX1:def_5_:_
for V being non empty RLSStruct
for M being Subset of V holds conv M = meet (Convex-Family M);
theorem :: CONVEX1:30
for V being non empty RLSStruct
for M being Subset of V
for N being convex Subset of V st M c= N holds
conv M c= N
proof
let V be non empty RLSStruct ; ::_thesis: for M being Subset of V
for N being convex Subset of V st M c= N holds
conv M c= N
let M be Subset of V; ::_thesis: for N being convex Subset of V st M c= N holds
conv M c= N
let N be convex Subset of V; ::_thesis: ( M c= N implies conv M c= N )
assume M c= N ; ::_thesis: conv M c= N
then N in Convex-Family M by Def4;
hence conv M c= N by SETFAM_1:3; ::_thesis: verum
end;
begin
theorem :: CONVEX1:31
for p being FinSequence
for x, y, z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x & not p = <*x,y,z*> & not p = <*x,z,y*> & not p = <*y,x,z*> & not p = <*y,z,x*> & not p = <*z,x,y*> holds
p = <*z,y,x*> by Lm13;
theorem :: CONVEX1:32
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V holds 1 * M = M by Lm1;
theorem :: CONVEX1:33
for V being non empty RLSStruct
for M being empty Subset of V
for r being Real holds r * M = {} by Lm7;
theorem :: CONVEX1:34
for V being RealLinearSpace
for M being non empty Subset of V holds 0 * M = {(0. V)} by Lm2;
theorem :: CONVEX1:35
for V being non empty right_zeroed addLoopStr
for M being Subset of V holds M + {(0. V)} = M by Lm9;
theorem :: CONVEX1:36
for V being non empty add-associative addLoopStr
for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3) by Lm3;
theorem :: CONVEX1:37
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V
for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M by Lm4;
theorem :: CONVEX1:38
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M1, M2 being Subset of V
for r being Real holds r * (M1 + M2) = (r * M1) + (r * M2) by Lm5;
theorem :: CONVEX1:39
for V being non empty RLSStruct
for M, N being Subset of V
for r being Real st M c= N holds
r * M c= r * N by Lm6;
theorem :: CONVEX1:40
for V being non empty addLoopStr
for M being empty Subset of V
for N being Subset of V holds M + N = {} by Lm8;
begin
registration
let V be non empty RLSStruct ;
let M, N be convex Subset of V;
clusterM /\ N -> convex for Subset of V;
coherence
for b1 being Subset of V st b1 = M /\ N holds
b1 is convex
proof
now__::_thesis:_for_x,_y_being_VECTOR_of_V
for_r_being_Real_st_0_<_r_&_r_<_1_&_x_in_M_/\_N_&_y_in_M_/\_N_holds_
(r_*_x)_+_((1_-_r)_*_y)_in_M_/\_N
let x, y be VECTOR of V; ::_thesis: for r being Real st 0 < r & r < 1 & x in M /\ N & y in M /\ N holds
(r * x) + ((1 - r) * y) in M /\ N
let r be Real; ::_thesis: ( 0 < r & r < 1 & x in M /\ N & y in M /\ N implies (r * x) + ((1 - r) * y) in M /\ N )
assume that
A1: ( 0 < r & r < 1 ) and
A2: ( x in M /\ N & y in M /\ N ) ; ::_thesis: (r * x) + ((1 - r) * 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; ::_thesis: verum
end;
hence for b1 being Subset of V st b1 = M /\ N holds
b1 is convex by Def2; ::_thesis: verum
end;
end;
registration
let V be RealLinearSpace;
let M be Subset of V;
cluster Convex-Family M -> non empty ;
coherence
not Convex-Family M is empty
proof
A1: M c= Up ((Omega). V)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in M or x in Up ((Omega). V) )
assume x in M ; ::_thesis: x in Up ((Omega). V)
then reconsider x = x as Element of V ;
x in the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ;
then x in the carrier of ((Omega). V) by RLSUB_1:def_4;
hence x in Up ((Omega). V) by RUSUB_4:def_5; ::_thesis: verum
end;
Up ((Omega). V) is convex by Th9;
hence not Convex-Family M is empty by A1, Def4; ::_thesis: verum
end;
end;
theorem :: CONVEX1:41
for V being RealLinearSpace
for M being Subset of V holds M c= conv M
proof
let V be RealLinearSpace; ::_thesis: for M being Subset of V holds M c= conv M
let M be Subset of V; ::_thesis: M c= conv M
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in M or v in conv M )
assume A1: v in M ; ::_thesis: v in conv M
for Y being set st Y in Convex-Family M holds
v in Y
proof
let Y be set ; ::_thesis: ( Y in Convex-Family M implies v in Y )
assume A2: Y in Convex-Family M ; ::_thesis: v in Y
then reconsider Y = Y as Subset of V ;
M c= Y by A2, Def4;
hence v in Y by A1; ::_thesis: verum
end;
hence v in conv M by SETFAM_1:def_1; ::_thesis: verum
end;