let n be Nat; :: thesis: for r being Real
for e, e1 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; :: thesis: for e, e1 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 e, e1 be Point of (Euclid n); :: thesis: ( 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) ; :: thesis: 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 such that
A2: s > 0 and
A3: Ball (e1,s) c= B by A1, TOPMETR:15;
per cases ( n <> 0 or n = 0 ) ;
suppose A4: n <> 0 ; :: thesis: ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r)
then consider m being Nat such that
A5: 1 / m < s / (sqrt n) and
A6: m > 0 by A2, FRECHET:36;
reconsider m = m as non zero Element of NAT by A6, ORDINAL1:def 12;
A7: OpenHypercube (e1,(s / (sqrt n))) c= Ball (e1,s) by A4, Th17;
OpenHypercube (e1,(1 / m)) c= OpenHypercube (e1,(s / (sqrt n))) by A5, Th13;
then OpenHypercube (e1,(1 / m)) c= Ball (e1,s) by A7;
hence ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r) by A3, XBOOLE_1:1; :: thesis: verum
end;
suppose n = 0 ; :: thesis: ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r)
then ( ( OpenHypercube (e1,(1 / 1)) = {} or OpenHypercube (e1,(1 / 1)) = {{}} ) & Ball (e,r) = {{}} ) by A1, EUCLID:77, ZFMISC_1:33;
hence ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r) ; :: thesis: verum
end;
end;