let u be Point of (Euclid 1); for r, u1 being Real st <*u1*> = u holds
cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }
let r, u1 be Real; ( <*u1*> = u implies cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } )
assume A1:
<*u1*> = u
; cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }
set E1 = { q where q is Element of (Euclid 1) : dist (u,q) <= r } ;
reconsider u1 = u1 as Element of REAL by XREAL_0:def 1;
set R1 = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } ;
A2:
{ q where q is Element of (Euclid 1) : dist (u,q) <= r } c= { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }
proof
let x be
object ;
TARSKI:def 3 ( not x in { q where q is Element of (Euclid 1) : dist (u,q) <= r } or x in { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } )
assume
x in { q where q is Element of (Euclid 1) : dist (u,q) <= r }
;
x in { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }
then consider q being
Element of
(Euclid 1) such that A3:
x = q
and A4:
dist (
u,
q)
<= r
;
q is
Tuple of 1,
REAL
by FINSEQ_2:131;
then consider s1 being
Element of
REAL such that A5:
q = <*s1*>
by FINSEQ_2:97;
<*u1*> - <*s1*> = <*(u1 - s1)*>
by RVSUM_1:29;
then
sqr (<*u1*> - <*s1*>) = <*((u1 - s1) ^2)*>
by RVSUM_1:55;
then
Sum (sqr (<*u1*> - <*s1*>)) = (u1 - s1) ^2
by RVSUM_1:73;
then A6:
sqrt (Sum (sqr (<*u1*> - <*s1*>))) = |.(u1 - s1).|
by COMPLEX1:72;
A7:
|.(<*u1*> - <*s1*>).| <= r
by A1, A4, A5, EUCLID:def 6;
then
u1 - s1 <= r
by A6, ABSVALUE:5;
then
(u1 - s1) + s1 <= r + s1
by XREAL_1:6;
then A8:
u1 - r <= (r + s1) - r
by XREAL_1:9;
- r <= u1 - s1
by A6, A7, ABSVALUE:5;
then
(- r) + s1 <= (u1 - s1) + s1
by XREAL_1:6;
then
(s1 - r) + r <= u1 + r
by XREAL_1:6;
hence
x in { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }
by A3, A5, A8;
verum
end;
{ <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } c= { q where q is Element of (Euclid 1) : dist (u,q) <= r }
proof
reconsider eu1 =
<*u1*> as
Element of
REAL 1
by FINSEQ_2:98;
let x be
object ;
TARSKI:def 3 ( not x in { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } or x in { q where q is Element of (Euclid 1) : dist (u,q) <= r } )
assume
x in { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }
;
x in { q where q is Element of (Euclid 1) : dist (u,q) <= r }
then consider s being
Real such that A9:
x = <*s*>
and A10:
u1 - r <= s
and A11:
s <= u1 + r
;
s - r <= (u1 + r) - r
by A11, XREAL_1:9;
then A12:
(s + (- r)) - s <= u1 - s
by XREAL_1:9;
reconsider s =
s as
Element of
REAL by XREAL_0:def 1;
reconsider es =
<*s*> as
Element of
REAL 1
by FINSEQ_2:98;
reconsider q1 =
<*s*> as
Element of
(Euclid 1) by FINSEQ_2:98;
<*u1*> - <*s*> = <*(u1 - s)*>
by RVSUM_1:29;
then
sqr (<*u1*> - <*s*>) = <*((u1 - s) ^2)*>
by RVSUM_1:55;
then A13:
Sum (sqr (<*u1*> - <*s*>)) = (u1 - s) ^2
by RVSUM_1:73;
(u1 - r) + r <= s + r
by A10, XREAL_1:6;
then
u1 - s <= (s + r) - s
by XREAL_1:9;
then
|.(u1 - s).| <= r
by A12, ABSVALUE:5;
then
|.(<*u1*> - <*s*>).| <= r
by A13, COMPLEX1:72;
then
( the
distance of
(Euclid 1) . (
u,
q1)
= dist (
u,
q1) &
(Pitag_dist 1) . (
eu1,
es)
<= r )
by EUCLID:def 6;
hence
x in { q where q is Element of (Euclid 1) : dist (u,q) <= r }
by A1, A9;
verum
end;
then
{ q where q is Element of (Euclid 1) : dist (u,q) <= r } = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }
by A2;
hence
cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }
by METRIC_1:18; verum