let V be RealUnitarySpace; for M being Subset of (TopUnitSpace V)
for v being VECTOR of V
for r being Real st M = Sphere (v,r) holds
M is closed
let M be Subset of (TopUnitSpace V); for v being VECTOR of V
for r being Real st M = Sphere (v,r) holds
M is closed
let v be VECTOR of V; for r being Real st M = Sphere (v,r) holds
M is closed
let r be Real; ( M = Sphere (v,r) implies M is closed )
reconsider B = cl_Ball (v,r), C = Ball (v,r) as Subset of (TopUnitSpace V) ;
assume A1:
M = Sphere (v,r)
; M is closed
A2:
M ` = (B `) \/ C
proof
hereby XBOOLE_0:def 10,
TARSKI:def 3 (B `) \/ C c= M `
let a be
object ;
( a in M ` implies a in (B `) \/ C )assume A3:
a in M `
;
a in (B `) \/ Cthen reconsider e =
a as
Point of
V ;
not
a in M
by A3, XBOOLE_0:def 5;
then
dist (
e,
v)
<> r
by A1, BHSP_2:52;
then
(
dist (
e,
v)
< r or
dist (
e,
v)
> r )
by XXREAL_0:1;
then
(
e in Ball (
v,
r) or not
e in cl_Ball (
v,
r) )
by BHSP_2:41, BHSP_2:48;
then
(
e in Ball (
v,
r) or
e in (cl_Ball (v,r)) ` )
by SUBSET_1:29;
hence
a in (B `) \/ C
by XBOOLE_0:def 3;
verum
end;
let a be
object ;
TARSKI:def 3 ( not a in (B `) \/ C or a in M ` )
assume A4:
a in (B `) \/ C
;
a in M `
then reconsider e =
a as
Point of
V ;
(
a in B ` or
a in C )
by A4, XBOOLE_0:def 3;
then
( not
e in cl_Ball (
v,
r) or
e in C )
by XBOOLE_0:def 5;
then
(
dist (
e,
v)
> r or
dist (
e,
v)
< r )
by BHSP_2:41, BHSP_2:48;
then
not
a in M
by A1, BHSP_2:52;
hence
a in M `
by A4, SUBSET_1:29;
verum
end;
( B is closed & C is open )
by Th50, Th53;
hence
M is closed
by A2; verum