let X, Y be RealNormSpace; for V being Subset of [:X,Y:]
for D being Subset of X
for E being Subset of Y st D is open & E is open & V = [:D,E:] holds
V is open
let V be Subset of [:X,Y:]; for D being Subset of X
for E being Subset of Y st D is open & E is open & V = [:D,E:] holds
V is open
let D be Subset of X; for E being Subset of Y st D is open & E is open & V = [:D,E:] holds
V is open
let E be Subset of Y; ( D is open & E is open & V = [:D,E:] implies V is open )
assume A1:
( D is open & E is open & V = [:D,E:] )
; 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 )
proof
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 A2:
(
x in D &
y in E )
by A1, ZFMISC_1:87;
then consider r being
Real such that A3:
(
r > 0 &
Ball (
x,
r)
c= D )
by A1, NDIFF_8:20;
consider r2 being
Real such that A4:
(
r2 > 0 &
Ball (
y,
r2)
c= E )
by A1, A2, NDIFF_8:20;
for
z being
object st
z in [:(Ball (x,r)),(Ball (y,r2)):] holds
z in V
proof
let z be
object ;
( z in [:(Ball (x,r)),(Ball (y,r2)):] implies z in V )
assume
z in [:(Ball (x,r)),(Ball (y,r2)):]
;
z in V
then consider qx,
qy being
object such that A5:
(
qx in Ball (
x,
r) &
qy in Ball (
y,
r2) &
z = [qx,qy] )
by ZFMISC_1:def 2;
reconsider qx =
qx as
Point of
X by A5;
reconsider qy =
qy as
Point of
Y by A5;
thus
z in V
by A1, A3, A4, A5, ZFMISC_1:87;
verum
end;
then
[:(Ball (x,r)),(Ball (y,r2)):] c= V
;
hence
ex
r1,
r2 being
Real st
(
0 < r1 &
0 < r2 &
[:(Ball (x,r1)),(Ball (y,r2)):] c= V )
by A3, A4;
verum
end;
hence
V is open
by NDIFF10:3; verum