let n be Nat; :: thesis: for a being Real
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; :: 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 object ; :: 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 = |.r.| by A7, ABSVALUE:def 1;
reconsider q = x as Point of (TOP-REAL n) by A5;
A10: |.((1 - r) * (p1 - Q)).| = |.(1 - r).| * |.(p1 - Q).| by TOPRNS_1:7;
A11: 1 - r >= 0 by A8, XREAL_1:48;
then A12: |.(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 <= |.r.| by COMPLEX1:46;
then A14: ( |.(r * (p2 - Q)).| = |.r.| * |.(p2 - Q).| & |.r.| * |.(p2 - Q).| <= |.r.| * a ) by A4, TOPRNS_1:7, XREAL_1:64;
((1 - r) * Q) + (r * Q) = ((1 * Q) - (r * Q)) + (r * Q) by RLVECT_1:35
.= 1 * Q by RLVECT_4:1
.= Q by RLVECT_1:def 8 ;
then q - Q = ((((1 - r) * p1) + (r * p2)) - ((1 - r) * Q)) - (r * Q) by A6, RLVECT_1:27
.= ((((1 - r) * p1) - ((1 - r) * Q)) + (r * p2)) - (r * Q) by RLVECT_1:def 3
.= (((1 - r) * (p1 - Q)) + (r * p2)) - (r * Q) by RLVECT_1:34
.= ((1 - r) * (p1 - Q)) + ((r * p2) - (r * Q)) by RLVECT_1:def 3
.= ((1 - r) * (p1 - Q)) + (r * (p2 - Q)) by RLVECT_1:34 ;
then A15: |.(q - Q).| <= |.((1 - r) * (p1 - Q)).| + |.(r * (p2 - Q)).| by TOPRNS_1:29;
|.(1 - r).| * |.(p1 - Q).| <= |.(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, Th2; :: thesis: verum

end;

end;