let r be real number ; for n being Element of NAT
for y, x 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 y, x being Point of (TOP-REAL n) st y in Sphere (x,r) holds
(LSeg (x,y)) \ {x,y} c= Ball (x,r)
let y, x 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, XBOOLE_1:2;
verum end; suppose A6:
r <> 0
;
(LSeg (x,y)) \ {x,y} c= Ball (x,r)let k be
set ;
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, JORDAN2C:7
.=
(((1 * x) - (l * x)) - x) + (l * y)
by EUCLID:50
.=
((x - (l * x)) - x) + (l * y)
by EUCLID:29
.=
((x - x) - (l * x)) + (l * y)
by TOPREAL9:1
.=
((0. (TOP-REAL n)) - (l * x)) + (l * y)
by EUCLID:42
.=
(l * y) - (l * x)
by EUCLID:27
.=
l * (y - x)
by EUCLID:49
;
then A12:
|.(k - x).| =
(abs 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;