let X, Y be RealNormSpace; for V being Subset of [:X,Y:] holds
( V is open iff for x being Point of X
for y being Point of Y st [x,y] in V holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) )
let V be Subset of [:X,Y:]; ( V is open iff for x being Point of X
for y being Point of Y st [x,y] in V holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) )
hereby ( ( for x being Point of X
for y being Point of Y st [x,y] in V holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) ) implies V is open )
assume A1:
V is
open
;
for x being Point of X
for y being Point of Y st [x,y] in V holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V )let x be
Point of
X;
for y being Point of Y st [x,y] in V holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V )let y be
Point of
Y;
( [x,y] in V implies ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) )assume
[x,y] in V
;
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V )then consider r being
Real such that A2:
(
0 < r &
[:(Ball (x,r)),(Ball (y,r)):] c= V )
by A1, NDIFF_8:23;
thus
ex
r1,
r2 being
Real st
(
0 < r1 &
0 < r2 &
[:(Ball (x,r1)),(Ball (y,r2)):] c= V )
by A2;
verum
end;
assume A3:
for x being Point of X
for y being Point of Y st [x,y] in V holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V )
; V is open
for z being Point of [:X,Y:] st z in V holds
ex s being Real st
( s > 0 & Ball (z,s) c= V )
proof
let z be
Point of
[:X,Y:];
( z in V implies ex s being Real st
( s > 0 & Ball (z,s) c= V ) )
assume A4:
z in V
;
ex s being Real st
( s > 0 & Ball (z,s) c= V )
consider x being
Point of
X,
y being
Point of
Y such that A5:
z = [x,y]
by PRVECT_3:18;
consider r1,
r2 being
Real such that A6:
(
0 < r1 &
0 < r2 &
[:(Ball (x,r1)),(Ball (y,r2)):] c= V )
by A3, A4, A5;
consider s being
Real such that A7:
(
s = min (
r1,
r2) &
s > 0 )
and A8:
Ball (
z,
s)
c= [:(Ball (x,r1)),(Ball (y,r2)):]
by A5, A6, Th2;
take
s
;
( s > 0 & Ball (z,s) c= V )
thus
(
s > 0 &
Ball (
z,
s)
c= V )
by A6, A7, A8, XBOOLE_1:1;
verum
end;
hence
V is open
by NDIFF_8:20; verum