let n be Element of 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:13;
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:18;
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:45;
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:13;
assume |.(p - p3).| < a ; :: thesis: p3 in P
then dist u,u3 < a by JGRAPH_1:45;
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:45;
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 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)).| = (abs (1 - r)) * |.(p - p1).| by TOPRNS_1:8;
((1 - r) * p) + (r * p) = ((1 - r) + r) * p by EUCLID:37
.= p by EUCLID:33 ;
then |.(p - (((1 - r) * p1) + (r * p2))).| = |.(((((1 - r) * p) + (r * p)) - ((1 - r) * p1)) - (r * p2)).| by EUCLID:50
.= |.(((((1 - r) * p) + (- ((1 - r) * p1))) + (r * p)) + (- (r * p2))).| by EUCLID:30
.= |.((((1 - r) * p) + (- ((1 - r) * p1))) + ((r * p) + (- (r * p2)))).| by EUCLID:30
.= |.((((1 - r) * p) + ((1 - r) * (- p1))) + ((r * p) + (- (r * p2)))).| by EUCLID:44
.= |.(((1 - r) * (p - p1)) + ((r * p) + (- (r * p2)))).| by EUCLID:36
.= |.(((1 - r) * (p - p1)) + ((r * p) + (r * (- p2)))).| by EUCLID:44
.= |.(((1 - r) * (p - p1)) + (r * (p - p2))).| by EUCLID:36 ;
then A13: |.(p - (((1 - r) * p1) + (r * p2))).| <= |.((1 - r) * (p - p1)).| + |.(r * (p - p2)).| by TOPRNS_1:30;
A14: 1 - r >= 0 by A11, XREAL_1:50;
then A15: abs (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)).| = (abs r) * |.(p - p2).| & r = abs r ) by A10, ABSVALUE:def 1, TOPRNS_1:8;
0 <= abs r by COMPLEX1:132;
then A18: (abs r) * |.(p - p2).| <= (abs r) * a by A5, XREAL_1:66;
(abs (1 - r)) * |.(p - p1).| < (abs (1 - r)) * a by A7, A15, A16, XREAL_1:70;
then |.((1 - r) * (p - p1)).| + |.(r * (p - p2)).| < ((1 - r) * a) + (r * a) by A12, A15, A18, A17, XREAL_1:10;
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 < abs r by ABSVALUE:def 1;
then A19: (abs r) * |.(p - p2).| < (abs r) * a by A5, XREAL_1:70;
A20: r = abs r by A10, ABSVALUE:def 1;
( (abs (1 - r)) * |.(p - p1).| <= (abs (1 - r)) * a & |.(r * (p - p2)).| = (abs r) * |.(p - p2).| ) by A7, A14, A15, TOPRNS_1:8, XREAL_1:66;
then |.((1 - r) * (p - p1)).| + |.(r * (p - p2)).| < ((1 - r) * a) + (r * a) by A12, A15, A19, A20, XREAL_1:10;
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