let n be Element of NAT ; :: thesis: for p being Point of (Euclid n)
for r being Real
for B being Subset of (TOP-REAL n) st B = cl_Ball (p,r) holds
( B is bounded & B is closed )
let p be Point of (Euclid n); :: thesis: for r being Real
for B being Subset of (TOP-REAL n) st B = cl_Ball (p,r) holds
( B is bounded & B is closed )
let r be Real; :: thesis: for B being Subset of (TOP-REAL n) st B = cl_Ball (p,r) holds
( B is bounded & B is closed )
let B be Subset of (TOP-REAL n); :: thesis: ( B = cl_Ball (p,r) implies ( B is bounded & B is closed ) )
assume A1: B = cl_Ball (p,r) ; :: thesis: ( B is bounded & B is closed )
cl_Ball (p,r) c= Ball (p,(r + 1))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in cl_Ball (p,r) or x in Ball (p,(r + 1)) )
A2: r < r + 1 by XREAL_1:29;
assume A3: x in cl_Ball (p,r) ; :: thesis: x in Ball (p,(r + 1))
then reconsider q = x as Point of (Euclid n) ;
dist (p,q) <= r by A3, METRIC_1:12;
then dist (p,q) < r + 1 by A2, XXREAL_0:2;
hence x in Ball (p,(r + 1)) by METRIC_1:11; :: thesis: verum
end;
then cl_Ball (p,r) is bounded by TBSP_1:14;
hence B is bounded by A1, JORDAN2C:11; :: thesis: B is closed
A4: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider BB = B as Subset of (TopSpaceMetr (Euclid n)) ;
BB is closed by A1, TOPREAL6:57;
hence B is closed by A4, PRE_TOPC:31; :: thesis: verum