let n be Nat; for A being Subset of (TOP-REAL n)
for a being bounded Subset of (Euclid n) st a = A holds
for p being Point of (Euclid n) st p in conv A holds
conv A c= cl_Ball (p,(diameter a))
let A be Subset of (TOP-REAL n); for a being bounded Subset of (Euclid n) st a = A holds
for p being Point of (Euclid n) st p in conv A holds
conv A c= cl_Ball (p,(diameter a))
A1:
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n)
by EUCLID:def 8;
let a be bounded Subset of (Euclid n); ( a = A implies for p being Point of (Euclid n) st p in conv A holds
conv A c= cl_Ball (p,(diameter a)) )
assume A2:
A = a
; for p being Point of (Euclid n) st p in conv A holds
conv A c= cl_Ball (p,(diameter a))
let x be Point of (Euclid n); ( x in conv A implies conv A c= cl_Ball (x,(diameter a)) )
assume A3:
x in conv A
; conv A c= cl_Ball (x,(diameter a))
A4:
A c= cl_Ball (x,(diameter a))
proof
let p be
object ;
TARSKI:def 3 ( not p in A or p in cl_Ball (x,(diameter a)) )
assume A5:
p in A
;
p in cl_Ball (x,(diameter a))
then reconsider p =
p as
Point of
(Euclid n) by A2;
reconsider pp =
p as
Point of
(TOP-REAL n) by A1;
A6:
cl_Ball (
p,
(diameter a))
= cl_Ball (
pp,
(diameter a))
by TOPREAL9:14;
A c= cl_Ball (
p,
(diameter a))
then
conv A c= cl_Ball (
pp,
(diameter a))
by A6, CONVEX1:30;
then
dist (
p,
x)
<= diameter a
by A3, A6, METRIC_1:12;
hence
p in cl_Ball (
x,
(diameter a))
by METRIC_1:12;
verum
end;
reconsider xx = x as Point of (TOP-REAL n) by A1;
cl_Ball (x,(diameter a)) = cl_Ball (xx,(diameter a))
by TOPREAL9:14;
hence
conv A c= cl_Ball (x,(diameter a))
by A4, CONVEX1:30; verum