let n be Nat; for p being Point of (TOP-REAL n)
for r being Real st r > 0 holds
Fr (cl_Ball (p,r)) = Sphere (p,r)
let p be Point of (TOP-REAL n); for r being Real st r > 0 holds
Fr (cl_Ball (p,r)) = Sphere (p,r)
let r be Real; ( r > 0 implies Fr (cl_Ball (p,r)) = Sphere (p,r) )
set TR = TOP-REAL n;
assume A1:
r > 0
; Fr (cl_Ball (p,r)) = Sphere (p,r)
set CB = cl_Ball (p,r);
set B = Ball (p,r);
set S = Sphere (p,r);
reconsider tr = TOP-REAL n as TopSpace ;
reconsider cb = cl_Ball (p,r) as Subset of tr ;
A2:
Ball (p,r) misses Sphere (p,r)
by TOPREAL9:19;
A3:
(Ball (p,r)) \/ (Sphere (p,r)) = cl_Ball (p,r)
by TOPREAL9:18;
A4:
Int cb c= Ball (p,r)
proof
reconsider ONE = 1 as
Real ;
let x be
object ;
TARSKI:def 3 ( not x in Int cb or x in Ball (p,r) )
assume
x in Int cb
;
x in Ball (p,r)
then consider Q being
Subset of
(TOP-REAL n) such that A5:
Q is
open
and A6:
Q c= cl_Ball (
p,
r)
and A7:
x in Q
by TOPS_1:22;
reconsider q =
x as
Point of
(TOP-REAL n) by A7;
consider w being
positive Real such that A8:
Ball (
q,
w)
c= Q
by A5, A7, TOPS_4:2;
assume
not
x in Ball (
p,
r)
;
contradiction
then
q in Sphere (
p,
r)
by A3, A6, A7, XBOOLE_0:def 3;
then A9:
|.(q - p).| = r
by TOPREAL9:9;
set w2 =
w / 2;
set wr =
((w / 2) / r) * (q - p);
A10:
|.((w / 2) / r).| = (w / 2) / r
by A1, ABSVALUE:def 1;
A11:
((((w / 2) / r) * (q - p)) + q) - p =
(((w / 2) / r) * (q - p)) + (q - p)
by RLVECT_1:28
.=
(((w / 2) / r) * (q - p)) + (ONE * (q - p))
by RLVECT_1:def 8
.=
(((w / 2) / r) + ONE) * (q - p)
by RLVECT_1:def 6
;
|.(((((w / 2) / r) * (q - p)) + q) - q).| =
|.((((w / 2) / r) * (q - p)) + (q - q)).|
by RLVECT_1:def 3
.=
|.((((w / 2) / r) * (q - p)) + (0. (TOP-REAL n))).|
by RLVECT_1:15
.=
|.(((w / 2) / r) * (q - p)).|
.=
((w / 2) / r) * r
by A9, A10, TOPRNS_1:7
.=
w / 2
by A1, XCMPLX_1:87
;
then
|.(((((w / 2) / r) * (q - p)) + q) - q).| < w
by XREAL_1:216;
then
(((w / 2) / r) * (q - p)) + q in Ball (
q,
w)
;
then A12:
(((w / 2) / r) * (q - p)) + q in Q
by A8;
A13:
((w / 2) / r) + ONE =
((w / 2) / r) + (r / r)
by A1, XCMPLX_1:60
.=
((w / 2) + r) / r
;
A14:
(w / 2) + r > 0 + r
by XREAL_1:6;
|.(((w / 2) + r) / r).| = ((w / 2) + r) / r
by A1, ABSVALUE:def 1;
then |.(((((w / 2) / r) * (q - p)) + q) - p).| =
(((w / 2) + r) / r) * r
by A9, A13, A11, TOPRNS_1:7
.=
(w / 2) + r
by A1, XCMPLX_1:87
;
hence
contradiction
by A6, A12, A14, TOPREAL9:8;
verum
end;
Ball (p,r) c= Int cb
by TOPREAL9:16, TOPS_1:24;
then
Int cb = Ball (p,r)
by A4, XBOOLE_0:def 10;
then
Fr (cl_Ball (p,r)) = (cl_Ball (p,r)) \ (Ball (p,r))
by TOPS_1:43;
hence
Fr (cl_Ball (p,r)) = Sphere (p,r)
by A3, A2, XBOOLE_1:88; verum