let n be 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 object ; :: 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).| = |.(1 - r).| * |.p1.| by TOPRNS_1:7;
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:29;
A12: 1 - r >= 0 by A9, XREAL_1:48;
then A13: |.(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).| = |.r.| * |.p2.| & r = |.r.| ) by A8, ABSVALUE:def 1, TOPRNS_1:7;
0 <= |.r.| by COMPLEX1:46;
then A16: |.r.| * |.p2.| <= |.r.| * a by A4, XREAL_1:64;
|.(1 - r).| * |.p1.| < |.(1 - r).| * a by A5, A13, A14, XREAL_1:68;
then |.((1 - r) * p1).| + |.(r * p2).| < ((1 - r) * a) + (r * a) by A10, A13, A16, A15, XREAL_1:8;
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 < |.r.| by ABSVALUE:def 1;
then A17: |.r.| * |.p2.| < |.r.| * a by A4, XREAL_1:68;
A18: r = |.r.| by A8, ABSVALUE:def 1;
( |.(1 - r).| * |.p1.| <= |.(1 - r).| * a & |.(r * p2).| = |.r.| * |.p2.| ) by A5, A12, A13, TOPRNS_1:7, XREAL_1:64;
then |.((1 - r) * p1).| + |.(r * p2).| < ((1 - r) * a) + (r * a) by A10, A13, A17, A18, XREAL_1:8;
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