let X be RealNormSpace; :: thesis: for x being Point of X
for r being real number
for V being Subset of (LinearTopSpaceNorm X) st V = Ball x,r holds
V is convex
let x be Point of X; :: thesis: for r being real number
for V being Subset of (LinearTopSpaceNorm X) st V = Ball x,r holds
V is convex
let r be real number ; :: thesis: for V being Subset of (LinearTopSpaceNorm X) st V = Ball x,r holds
V is convex
let V be Subset of (LinearTopSpaceNorm X); :: thesis: ( V = Ball x,r implies V is convex )
assume A1: V = Ball x,r ; :: thesis: V is convex
reconsider V1 = Ball x,r as Subset of X ;
K2: for u, v being Point of X
for s being Real st 0 < s & s < 1 & u in V1 & v in V1 holds
(s * u) + ((1 - s) * v) in V1

proof

let u, v be Point of X; :: thesis: for s being Real st 0 < s & s < 1 & u in V1 & v in V1 holds
(s * u) + ((1 - s) * v) in V1
let s be Real; :: thesis: ( 0 < s & s < 1 & u in V1 & v in V1 implies (s * u) + ((1 - s) * v) in V1 )
assume A2: ( 0 < s & s < 1 & u in V1 & v in V1 ) ; :: thesis: (s * u) + ((1 - s) * v) in V1
s + 0 < 1 by A2;
then AX1: 1 - s > 0 by XREAL_1:22;
A4: ||.(((s * x) + ((1 - s) * x)) - ((s * u) + ((1 - s) * v))).|| = ||.(((s * x) + (- ((s * u) + ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:def 6
.= ||.(((s * x) + ((- 1) * ((s * u) + ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:29
.= ||.(((s * x) + (((- 1) * (s * u)) + ((- 1) * ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:def 9
.= ||.(((s * x) + ((- (s * u)) + ((- 1) * ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:29
.= ||.(((s * x) + ((- (s * u)) + (- ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:29
.= ||.((((s * x) + (- (s * u))) + (- ((1 - s) * v))) + ((1 - s) * x)).|| by RLVECT_1:def 6
.= ||.(((s * x) - (s * u)) + (((1 - s) * x) - ((1 - s) * v))).|| by RLVECT_1:def 6
.= ||.((s * (x - u)) + (((1 - s) * x) - ((1 - s) * v))).|| by RLVECT_1:48
.= ||.((s * (x - u)) + ((1 - s) * (x - v))).|| by RLVECT_1:48 ;
A7: 0 < abs s by A2, ABSVALUE:def 1;
A8: 0 < abs (1 - s) by AX1, ABSVALUE:def 1;
AZ1: ex u1 being Point of X st
( u = u1 & ||.(x - u1).|| < r ) by A2;
ex v1 being Point of X st
( v = v1 & ||.(x - v1).|| < r ) by A2;
then ( (abs s) * ||.(x - u).|| < (abs s) * r & (abs (1 - s)) * ||.(x - v).|| < (abs (1 - s)) * r ) by A7, A8, AZ1, XREAL_1:70;
then ((abs s) * ||.(x - u).||) + ((abs (1 - s)) * ||.(x - v).||) < ((abs s) * r) + ((abs (1 - s)) * r) by XREAL_1:10;
then ((abs s) * ||.(x - u).||) + ((abs (1 - s)) * ||.(x - v).||) < (s * r) + ((abs (1 - s)) * r) by A2, ABSVALUE:def 1;
then ((abs s) * ||.(x - u).||) + ((abs (1 - s)) * ||.(x - v).||) < (s * r) + ((1 - s) * r) by AX1, ABSVALUE:def 1;
then ||.(s * (x - u)).|| + ((abs (1 - s)) * ||.(x - v).||) < 1 * r by NORMSP_1:def 2;
then A9: ||.(s * (x - u)).|| + ||.((1 - s) * (x - v)).|| < r by NORMSP_1:def 2;
||.(((s * x) + ((1 - s) * x)) - ((s * u) + ((1 - s) * v))).|| <= ||.(s * (x - u)).|| + ||.((1 - s) * (x - v)).|| by A4, NORMSP_1:def 2;
then ||.(((s * x) + ((1 - s) * x)) - ((s * u) + ((1 - s) * v))).|| < r by A9, XXREAL_0:2;
then ||.(((s + (1 - s)) * x) - ((s * u) + ((1 - s) * v))).|| < r by RLVECT_1:def 9;
then ||.(x - ((s * u) + ((1 - s) * v))).|| < r by RLVECT_1:def 9;
hence (s * u) + ((1 - s) * v) in V1 ; :: thesis: verum

end;

for u, v being Point of (LinearTopSpaceNorm X)
for s being Real st 0 < s & s < 1 & u in V & v in V holds
(s * u) + ((1 - s) * v) in V

proof

let u, v be Point of (LinearTopSpaceNorm X); :: thesis: for s being Real st 0 < s & s < 1 & u in V & v in V holds
(s * u) + ((1 - s) * v) in V
let s be Real; :: thesis: ( 0 < s & s < 1 & u in V & v in V implies (s * u) + ((1 - s) * v) in V )
assume ASV: ( 0 < s & s < 1 & u in V & v in V ) ; :: thesis: (s * u) + ((1 - s) * v) in V
reconsider u1 = u as Point of X by NORMSP_2:def 4;
reconsider v1 = v as Point of X by NORMSP_2:def 4;
L2: s * u1 = s * u by NORMSP_2:def 4;
L3: (1 - s) * v1 = (1 - s) * v by NORMSP_2:def 4;
(s * u1) + ((1 - s) * v1) = (s * u) + ((1 - s) * v) by L2, L3, NORMSP_2:def 4;
hence (s * u) + ((1 - s) * v) in V by A1, K2, ASV; :: thesis: verum

end;

hence V is convex by CONVEX1:def 2; :: thesis: verum