let PM be MetrStruct ; for x, y being Element of PM
for r being Real st PM is triangle & y in Ball (x,r) holds
ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )
let x, y be Element of PM; for r being Real st PM is triangle & y in Ball (x,r) holds
ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )
let r be Real; ( PM is triangle & y in Ball (x,r) implies ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) ) )
reconsider r9 = r as Real ;
assume A1:
PM is triangle
; ( not y in Ball (x,r) or ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) ) )
assume A2:
y in Ball (x,r)
; ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )
then A3:
dist (x,y) < r
by METRIC_1:11;
A4:
not PM is empty
by A2;
thus
ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )
verumproof
set p =
r9 - (dist (x,y));
take
r9 - (dist (x,y))
;
( r9 - (dist (x,y)) > 0 & Ball (y,(r9 - (dist (x,y)))) c= Ball (x,r) )
thus
r9 - (dist (x,y)) > 0
by A3, XREAL_1:50;
Ball (y,(r9 - (dist (x,y)))) c= Ball (x,r)
for
z being
Element of
PM st
z in Ball (
y,
(r9 - (dist (x,y)))) holds
z in Ball (
x,
r)
proof
let z be
Element of
PM;
( z in Ball (y,(r9 - (dist (x,y)))) implies z in Ball (x,r) )
assume
z in Ball (
y,
(r9 - (dist (x,y))))
;
z in Ball (x,r)
then
dist (
y,
z)
< r9 - (dist (x,y))
by METRIC_1:11;
then A5:
(dist (x,y)) + (dist (y,z)) < r
by XREAL_1:20;
(dist (x,y)) + (dist (y,z)) >= dist (
x,
z)
by A1, METRIC_1:4;
then
dist (
x,
z)
< r
by A5, XXREAL_0:2;
hence
z in Ball (
x,
r)
by A4, METRIC_1:11;
verum
end;
hence
Ball (
y,
(r9 - (dist (x,y))))
c= Ball (
x,
r)
;
verum
end;