let n be Nat; :: thesis: 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; :: thesis: 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); :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum