let V be 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
let M, N be Subset of V; ( M is convex & N is convex implies M + N is convex )
assume A1:
( M is convex & N is convex )
; 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;
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 + Nlet r be
Real;
( 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
;
(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;
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;
verum
end;
hence
M + N is convex
; verum