let X be RealNormSpace; :: thesis: for x being Point of X
for r being Real
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
for V being Subset of (LinearTopSpaceNorm X) st V = Ball (x,r) holds
V is convex
let r be Real; :: 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 )
reconsider V1 = Ball (x,r) as Subset of X ;
A1: 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 that
A2: 0 < s and
A3: s < 1 and
A4: u in V1 and
A5: v in V1 ; :: thesis: (s * u) + ((1 - s) * v) in V1
A6: ex v1 being Point of X st
( v = v1 & ||.(x - v1).|| < r ) by A5;
( 0 < |.s.| & ex u1 being Point of X st
( u = u1 & ||.(x - u1).|| < r ) ) by A2, A4, ABSVALUE:def 1;
then A7: |.s.| * ||.(x - u).|| < |.s.| * r by XREAL_1:68;
s + 0 < 1 by A3;
then A8: 1 - s > 0 by XREAL_1:20;
then 0 < |.(1 - s).| by ABSVALUE:def 1;
then |.(1 - s).| * ||.(x - v).|| < |.(1 - s).| * r by A6, XREAL_1:68;
then (|.s.| * ||.(x - u).||) + (|.(1 - s).| * ||.(x - v).||) < (|.s.| * r) + (|.(1 - s).| * r) by A7, XREAL_1:8;
then (|.s.| * ||.(x - u).||) + (|.(1 - s).| * ||.(x - v).||) < (s * r) + (|.(1 - s).| * r) by A2, ABSVALUE:def 1;
then (|.s.| * ||.(x - u).||) + (|.(1 - s).| * ||.(x - v).||) < (s * r) + ((1 - s) * r) by A8, ABSVALUE:def 1;
then ||.(s * (x - u)).|| + (|.(1 - s).| * ||.(x - v).||) < 1 * r by NORMSP_1:def 1;
then A9: ||.(s * (x - u)).|| + ||.((1 - s) * (x - v)).|| < r by NORMSP_1:def 1;
||.(((s * x) + ((1 - s) * x)) - ((s * u) + ((1 - s) * v))).|| = ||.(((s * x) + (- ((s * u) + ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:def 3
.= ||.(((s * x) + ((- 1) * ((s * u) + ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:16
.= ||.(((s * x) + (((- 1) * (s * u)) + ((- 1) * ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:def 5
.= ||.(((s * x) + ((- (s * u)) + ((- 1) * ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:16
.= ||.(((s * x) + ((- (s * u)) + (- ((1 - s) * v)))) + ((1 - s) * x)).|| by RLVECT_1:16
.= ||.((((s * x) + (- (s * u))) + (- ((1 - s) * v))) + ((1 - s) * x)).|| by RLVECT_1:def 3
.= ||.(((s * x) - (s * u)) + (((1 - s) * x) - ((1 - s) * v))).|| by RLVECT_1:def 3
.= ||.((s * (x - u)) + (((1 - s) * x) - ((1 - s) * v))).|| by RLVECT_1:34
.= ||.((s * (x - u)) + ((1 - s) * (x - v))).|| by RLVECT_1:34 ;
then ||.(((s * x) + ((1 - s) * x)) - ((s * u) + ((1 - s) * v))).|| <= ||.(s * (x - u)).|| + ||.((1 - s) * (x - v)).|| by NORMSP_1:def 1;
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 6;
then ||.(x - ((s * u) + ((1 - s) * v))).|| < r by RLVECT_1:def 8;
hence (s * u) + ((1 - s) * v) in V1 ; :: thesis: verum

end;

assume A10: V = Ball (x,r) ; :: thesis: V is convex
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 )
reconsider u1 = u as Point of X by NORMSP_2:def 4;
reconsider v1 = v as Point of X by NORMSP_2:def 4;
( s * u1 = s * u & (1 - s) * v1 = (1 - s) * v ) by NORMSP_2:def 4;
then A11: (s * u1) + ((1 - s) * v1) = (s * u) + ((1 - s) * v) by NORMSP_2:def 4;
assume ( 0 < s & s < 1 & u in V & v in V ) ; :: thesis: (s * u) + ((1 - s) * v) in V
hence (s * u) + ((1 - s) * v) in V by A10, A1, A11; :: thesis: verum

end;

hence V is convex ; :: thesis: verum