let x be Point of RealSpace; for r being Real holds Ball (x,r) = ].(x - r),(x + r).[
let r be Real; Ball (x,r) = ].(x - r),(x + r).[
reconsider x2 = x as Element of REAL by METRIC_1:def 13;
thus
Ball (x,r) c= ].(x - r),(x + r).[
XBOOLE_0:def 10 ].(x - r),(x + r).[ c= Ball (x,r)proof
let y be
object ;
TARSKI:def 3 ( not y in Ball (x,r) or y in ].(x - r),(x + r).[ )
assume A1:
y in Ball (
x,
r)
;
y in ].(x - r),(x + r).[
then reconsider y1 =
y as
Element of
RealSpace ;
reconsider y2 =
y1 as
Element of
REAL by METRIC_1:def 13;
A2:
dist (
x,
y1) =
real_dist . (
x2,
y2)
by METRIC_1:def 1, METRIC_1:def 13
.=
|.(x2 - y2).|
by METRIC_1:def 12
.=
|.(- (y2 - x2)).|
.=
|.(y2 - x2).|
by COMPLEX1:52
;
dist (
x,
y1)
< r
by A1, METRIC_1:11;
hence
y in ].(x - r),(x + r).[
by A2, RCOMP_1:1;
verum
end;
let y be object ; TARSKI:def 3 ( not y in ].(x - r),(x + r).[ or y in Ball (x,r) )
assume A3:
y in ].(x - r),(x + r).[
; y in Ball (x,r)
then reconsider y2 = y as Element of REAL ;
reconsider x1 = x, y1 = y2 as Element of RealSpace by METRIC_1:def 13;
|.(y2 - x).| =
|.(- (y2 - x)).|
by COMPLEX1:52
.=
|.(x - y2).|
.=
real_dist . (x2,y2)
by METRIC_1:def 12
;
then A4:
real_dist . (x2,y2) < r
by A3, RCOMP_1:1;
dist (x1,y1) = real_dist . (x2,y2)
by METRIC_1:def 1, METRIC_1:def 13;
hence
y in Ball (x,r)
by A4, METRIC_1:11; verum