let n be Nat; :: thesis: for r being real number
for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube e,r holds
dist e1,e < r * (sqrt n)
let r be real number ; :: thesis: for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube e,r holds
dist e1,e < r * (sqrt n)
let e1, e 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:116;
then A4: sqrt (Sum (sqr (e1 - e))) < sqrt (n * (r ^2 )) by A1, A2, Th15, SQUARE_1:95;
0 <= r by A1, A2;
then sqrt (r ^2 ) = r by SQUARE_1:89;
hence dist e1,e < r * (sqrt n) by A3, A4, SQUARE_1:97; :: thesis: verum