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 that
A1:
M is convex
and
A2:
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 - Nlet 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 A3:
(
0 < r &
r < 1 &
u in M - N &
v in M - N )
;
:: thesis: (r * u) + ((1 - r) * v) in M - N
then
u in { (x - y) where x, y is Element of V : ( x in M & y in N ) }
by RUSUB_5:def 2;
then consider x1,
y1 being
Element of
V such that A4:
(
u = x1 - y1 &
x1 in M &
y1 in N )
;
v in { (x - y) where x, y is Element of V : ( x in M & y in N ) }
by A3, RUSUB_5:def 2;
then consider x2,
y2 being
Element of
V such that A5:
(
v = x2 - y2 &
x2 in M &
y2 in N )
;
A6:
(r * x1) + ((1 - r) * x2) in M
by A1, A3, A4, A5, Def2;
A7:
(r * y1) + ((1 - r) * y2) in N
by A2, A3, A4, A5, Def2;
(r * u) + ((1 - r) * v) =
((r * x1) - (r * y1)) + ((1 - r) * (x2 - y2))
by A4, A5, RLVECT_1:48
.=
((r * x1) - (r * y1)) + (((1 - r) * x2) - ((1 - r) * y2))
by RLVECT_1:48
.=
(((r * x1) - (r * y1)) + ((1 - r) * x2)) - ((1 - r) * y2)
by RLVECT_1:def 6
.=
((r * x1) - ((r * y1) - ((1 - r) * x2))) - ((1 - r) * y2)
by RLVECT_1:43
.=
((r * x1) + (((1 - r) * x2) + (- (r * y1)))) - ((1 - r) * y2)
by RLVECT_1:47
.=
(((r * x1) + ((1 - r) * x2)) + (- (r * y1))) - ((1 - r) * y2)
by RLVECT_1:def 6
.=
((r * x1) + ((1 - r) * x2)) + ((- (r * y1)) - ((1 - r) * y2))
by RLVECT_1:def 6
.=
((r * x1) + ((1 - r) * x2)) - ((r * y1) + ((1 - r) * y2))
by RLVECT_1:44
;
then
(r * u) + ((1 - r) * v) in { (x - y) where x, y is Element of V : ( x in M & y in N ) }
by A6, A7;
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