let n be Nat; for r being Real
for e, e1 being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds
dist (e1,e) < r * (sqrt n)
let r be Real; for e, e1 being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds
dist (e1,e) < r * (sqrt n)
let e, e1 be Point of (Euclid n); ( n <> 0 & e1 in OpenHypercube (e,r) implies dist (e1,e) < r * (sqrt n) )
assume that
A1:
n <> 0
and
A2:
e1 in OpenHypercube (e,r)
; dist (e1,e) < r * (sqrt n)
A3:
dist (e1,e) = |.(e1 - e).|
by EUCLID:def 6;
0 <= Sum (sqr (e1 - e))
by RVSUM_1:86;
then A4:
sqrt (Sum (sqr (e1 - e))) < sqrt (n * (r ^2))
by A1, A2, Th15, SQUARE_1:27;
0 <= r
by A1, A2;
then
sqrt (r ^2) = r
by SQUARE_1:22;
hence
dist (e1,e) < r * (sqrt n)
by A3, A4, SQUARE_1:29; verum