let n be Nat; for r being real number
for e1, e being Point of (Euclid n) st e1 in Ball e,r holds
ex m being non zero Element of NAT st OpenHypercube e1,(1 / m) c= Ball e,r
let r be real number ; for e1, e being Point of (Euclid n) st e1 in Ball e,r holds
ex m being non zero Element of NAT st OpenHypercube e1,(1 / m) c= Ball e,r
let e1, e be Point of (Euclid n); ( e1 in Ball e,r implies ex m being non zero Element of NAT st OpenHypercube e1,(1 / m) c= Ball e,r )
reconsider B = Ball e,r as Subset of (TopSpaceMetr (Euclid n)) ;
assume A1:
e1 in Ball e,r
; ex m being non zero Element of NAT st OpenHypercube e1,(1 / m) c= Ball e,r
B is open
by TOPMETR:21;
then consider s being real number such that
A2:
s > 0
and
A3:
Ball e1,s c= B
by A1, TOPMETR:22;
A4:
s / (sqrt n) is Real
by XREAL_0:def 1;
per cases
( n <> 0 or n = 0 )
;
suppose A5:
n <> 0
;
ex m being non zero Element of NAT st OpenHypercube e1,(1 / m) c= Ball e,rthen consider m being
Element of
NAT such that A6:
1
/ m < s / (sqrt n)
and A7:
m > 0
by A2, A4, FRECHET:40;
reconsider m =
m as non
zero Element of
NAT by A7;
A8:
OpenHypercube e1,
(s / (sqrt n)) c= Ball e1,
s
by A5, Th17;
OpenHypercube e1,
(1 / m) c= OpenHypercube e1,
(s / (sqrt n))
by A6, Th13;
then
OpenHypercube e1,
(1 / m) c= Ball e1,
s
by A8, XBOOLE_1:1;
hence
ex
m being non
zero Element of
NAT st
OpenHypercube e1,
(1 / m) c= Ball e,
r
by A3, XBOOLE_1:1;
verum end;