let n be Element of NAT ; for X, B being Subset of (TOP-REAL n) st X is convex & B is convex holds
( X (+) B is convex & X (-) B is convex )
let X, B be Subset of (TOP-REAL n); ( X is convex & B is convex implies ( X (+) B is convex & X (-) B is convex ) )
assume that
A1:
X is convex
and
A2:
B is convex
; ( X (+) B is convex & X (-) B is convex )
for x, y being Point of (TOP-REAL n)
for r being Real st 0 <= r & r <= 1 & x in X (+) B & y in X (+) B holds
(r * x) + ((1 - r) * y) in X (+) B
proof
let x,
y be
Point of
(TOP-REAL n);
for r being Real st 0 <= r & r <= 1 & x in X (+) B & y in X (+) B holds
(r * x) + ((1 - r) * y) in X (+) Blet r be
Real;
( 0 <= r & r <= 1 & x in X (+) B & y in X (+) B implies (r * x) + ((1 - r) * y) in X (+) B )
assume that A3:
(
0 <= r &
r <= 1 )
and A4:
x in X (+) B
and A5:
y in X (+) B
;
(r * x) + ((1 - r) * y) in X (+) B
consider x2,
b2 being
Point of
(TOP-REAL n) such that A6:
y = x2 + b2
and A7:
(
x2 in X &
b2 in B )
by A5;
consider x1,
b1 being
Point of
(TOP-REAL n) such that A8:
x = x1 + b1
and A9:
(
x1 in X &
b1 in B )
by A4;
(
(r * x1) + ((1 - r) * x2) in X &
(r * b1) + ((1 - r) * b2) in B )
by A1, A2, A3, A9, A7;
then
((r * x1) + ((1 - r) * x2)) + ((r * b1) + ((1 - r) * b2)) in { (x3 + b3) where x3, b3 is Point of (TOP-REAL n) : ( x3 in X & b3 in B ) }
;
then
(((r * x1) + ((1 - r) * x2)) + (r * b1)) + ((1 - r) * b2) in X (+) B
by RLVECT_1:def 3;
then
(((r * x1) + (r * b1)) + ((1 - r) * x2)) + ((1 - r) * b2) in X (+) B
by RLVECT_1:def 3;
then
((r * x1) + (r * b1)) + (((1 - r) * x2) + ((1 - r) * b2)) in X (+) B
by RLVECT_1:def 3;
then
(r * (x1 + b1)) + (((1 - r) * x2) + ((1 - r) * b2)) in X (+) B
by RLVECT_1:def 5;
hence
(r * x) + ((1 - r) * y) in X (+) B
by A8, A6, RLVECT_1:def 5;
verum
end;
hence
X (+) B is convex
; X (-) B is convex
for x, y being Point of (TOP-REAL n)
for r being Real st 0 <= r & r <= 1 & x in X (-) B & y in X (-) B holds
(r * x) + ((1 - r) * y) in X (-) B
hence
X (-) B is convex
; verum