let V be RealUnitarySpace; for v, u being Point of V
for r being Real st u in Ball (v,r) holds
ex p being Real st
( p > 0 & Ball (u,p) c= Ball (v,r) )
let v, u be Point of V; for r being Real st u in Ball (v,r) holds
ex p being Real st
( p > 0 & Ball (u,p) c= Ball (v,r) )
let r be Real; ( u in Ball (v,r) implies ex p being Real st
( p > 0 & Ball (u,p) c= Ball (v,r) ) )
assume
u in Ball (v,r)
; ex p being Real st
( p > 0 & Ball (u,p) c= Ball (v,r) )
then A1:
dist (v,u) < r
by BHSP_2:41;
thus
ex p being Real st
( p > 0 & Ball (u,p) c= Ball (v,r) )
verumproof
set p =
r - (dist (v,u));
take
r - (dist (v,u))
;
( r - (dist (v,u)) > 0 & Ball (u,(r - (dist (v,u)))) c= Ball (v,r) )
thus
r - (dist (v,u)) > 0
by A1, XREAL_1:50;
Ball (u,(r - (dist (v,u)))) c= Ball (v,r)
for
w being
Point of
V st
w in Ball (
u,
(r - (dist (v,u)))) holds
w in Ball (
v,
r)
proof
let w be
Point of
V;
( w in Ball (u,(r - (dist (v,u)))) implies w in Ball (v,r) )
assume
w in Ball (
u,
(r - (dist (v,u))))
;
w in Ball (v,r)
then
dist (
u,
w)
< r - (dist (v,u))
by BHSP_2:41;
then A2:
(dist (v,u)) + (dist (u,w)) < r
by XREAL_1:20;
(dist (v,u)) + (dist (u,w)) >= dist (
v,
w)
by BHSP_1:35;
then
dist (
v,
w)
< r
by A2, XXREAL_0:2;
hence
w in Ball (
v,
r)
by BHSP_2:41;
verum
end;
hence
Ball (
u,
(r - (dist (v,u))))
c= Ball (
v,
r)
;
verum
end;