let r be Real; for n being Element of NAT
for x, y being Point of (TOP-REAL n) st y in Sphere (x,r) holds
(LSeg (x,y)) \ {x,y} c= Ball (x,r)
let n be Element of NAT ; for x, y being Point of (TOP-REAL n) st y in Sphere (x,r) holds
(LSeg (x,y)) \ {x,y} c= Ball (x,r)
let x, y be Point of (TOP-REAL n); ( y in Sphere (x,r) implies (LSeg (x,y)) \ {x,y} c= Ball (x,r) )
assume A1:
y in Sphere (x,r)
; (LSeg (x,y)) \ {x,y} c= Ball (x,r)
per cases
( r = 0 or r <> 0 )
;
suppose A2:
r = 0
;
(LSeg (x,y)) \ {x,y} c= Ball (x,r)reconsider xe =
x as
Point of
(Euclid n) by TOPREAL3:8;
Sphere (
x,
r)
= Sphere (
xe,
r)
by TOPREAL9:15;
then
Sphere (
x,
r)
= {x}
by A2, TOPREAL6:54;
then A3:
x = y
by A1, TARSKI:def 1;
A4:
LSeg (
x,
x)
= {x}
by RLTOPSP1:70;
A5:
{x,x} = {x}
by ENUMSET1:29;
{x} \ {x} = {}
by XBOOLE_1:37;
hence
(LSeg (x,y)) \ {x,y} c= Ball (
x,
r)
by A3, A4, A5;
verum end; suppose A6:
r <> 0
;
(LSeg (x,y)) \ {x,y} c= Ball (x,r)let k be
object ;
TARSKI:def 3 ( not k in (LSeg (x,y)) \ {x,y} or k in Ball (x,r) )assume A7:
k in (LSeg (x,y)) \ {x,y}
;
k in Ball (x,r)then
k in LSeg (
x,
y)
by XBOOLE_0:def 5;
then consider l being
Real such that A8:
k = ((1 - l) * x) + (l * y)
and A9:
0 <= l
and A10:
l <= 1
;
reconsider k =
k as
Point of
(TOP-REAL n) by A8;
not
k in {x,y}
by A7, XBOOLE_0:def 5;
then
k <> y
by TARSKI:def 2;
then
l <> 1
by A8, TOPREAL9:4;
then A11:
l < 1
by A10, XXREAL_0:1;
k - x =
(((1 - l) * x) - x) + (l * y)
by A8, RLVECT_1:def 3
.=
(((1 * x) - (l * x)) - x) + (l * y)
by RLVECT_1:35
.=
((x - (l * x)) - x) + (l * y)
by RLVECT_1:def 8
.=
((x + (- (l * x))) + (- x)) + (l * y)
.=
((x + (- x)) + (- (l * x))) + (l * y)
by RLVECT_1:def 3
.=
((x - x) - (l * x)) + (l * y)
.=
((0. (TOP-REAL n)) - (l * x)) + (l * y)
by RLVECT_1:5
.=
(l * y) - (l * x)
by RLVECT_1:4
.=
l * (y - x)
by RLVECT_1:34
;
then A12:
|.(k - x).| =
|.l.| * |.(y - x).|
by TOPRNS_1:7
.=
l * |.(y - x).|
by A9, ABSVALUE:def 1
.=
l * r
by A1, TOPREAL9:9
;
0 <= r
by A1;
then
l * r < 1
* r
by A6, A11, XREAL_1:68;
hence
k in Ball (
x,
r)
by A12, TOPREAL9:7;
verum end;