let n be Nat; :: thesis: for V being Subset of (TopSpaceMetr (Euclid n)) st ( for e being Point of (Euclid n) st e in V holds
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= V ) ) holds
V is open
let V be Subset of (TopSpaceMetr (Euclid n)); :: thesis: ( ( for e being Point of (Euclid n) st e in V holds
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= V ) ) implies V is open )
assume A1: for e being Point of (Euclid n) st e in V holds
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= V ) ; :: thesis: V is open
for e being Point of (Euclid n) st e in V holds
ex r being Real st
( r > 0 & Ball (e,r) c= V )
proof
let e be Point of (Euclid n); :: thesis: ( e in V implies ex r being Real st
( r > 0 & Ball (e,r) c= V ) )
assume e in V ; :: thesis: ex r being Real st
( r > 0 & Ball (e,r) c= V )
then consider r being Real such that
A2: r > 0 and
A3: OpenHypercube (e,r) c= V by A1;
Ball (e,r) c= OpenHypercube (e,r) by Th22;
hence ex r being Real st
( r > 0 & Ball (e,r) c= V ) by A2, A3, XBOOLE_1:1; :: thesis: verum
end;
hence V is open by TOPMETR:15; :: thesis: verum