let r be Real; for n being non zero Nat
for p being Point of (TOP-REAL n)
for q being Element of (EMINFTY n) st q = p holds
cl_Ball (q,r) = ClosedHypercube (p,(n |-> r))
let n be non zero Nat; for p being Point of (TOP-REAL n)
for q being Element of (EMINFTY n) st q = p holds
cl_Ball (q,r) = ClosedHypercube (p,(n |-> r))
let p be Point of (TOP-REAL n); for q being Element of (EMINFTY n) st q = p holds
cl_Ball (q,r) = ClosedHypercube (p,(n |-> r))
let q be Element of (EMINFTY n); ( q = p implies cl_Ball (q,r) = ClosedHypercube (p,(n |-> r)) )
assume A1:
q = p
; cl_Ball (q,r) = ClosedHypercube (p,(n |-> r))
A8:
cl_Ball (q,r) c= ClosedHypercube (p,(n |-> r))
proof
let x be
object ;
TARSKI:def 3 ( not x in cl_Ball (q,r) or x in ClosedHypercube (p,(n |-> r)) )
assume
x in cl_Ball (
q,
r)
;
x in ClosedHypercube (p,(n |-> r))
then consider f being
Function such that A2:
x = f
and A3:
dom f = Seg n
and A4:
for
i being
Nat st
i in Seg n holds
f . i in [.(((@ q) . i) - r),(((@ q) . i) + r).]
by Th69;
reconsider rq =
@ q as
Element of
REAL n ;
rng f c= REAL
then
f in Funcs (
(Seg n),
REAL)
by A3, FUNCT_2:def 2;
then
f in REAL n
by FINSEQ_2:93;
then reconsider fx =
f as
Element of
(TOP-REAL n) by EUCLID:22;
fx in ClosedHypercube (
p,
(n |-> r))
by A5, TIETZE_2:def 2;
hence
x in ClosedHypercube (
p,
(n |-> r))
by A2;
verum
end;
ClosedHypercube (p,(n |-> r)) c= cl_Ball (q,r)
hence
cl_Ball (q,r) = ClosedHypercube (p,(n |-> r))
by A8; verum