let n be Nat; :: thesis: for u being Point of (Euclid n)
for a being Real
for P being Subset of (TOP-REAL n) st P = Ball (u,a) holds
P is convex
let u be Point of (Euclid n); :: thesis: for a being Real
for P being Subset of (TOP-REAL n) st P = Ball (u,a) holds
P is convex
let a be Real; :: thesis: for P being Subset of (TOP-REAL n) st P = Ball (u,a) holds
P is convex
let P be Subset of (TOP-REAL n); :: thesis: ( P = Ball (u,a) implies P is convex )
assume A1: P = Ball (u,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

reconsider p = u as Point of (TOP-REAL n) by TOPREAL3:8;
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: P = { q where q is Element of (Euclid n) : dist (u,q) < a } by A1, METRIC_1:17;
then ex q2 being Point of (Euclid n) st
( q2 = p2 & dist (u,q2) < a ) by A3;
then A5: |.(p - p2).| < a by JGRAPH_1:28;
A6: for p3 being Point of (TOP-REAL n) st |.(p - p3).| < a holds
p3 in P

proof

let p3 be Point of (TOP-REAL n); :: thesis: ( |.(p - p3).| < a implies p3 in P )
reconsider u3 = p3 as Point of (Euclid n) by TOPREAL3:8;
assume |.(p - p3).| < a ; :: thesis: p3 in P
then dist (u,u3) < a by JGRAPH_1:28;
hence p3 in P by A4; :: thesis: verum

end;

ex q1 being Point of (Euclid n) st
( q1 = p1 & dist (u,q1) < a ) by A2, A4;
then A7: |.(p - p1).| < a by JGRAPH_1:28;
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 A8: x in LSeg (p1,p2) ; :: thesis: x in P
then consider r being Real such that
A9: x = ((1 - r) * p1) + (r * p2) and
A10: 0 <= r and
A11: r <= 1 ;
reconsider q = x as Point of (TOP-REAL n) by A8;
A12: |.((1 - r) * (p - p1)).| = |.(1 - r).| * |.(p - p1).| by TOPRNS_1:7;
((1 - r) * p) + (r * p) = ((1 - r) + r) * p by RLVECT_1:def 6
.= p by RLVECT_1:def 8 ;
then |.(p - (((1 - r) * p1) + (r * p2))).| = |.(((((1 - r) * p) + (r * p)) - ((1 - r) * p1)) - (r * p2)).| by RLVECT_1:27
.= |.(((((1 - r) * p) + (- ((1 - r) * p1))) + (r * p)) + (- (r * p2))).| by RLVECT_1:def 3
.= |.((((1 - r) * p) + (- ((1 - r) * p1))) + ((r * p) + (- (r * p2)))).| by RLVECT_1:def 3
.= |.((((1 - r) * p) + ((1 - r) * (- p1))) + ((r * p) + (- (r * p2)))).| by RLVECT_1:25
.= |.(((1 - r) * (p - p1)) + ((r * p) + (- (r * p2)))).| by RLVECT_1:def 5
.= |.(((1 - r) * (p - p1)) + ((r * p) + (r * (- p2)))).| by RLVECT_1:25
.= |.(((1 - r) * (p - p1)) + (r * (p - p2))).| by RLVECT_1:def 5 ;
then A13: |.(p - (((1 - r) * p1) + (r * p2))).| <= |.((1 - r) * (p - p1)).| + |.(r * (p - p2)).| by TOPRNS_1:29;
A14: 1 - r >= 0 by A11, XREAL_1:48;
then A15: |.(1 - r).| = 1 - r by ABSVALUE:def 1;

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

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

A17: ( |.(r * (p - p2)).| = |.r.| * |.(p - p2).| & r = |.r.| ) by A10, ABSVALUE:def 1, TOPRNS_1:7;
0 <= |.r.| by COMPLEX1:46;
then A18: |.r.| * |.(p - p2).| <= |.r.| * a by A5, XREAL_1:64;
|.(1 - r).| * |.(p - p1).| < |.(1 - r).| * a by A7, A15, A16, XREAL_1:68;
then |.((1 - r) * (p - p1)).| + |.(r * (p - p2)).| < ((1 - r) * a) + (r * a) by A12, A15, A18, A17, XREAL_1:8;
then |.(p - q).| < a by A9, A13, XXREAL_0:2;
hence x in P by A6; :: thesis: verum

end;

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

then (1 - r) + r = 0 + r by A14;
then 0 < |.r.| by ABSVALUE:def 1;
then A19: |.r.| * |.(p - p2).| < |.r.| * a by A5, XREAL_1:68;
A20: r = |.r.| by A10, ABSVALUE:def 1;
( |.(1 - r).| * |.(p - p1).| <= |.(1 - r).| * a & |.(r * (p - p2)).| = |.r.| * |.(p - p2).| ) by A7, A14, A15, TOPRNS_1:7, XREAL_1:64;
then |.((1 - r) * (p - p1)).| + |.(r * (p - p2)).| < ((1 - r) * a) + (r * a) by A12, A15, A19, A20, XREAL_1:8;
then |.(p - q).| < a by A9, A13, XXREAL_0:2;
hence x in P by A6; :: thesis: verum

end;

end;

end;

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

end;

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