let n be Element of NAT ; :: thesis: for x being Point of (TOP-REAL n)
for r being non zero Real holds Cl (Ball (x,r)) = cl_Ball (x,r)
let x be Point of (TOP-REAL n); :: thesis: for r being non zero Real holds Cl (Ball (x,r)) = cl_Ball (x,r)
let r be non zero Real; :: thesis: Cl (Ball (x,r)) = cl_Ball (x,r)
thus Cl (Ball (x,r)) c= cl_Ball (x,r) by TOPREAL9:16, TOPS_1:5; :: according to XBOOLE_0:def 10 :: thesis: cl_Ball (x,r) c= Cl (Ball (x,r))
per cases ( Ball (x,r) is empty or not Ball (x,r) is empty ) ;
suppose Ball (x,r) is empty ; :: thesis: cl_Ball (x,r) c= Cl (Ball (x,r))
then r < 0 ;
hence cl_Ball (x,r) c= Cl (Ball (x,r)) ; :: thesis: verum
end;
suppose A1: not Ball (x,r) is empty ; :: thesis: cl_Ball (x,r) c= Cl (Ball (x,r))
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in cl_Ball (x,r) or a in Cl (Ball (x,r)) )
assume A2: a in cl_Ball (x,r) ; :: thesis: a in Cl (Ball (x,r))
then reconsider a = a as Point of (TOP-REAL n) ;
reconsider ae = a as Point of (Euclid n) by TOPREAL3:8;
A3: 0 < r by A1;
for s being Real st 0 < s & s < r holds
Ball (ae,s) meets Ball (x,r)
proof
let s be Real; :: thesis: ( 0 < s & s < r implies Ball (ae,s) meets Ball (x,r) )
assume that
A4: 0 < s and
A5: s < r ; :: thesis: Ball (ae,s) meets Ball (x,r)
now :: thesis: Ball (a,s) meets Ball (x,r)
A6: (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r) by TOPREAL9:18;
per cases ( a in Ball (x,r) or a in Sphere (x,r) ) by A2, A6, XBOOLE_0:def 3;
suppose A7: a in Ball (x,r) ; :: thesis: Ball (a,s) meets Ball (x,r)
|.(a - a).| = 0 by TOPRNS_1:28;
then a in Ball (a,s) by A4, TOPREAL9:7;
hence Ball (a,s) meets Ball (x,r) by A7, XBOOLE_0:3; :: thesis: verum
end;
suppose A8: a in Sphere (x,r) ; :: thesis: Ball (a,s) meets Ball (x,r)
then A9: |.(a - x).| = r by TOPREAL9:9;
|.(x - x).| = 0 by TOPRNS_1:28;
then A10: x in Ball (x,r) by A3, TOPREAL9:7;
set z = s / (2 * r);
set q = ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x);
1 * r < 2 * r by A3, XREAL_1:68;
then s < 2 * r by A5, XXREAL_0:2;
then A11: s / (2 * r) < 1 by A4, XREAL_1:189;
0 < 2 * r by A3, XREAL_1:129;
then A12: 0 < s / (2 * r) by A4, XREAL_1:139;
A13: ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) in LSeg (a,x) by A3, A4, A11;
Ball (x,r) misses Sphere (x,r) by TOPREAL9:19;
then A14: a <> x by A8, A10, XBOOLE_0:3;
then A15: ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) <> a by A12, TOPREAL9:4;
((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) <> x by A11, A14, TOPREAL9:4;
then not ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) in {a,x} by A15, TARSKI:def 2;
then A16: ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) in (LSeg (a,x)) \ {a,x} by A13, XBOOLE_0:def 5;
A17: (LSeg (a,x)) \ {a,x} c= Ball (x,r) by A8, Th20;
(((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x)) - a = (((1 - (s / (2 * r))) * a) - a) + ((s / (2 * r)) * x) by RLVECT_1:def 3
.= (((1 * a) - ((s / (2 * r)) * a)) - a) + ((s / (2 * r)) * x) by RLVECT_1:35
.= ((a - ((s / (2 * r)) * a)) - a) + ((s / (2 * r)) * x) by RLVECT_1:def 8
.= ((a + (- ((s / (2 * r)) * a))) + (- a)) + ((s / (2 * r)) * x)
.= ((a + (- a)) + (- ((s / (2 * r)) * a))) + ((s / (2 * r)) * x) by RLVECT_1:def 3
.= ((a - a) - ((s / (2 * r)) * a)) + ((s / (2 * r)) * x)
.= ((0. (TOP-REAL n)) - ((s / (2 * r)) * a)) + ((s / (2 * r)) * x) by RLVECT_1:5
.= ((s / (2 * r)) * x) - ((s / (2 * r)) * a) by RLVECT_1:4
.= (s / (2 * r)) * (x - a) by RLVECT_1:34 ;
then |.((((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x)) - a).| = |.(s / (2 * r)).| * |.(x - a).| by TOPRNS_1:7
.= (s / (2 * r)) * |.(x - a).| by A3, A4, ABSVALUE:def 1
.= (s / (2 * r)) * |.(a - x).| by TOPRNS_1:27
.= s / 2 by A9, XCMPLX_1:92 ;
then A18: ((1 - (s / (2 * r))) * a) + ((s / (2 * r)) * x) in Sphere (a,(s / 2)) by TOPREAL9:9;
s / 2 < s / 1 by A4, XREAL_1:76;
then Sphere (a,(s / 2)) c= Ball (a,s) by Th22;
hence Ball (a,s) meets Ball (x,r) by A16, A17, A18, XBOOLE_0:3; :: thesis: verum
end;
end;
end;
hence Ball (ae,s) meets Ball (x,r) by TOPREAL9:13; :: thesis: verum
end;
hence a in Cl (Ball (x,r)) by A3, GOBOARD6:93; :: thesis: verum
end;
end;