let n be Element of NAT ; :: thesis: for a being Real
for P being Subset of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
P is convex
let a be Real; :: thesis: for P being Subset of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
P is convex
let P be Subset of (TOP-REAL n); :: thesis: ( P = { q where q is Point of (TOP-REAL n) : |.q.| < a } implies P is convex )
assume A1: P = { q where q is Point of (TOP-REAL n) : |.q.| < a } ; :: thesis: P is convex
for p1, p2 being Point of (TOP-REAL n) st p1 in P & p2 in P holds
LSeg p1,p2 c= P

proof

let p1, p2 be Point of (TOP-REAL n); :: thesis: ( p1 in P & p2 in P implies LSeg p1,p2 c= P )
assume that
A2: p1 in P and
A3: p2 in P ; :: thesis: LSeg p1,p2 c= P
A4: ex q2 being Point of (TOP-REAL n) st
( q2 = p2 & |.q2.| < a ) by A1, A3;
A5: ex q1 being Point of (TOP-REAL n) st
( q1 = p1 & |.q1.| < a ) by A1, A2;
LSeg p1,p2 c= P

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg p1,p2 or x in P )
assume A6: x in LSeg p1,p2 ; :: thesis: x in P
then consider r being Real such that
A7: x = ((1 - r) * p1) + (r * p2) and
A8: 0 <= r and
A9: r <= 1 ;
A10: |.((1 - r) * p1).| = (abs (1 - r)) * |.p1.| by TOPRNS_1:8;
reconsider q = x as Point of (TOP-REAL n) by A6;
A11: |.(((1 - r) * p1) + (r * p2)).| <= |.((1 - r) * p1).| + |.(r * p2).| by TOPRNS_1:30;
A12: 1 - r >= 0 by A9, XREAL_1:50;
then A13: abs (1 - r) = 1 - r by ABSVALUE:def 1;

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

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

A15: ( |.(r * p2).| = (abs r) * |.p2.| & r = abs r ) by A8, ABSVALUE:def 1, TOPRNS_1:8;
0 <= abs r by COMPLEX1:132;
then A16: (abs r) * |.p2.| <= (abs r) * a by A4, XREAL_1:66;
(abs (1 - r)) * |.p1.| < (abs (1 - r)) * a by A5, A13, A14, XREAL_1:70;
then |.((1 - r) * p1).| + |.(r * p2).| < ((1 - r) * a) + (r * a) by A10, A13, A16, A15, XREAL_1:10;
then |.q.| < a by A7, A11, 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 A12;
then 0 < abs r by ABSVALUE:def 1;
then A17: (abs r) * |.p2.| < (abs r) * a by A4, XREAL_1:70;
A18: r = abs r by A8, ABSVALUE:def 1;
( (abs (1 - r)) * |.p1.| <= (abs (1 - r)) * a & |.(r * p2).| = (abs r) * |.p2.| ) by A5, A12, A13, TOPRNS_1:8, XREAL_1:66;
then |.((1 - r) * p1).| + |.(r * p2).| < ((1 - r) * a) + (r * a) by A10, A13, A17, A18, XREAL_1:10;
then |.q.| < a by A7, A11, XXREAL_0:2;
hence x in P by A1; :: thesis: verum

end;

end;

end;

hence LSeg p1,p2 c= P ; :: thesis: verum

end;

hence P is convex by JORDAN1:def 1; :: thesis: verum