let n be Nat; for V being Subset of (TopSpaceMetr (Euclid n)) st V is open holds
for e being Point of (Euclid n) st e in V holds
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= V )
let V be Subset of (TopSpaceMetr (Euclid n)); ( V is open implies for e being Point of (Euclid n) st e in V holds
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= V ) )
assume A1:
V is open
; for e being Point of (Euclid n) st e in V holds
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= V )
let e be Point of (Euclid n); ( e in V implies ex r being Real st
( r > 0 & OpenHypercube (e,r) c= V ) )
assume
e in V
; ex r being Real st
( r > 0 & OpenHypercube (e,r) c= V )
then consider r being Real such that
A2:
r > 0
and
A3:
Ball (e,r) c= V
by A1, TOPMETR:15;
per cases
( n <> 0 or n = 0 )
;
suppose A5:
n = 0
;
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= V )set TR =
TOP-REAL 0;
set Z =
0. (TOP-REAL 0);
A6:
OpenHypercube (
e,1)
= {(0. (TOP-REAL 0))}
by EUCLID_9:12, A5;
A7:
the
carrier of
(TOP-REAL 0) = REAL 0
by EUCLID:22;
the
carrier of
(Euclid 0) = the
carrier of
(TOP-REAL 0)
by EUCLID:67;
then
(
Ball (
e,
r)
= {} or
Ball (
e,
r)
= {(0. (TOP-REAL 0))} )
by A7, EUCLID:77, ZFMISC_1:33, A5;
hence
ex
r being
Real st
(
r > 0 &
OpenHypercube (
e,
r)
c= V )
by A6, A2, A3;
verum end;