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