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:14;
then consider s being real number such that
A2:
s > 0
and
A3:
Ball (e1,s) c= B
by A1, TOPMETR:15;
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,r)then consider m being
Element of
NAT such that A6:
1
/ m < s / (sqrt n)
and A7:
m > 0
by A2, A4, FRECHET:36;
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;