let X, Y be RealNormSpace; for x being Point of X
for y being Point of Y
for z being Point of [:X,Y:]
for r1, r2 being Real st 0 < r1 & 0 < r2 & z = [x,y] holds
ex s being Real st
( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )
let x be Point of X; for y being Point of Y
for z being Point of [:X,Y:]
for r1, r2 being Real st 0 < r1 & 0 < r2 & z = [x,y] holds
ex s being Real st
( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )
let y be Point of Y; for z being Point of [:X,Y:]
for r1, r2 being Real st 0 < r1 & 0 < r2 & z = [x,y] holds
ex s being Real st
( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )
let z be Point of [:X,Y:]; for r1, r2 being Real st 0 < r1 & 0 < r2 & z = [x,y] holds
ex s being Real st
( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )
let r1, r2 be Real; ( 0 < r1 & 0 < r2 & z = [x,y] implies ex s being Real st
( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] ) )
assume A1:
( 0 < r1 & 0 < r2 & z = [x,y] )
; ex s being Real st
( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )
take s = min (r1,r2); ( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )
Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):]
proof
let z1 be
object ;
TARSKI:def 3 ( not z1 in Ball (z,s) or z1 in [:(Ball (x,r1)),(Ball (y,r2)):] )
assume A3:
z1 in Ball (
z,
s)
;
z1 in [:(Ball (x,r1)),(Ball (y,r2)):]
then reconsider z1 =
z1 as
Point of
[:X,Y:] ;
A4:
ex
z2 being
Point of
[:X,Y:] st
(
z2 = z1 &
||.(z - z2).|| < s )
by A3;
consider x1 being
Point of
X,
y1 being
Point of
Y such that A5:
z1 = [x1,y1]
by PRVECT_3:18;
- z1 = [(- x1),(- y1)]
by A5, PRVECT_3:18;
then
z - z1 = [(x - x1),(y - y1)]
by A1, PRVECT_3:18;
then
(
||.(x - x1).|| <= ||.(z - z1).|| &
||.(y - y1).|| <= ||.(z - z1).|| )
by NDIFF_8:21;
then A6:
(
||.(x - x1).|| < s &
||.(y - y1).|| < s )
by A4, XXREAL_0:2;
(
s <= r1 &
s <= r2 )
by XXREAL_0:17;
then
(
||.(x - x1).|| < r1 &
||.(y - y1).|| < r2 )
by A6, XXREAL_0:2;
then
(
x1 in Ball (
x,
r1) &
y1 in Ball (
y,
r2) )
;
hence
z1 in [:(Ball (x,r1)),(Ball (y,r2)):]
by A5, ZFMISC_1:87;
verum
end;
hence
( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )
by A1, XXREAL_0:15; verum