let n be Element of NAT ; :: thesis: for a being real number
for P being Subset of (TOP-REAL n)
for Q being Point of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| <= a } holds
P is convex
let a be real number ; :: thesis: for P being Subset of (TOP-REAL n)
for Q being Point of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| <= a } holds
P is convex
let P be Subset of (TOP-REAL n); :: thesis: for Q being Point of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| <= a } holds
P is convex
let Q be Point of (TOP-REAL n); :: thesis: ( P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| <= a } implies P is convex )
assume A1: P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| <= a } ; :: thesis: P is convex
let p1, p2 be Point of (TOP-REAL n); :: according to JORDAN1:def 1 :: thesis: ( not p1 in P or not p2 in P or LSeg (p1,p2) c= P )
assume p1 in P ; :: thesis: ( not p2 in P or LSeg (p1,p2) c= P )
then A2: ex q1 being Point of (TOP-REAL n) st
( q1 = p1 & |.(q1 - Q).| <= a ) by A1;
assume A3: p2 in P ; :: thesis: LSeg (p1,p2) c= P
then A4: ex q2 being Point of (TOP-REAL n) st
( q2 = p2 & |.(q2 - Q).| <= a ) by A1;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg (p1,p2) or x in P )
assume A5: x in LSeg (p1,p2) ; :: thesis: x in P
then consider r being Real such that
A6: x = ((1 - r) * p1) + (r * p2) and
A7: 0 <= r and
A8: r <= 1 ;
A9: r = abs r by A7, ABSVALUE:def 1;
reconsider q = x as Point of (TOP-REAL n) by A5;
A10: |.((1 - r) * (p1 - Q)).| = (abs (1 - r)) * |.(p1 - Q).| by TOPRNS_1:7;
A11: 1 - r >= 0 by A8, XREAL_1:48;
then A12: abs (1 - r) = 1 - r by ABSVALUE:def 1;

per cases ( 1 - r > 0 or 1 - r <= 0 ) ;

suppose A13: 1 - r > 0 ; :: thesis: x in P

0 <= abs r by COMPLEX1:46;
then A14: ( |.(r * (p2 - Q)).| = (abs r) * |.(p2 - Q).| & (abs r) * |.(p2 - Q).| <= (abs r) * a ) by A4, TOPRNS_1:7, XREAL_1:64;
((1 - r) * Q) + (r * Q) = ((1 * Q) - (r * Q)) + (r * Q) by EUCLID:50
.= 1 * Q by EUCLID:48
.= Q by EUCLID:29 ;
then q - Q = ((((1 - r) * p1) + (r * p2)) - ((1 - r) * Q)) - (r * Q) by A6, EUCLID:46
.= ((((1 - r) * p1) + (- ((1 - r) * Q))) + (r * p2)) - (r * Q) by EUCLID:26
.= ((((1 - r) * p1) - ((1 - r) * Q)) + (r * p2)) - (r * Q)
.= (((1 - r) * (p1 - Q)) + (r * p2)) - (r * Q) by EUCLID:49
.= ((1 - r) * (p1 - Q)) + ((r * p2) - (r * Q)) by EUCLID:45
.= ((1 - r) * (p1 - Q)) + (r * (p2 - Q)) by EUCLID:49 ;
then A15: |.(q - Q).| <= |.((1 - r) * (p1 - Q)).| + |.(r * (p2 - Q)).| by TOPRNS_1:29;
(abs (1 - r)) * |.(p1 - Q).| <= (abs (1 - r)) * a by A2, A12, A13, XREAL_1:64;
then |.((1 - r) * (p1 - Q)).| + |.(r * (p2 - Q)).| <= ((1 - r) * a) + (r * a) by A9, A10, A12, A14, XREAL_1:7;
then |.(q - Q).| <= a by A15, XXREAL_0:2;
hence x in P by A1; :: thesis: verum

end;

suppose 1 - r <= 0 ; :: thesis: x in P

then (1 - r) + r = 0 + r by A11;
hence x in P by A3, A6, Th4; :: thesis: verum

end;

end;