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
let p1,
p2 be
Point of
(TOP-REAL n);
:: thesis: ( p1 in P & p2 in P implies LSeg p1,p2 c= P )
assume A2:
(
p1 in P &
p2 in P )
;
:: thesis: LSeg p1,p2 c= P
A3:
P = { q where q is Element of (Euclid n) : dist u,q < a }
by A1, METRIC_1:18;
then consider q1 being
Point of
(Euclid n) such that A4:
(
q1 = p1 &
dist u,
q1 < a )
by A2;
reconsider p =
u as
Point of
(TOP-REAL n) by TOPREAL3:13;
A5:
|.(p - p1).| < a
by A4, JGRAPH_1:45;
consider q2 being
Point of
(Euclid n) such that A6:
(
q2 = p2 &
dist u,
q2 < a )
by A2, A3;
A7:
|.(p - p2).| < a
by A6, JGRAPH_1:45;
A8:
for
p3 being
Point of
(TOP-REAL n) st
|.(p - p3).| < a holds
p3 in P
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 A10:
x in LSeg p1,
p2
;
:: thesis: x in P
then
x in { (((1 - r) * p1) + (r * p2)) where r is Real : ( 0 <= r & r <= 1 ) }
;
then consider r being
Real such that A11:
(
x = ((1 - r) * p1) + (r * p2) &
0 <= r &
r <= 1 )
;
reconsider q =
x as
Point of
(TOP-REAL n) by A10;
((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 A12:
|.(p - (((1 - r) * p1) + (r * p2))).| <= |.((1 - r) * (p - p1)).| + |.(r * (p - p2)).|
by TOPRNS_1:30;
A13:
|.((1 - r) * (p - p1)).| = (abs (1 - r)) * |.(p - p1).|
by TOPRNS_1:8;
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
1
- r > 0
;
:: thesis: x in Pthen A16:
(abs (1 - r)) * |.(p - p1).| < (abs (1 - r)) * a
by A5, A15, XREAL_1:70;
A17:
|.(r * (p - p2)).| = (abs r) * |.(p - p2).|
by TOPRNS_1:8;
0 <= abs r
by COMPLEX1:132;
then A18:
(abs r) * |.(p - p2).| <= (abs r) * a
by A7, XREAL_1:66;
r = abs r
by A11, ABSVALUE:def 1;
then
|.((1 - r) * (p - p1)).| + |.(r * (p - p2)).| < ((1 - r) * a) + (r * a)
by A13, A15, A16, A17, A18, XREAL_1:10;
then
|.(p - q).| < a
by A11, A12, XXREAL_0:2;
hence
x in P
by A8;
:: thesis: verum end; suppose
1
- r <= 0
;
:: thesis: x in Pthen A19:
(1 - r) + r = 0 + r
by A14;
A20:
(abs (1 - r)) * |.(p - p1).| <= (abs (1 - r)) * a
by A5, A14, A15, XREAL_1:66;
A21:
|.(r * (p - p2)).| = (abs r) * |.(p - p2).|
by TOPRNS_1:8;
0 < abs r
by A19, ABSVALUE:def 1;
then A22:
(abs r) * |.(p - p2).| < (abs r) * a
by A7, XREAL_1:70;
r = abs r
by A11, ABSVALUE:def 1;
then
|.((1 - r) * (p - p1)).| + |.(r * (p - p2)).| < ((1 - r) * a) + (r * a)
by A13, A15, A20, A21, A22, XREAL_1:10;
then
|.(p - q).| < a
by A11, A12, XXREAL_0:2;
hence
x in P
by A8;
:: thesis: verum end;
end;
hence
LSeg p1,
p2 c= P
;
:: thesis: verum
end;
hence
P is convex
by JORDAN1:def 1; :: thesis: verum