let V be RealUnitarySpace; :: thesis: 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); :: thesis: 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; :: thesis: for r being Real st M = Sphere v,r holds
M is closed
let r be Real; :: thesis: ( M = Sphere v,r implies M is closed )
assume A1:
M = Sphere v,r
; :: thesis: M is closed
reconsider B = cl_Ball v,r, C = Ball v,r as Subset of (TopUnitSpace V) ;
A2:
M ` = (B ` ) \/ C
proof
hereby :: according to XBOOLE_0:def 10,
TARSKI:def 3 :: thesis: (B ` ) \/ C c= M `
let a be
set ;
:: thesis: ( a in M ` implies a in (B ` ) \/ C )assume A3:
a in M `
;
:: thesis: 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:50;
hence
a in (B ` ) \/ C
by XBOOLE_0:def 3;
:: thesis: verum
end;
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in (B ` ) \/ C or a in M ` )
assume A4:
a in (B ` ) \/ C
;
:: thesis: 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:50;
:: thesis: verum
end;
( B is closed & C is open )
by Th50, Th53;
then
( B ` is open & C is open )
;
then
M ` is open
by A2, TOPS_1:37;
hence
M is closed
by TOPS_1:29; :: thesis: verum