let X, Y be RealNormSpace; for x being Point of X
for y being Point of Y
for V being Subset of [:X,Y:]
for r being Real st V = [:(Ball (x,r)),(Ball (y,r)):] holds
V is open
let x be Point of X; for y being Point of Y
for V being Subset of [:X,Y:]
for r being Real st V = [:(Ball (x,r)),(Ball (y,r)):] holds
V is open
let y be Point of Y; for V being Subset of [:X,Y:]
for r being Real st V = [:(Ball (x,r)),(Ball (y,r)):] holds
V is open
let V be Subset of [:X,Y:]; for r being Real st V = [:(Ball (x,r)),(Ball (y,r)):] holds
V is open
let r be Real; ( V = [:(Ball (x,r)),(Ball (y,r)):] implies V is open )
assume A1:
V = [:(Ball (x,r)),(Ball (y,r)):]
; 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 A2:
z in V
;
ex s being Real st
( s > 0 & Ball (z,s) c= V )
consider x1 being
Point of
X,
y1 being
Point of
Y such that A3:
z = [x1,y1]
by PRVECT_3:18;
A4:
(
x1 in Ball (
x,
r) &
y1 in Ball (
y,
r) )
by A1, A2, A3, ZFMISC_1:87;
A5:
ex
p being
Point of
X st
(
x1 = p &
||.(x - p).|| < r )
by A4;
A6:
ex
p being
Point of
Y st
(
y1 = p &
||.(y - p).|| < r )
by A4;
set r1 =
r - ||.(x - x1).||;
set r2 =
r - ||.(y - y1).||;
A7:
0 < r - ||.(x - x1).||
by A5, XREAL_1:50;
A8:
0 < r - ||.(y - y1).||
by A6, XREAL_1:50;
reconsider s =
min (
(r - ||.(x - x1).||),
(r - ||.(y - y1).||)) as
Real ;
A9:
0 < s
by A7, A8, XXREAL_0:15;
A10:
s <= r - ||.(x - x1).||
by XXREAL_0:17;
A11:
s <= r - ||.(y - y1).||
by XXREAL_0:17;
Ball (
z,
s)
c= V
proof
let w be
object ;
TARSKI:def 3 ( not w in Ball (z,s) or w in V )
assume A12:
w in Ball (
z,
s)
;
w in V
then reconsider q =
w as
Point of
[:X,Y:] ;
A13:
ex
t being
Point of
[:X,Y:] st
(
q = t &
||.(z - t).|| < s )
by A12;
consider qx being
Point of
X,
qy being
Point of
Y such that A14:
q = [qx,qy]
by PRVECT_3:18;
- q = [(- qx),(- qy)]
by A14, PRVECT_3:18;
then
z - q = [(x1 - qx),(y1 - qy)]
by A3, PRVECT_3:18;
then
(
||.(x1 - qx).|| <= ||.(z - q).|| &
||.(y1 - qy).|| <= ||.(z - q).|| )
by NORMSP35;
then A16:
(
||.(x1 - qx).|| < s &
||.(y1 - qy).|| < s )
by A13, XXREAL_0:2;
(x - x1) + (x1 - qx) =
((x - x1) + x1) - qx
by RLVECT_1:28
.=
x - qx
by RLVECT_4:1
;
then A17:
||.(x - qx).|| <= ||.(x - x1).|| + ||.(x1 - qx).||
by NORMSP_1:def 1;
A18:
||.(x - x1).|| + ||.(x1 - qx).|| < ||.(x - x1).|| + s
by A16, XREAL_1:8;
||.(x - x1).|| + s <= ||.(x - x1).|| + (r - ||.(x - x1).||)
by A10, XREAL_1:7;
then
||.(x - x1).|| + ||.(x1 - qx).|| < r
by A18, XXREAL_0:2;
then
||.(x - qx).|| < r
by A17, XXREAL_0:2;
then A19:
qx in Ball (
x,
r)
;
(y - y1) + (y1 - qy) =
((y - y1) + y1) - qy
by RLVECT_1:28
.=
y - qy
by RLVECT_4:1
;
then A20:
||.(y - qy).|| <= ||.(y - y1).|| + ||.(y1 - qy).||
by NORMSP_1:def 1;
A21:
||.(y - y1).|| + ||.(y1 - qy).|| < ||.(y - y1).|| + s
by A16, XREAL_1:8;
||.(y - y1).|| + s <= ||.(y - y1).|| + (r - ||.(y - y1).||)
by A11, XREAL_1:7;
then
||.(y - y1).|| + ||.(y1 - qy).|| < r
by A21, XXREAL_0:2;
then
||.(y - qy).|| < r
by A20, XXREAL_0:2;
then
qy in Ball (
y,
r)
;
hence
w in V
by A1, A14, A19, ZFMISC_1:87;
verum
end;
hence
ex
s being
Real st
(
s > 0 &
Ball (
z,
s)
c= V )
by A9;
verum
end;
hence
V is open
by NORMSP27; verum