let r be Real; for n being non zero Nat
for p being Element of (EMINFTY n) holds Ball (p,r) = product (Intervals ((@ p),r))
let n be non zero Nat; for p being Element of (EMINFTY n) holds Ball (p,r) = product (Intervals ((@ p),r))
let p be Element of (EMINFTY n); Ball (p,r) = product (Intervals ((@ p),r))
consider x being Element of REAL n such that
A1:
@ p = x
;
per cases
( r <= 0 or r > 0 )
;
suppose A2:
r > 0
;
Ball (p,r) = product (Intervals ((@ p),r))A3:
{ q where q is Element of (EMINFTY n) : dist (p,q) < r } c= product (Intervals (x,r))
proof
let t be
object ;
TARSKI:def 3 ( not t in { q where q is Element of (EMINFTY n) : dist (p,q) < r } or t in product (Intervals (x,r)) )
assume
t in { q where q is Element of (EMINFTY n) : dist (p,q) < r }
;
t in product (Intervals (x,r))
then consider q being
Element of
(EMINFTY n) such that A4:
t = q
and A5:
dist (
p,
q)
< r
;
reconsider pr =
p,
qr =
q as
Element of
REAL n ;
consider S being
ext-real-membered set such that A6:
S = { |.((pr . i) - (qr . i)).| where i is Element of Seg n : verum }
and A7:
(Infty_dist n) . (
pr,
qr)
= sup S
by Th57;
(Infty_dist n) . (
p,
q)
in REAL
by BINOP_1:17;
then reconsider s =
(Infty_dist n) . (
p,
q) as
Real ;
reconsider f =
Intervals (
x,
r) as
Function ;
hence
t in product (Intervals (x,r))
by A4, CARD_3:9;
verum
end;
product (Intervals (x,r)) c= { q where q is Element of (EMINFTY n) : dist (p,q) < r }
proof
let t be
object ;
TARSKI:def 3 ( not t in product (Intervals (x,r)) or t in { q where q is Element of (EMINFTY n) : dist (p,q) < r } )
assume
t in product (Intervals (x,r))
;
t in { q where q is Element of (EMINFTY n) : dist (p,q) < r }
then consider g being
Function such that A14:
t = g
and A15:
dom g = dom (Intervals (x,r))
and A16:
for
y being
object st
y in dom (Intervals (x,r)) holds
g . y in (Intervals (x,r)) . y
by CARD_3:def 5;
A17:
dom (Intervals (x,r)) =
dom x
by EUCLID_9:def 3
.=
Seg n
by FINSEQ_1:89
;
rng g c= REAL
then
g in Funcs (
(Seg n),
REAL)
by A17, A15, FUNCT_2:def 2;
then reconsider g0 =
g as
Element of
(EMINFTY n) by FINSEQ_2:93;
dist (
p,
g0)
< r
proof
reconsider p1 =
p,
g1 =
g0 as
Element of
REAL n ;
consider S being
ext-real-membered set such that
S = { |.((p1 . i) - (g1 . i)).| where i is Element of Seg n : verum }
and A21:
(Infty_dist n) . (
p1,
g1)
= sup S
by Th57;
sup S < r
proof
assume A22:
r <= sup S
;
contradiction
set md =
max_diff_index (
p1,
g1);
A23:
r <= (abs (p1 - g1)) . (max_diff_index (p1,g1))
by A22, A21, Th58;
A24:
max_diff_index (
p1,
g1)
in dom x
by A1, EUCLID_9:4;
then
max_diff_index (
p1,
g1)
in dom (Intervals (x,r))
by EUCLID_9:def 3;
then
g1 . (max_diff_index (p1,g1)) in (Intervals (x,r)) . (max_diff_index (p1,g1))
by A16;
then A25:
g1 . (max_diff_index (p1,g1)) in ].((p1 . (max_diff_index (p1,g1))) - r),((p1 . (max_diff_index (p1,g1))) + r).[
by A24, A1, EUCLID_9:def 3;
A26:
(
(p1 . (max_diff_index (p1,g1))) - r < g1 . (max_diff_index (p1,g1)) &
g1 . (max_diff_index (p1,g1)) < (p1 . (max_diff_index (p1,g1))) + r )
by A25, XXREAL_1:4;
((p1 . (max_diff_index (p1,g1))) - r) + r < (g1 . (max_diff_index (p1,g1))) + r
by A26, XREAL_1:8;
then A27:
(p1 . (max_diff_index (p1,g1))) - (g1 . (max_diff_index (p1,g1))) < ((g1 . (max_diff_index (p1,g1))) + r) - (g1 . (max_diff_index (p1,g1)))
by XREAL_1:14;
(g1 . (max_diff_index (p1,g1))) - (p1 . (max_diff_index (p1,g1))) < ((p1 . (max_diff_index (p1,g1))) + r) - (p1 . (max_diff_index (p1,g1)))
by A26, XREAL_1:14;
then A28:
(
(p1 . (max_diff_index (p1,g1))) - (g1 . (max_diff_index (p1,g1))) < r &
- ((p1 . (max_diff_index (p1,g1))) - (g1 . (max_diff_index (p1,g1)))) < r )
by A27;
then A29:
(
(p1 - g1) . (max_diff_index (p1,g1)) < r &
- ((p1 - g1) . (max_diff_index (p1,g1))) < r )
by RVSUM_1:27;
set pg =
(p1 - g1) . (max_diff_index (p1,g1));
|.((p1 - g1) . (max_diff_index (p1,g1))).| < r
hence
contradiction
by A23, VALUED_1:18;
verum
end;
hence
dist (
p,
g0)
< r
by A21;
verum
end;
hence
t in { q where q is Element of (EMINFTY n) : dist (p,q) < r }
by A14;
verum
end; hence
Ball (
p,
r)
= product (Intervals ((@ p),r))
by A1, A3, METRIC_1:def 14;
verum end; end;