let r be Real; :: thesis: 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; :: thesis: 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); :: thesis: 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); :: thesis: ( q = p implies cl_Ball (q,r) = ClosedHypercube (p,(n |-> r)) )
assume A1: q = p ; :: thesis: cl_Ball (q,r) = ClosedHypercube (p,(n |-> r))
A8: cl_Ball (q,r) c= ClosedHypercube (p,(n |-> r))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in cl_Ball (q,r) or x in ClosedHypercube (p,(n |-> r)) )
assume x in cl_Ball (q,r) ; :: thesis: 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 ;
A5: now :: thesis: for i being Nat st i in Seg n holds
f . i in [.((p . i) - ((n |-> r) . i)),((p . i) + ((n |-> r) . i)).]
let i be Nat; :: thesis: ( i in Seg n implies f . i in [.((p . i) - ((n |-> r) . i)),((p . i) + ((n |-> r) . i)).] )
assume i in Seg n ; :: thesis: f . i in [.((p . i) - ((n |-> r) . i)),((p . i) + ((n |-> r) . i)).]
then ( f . i in [.((rq . i) - r),((rq . i) + r).] & (n |-> r) . i = r ) by A4, FINSEQ_2:57;
hence f . i in [.((p . i) - ((n |-> r) . i)),((p . i) + ((n |-> r) . i)).] by A1; :: thesis: verum
end;
rng f c= REAL
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng f or u in REAL )
assume u in rng f ; :: thesis: u in REAL
then consider v being object such that
A6: v in dom f and
A7: u = f . v by FUNCT_1:def 3;
f . v in [.((rq . v) - r),((rq . v) + r).] by A6, A3, A4;
hence u in REAL by A7; :: thesis: verum
end;
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; :: thesis: verum
end;
ClosedHypercube (p,(n |-> r)) c= cl_Ball (q,r)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ClosedHypercube (p,(n |-> r)) or x in cl_Ball (q,r) )
assume A9: x in ClosedHypercube (p,(n |-> r)) ; :: thesis: x in cl_Ball (q,r)
then reconsider y = x as Element of (TOP-REAL n) ;
reconsider f = y as Function ;
now :: thesis: ex f being Function st
( y = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.(((@ q) . i) - r),(((@ q) . i) + r).] ) )
take f = f; :: thesis: ( y = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.(((@ q) . i) - r),(((@ q) . i) + r).] ) )
thus y = f ; :: thesis: ( dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.(((@ q) . i) - r),(((@ q) . i) + r).] ) )
y in TOP-REAL n ;
then y in REAL n by EUCLID:22;
then y is Tuple of n, REAL by FINSEQ_2:131;
hence dom f = Seg n by FINSEQ_2:124; :: thesis: for i being Nat st i in Seg n holds
f . i in [.(((@ q) . i) - r),(((@ q) . i) + r).]
hereby :: thesis: verum
let i be Nat; :: thesis: ( i in Seg n implies f . i in [.(((@ q) . i) - r),(((@ q) . i) + r).] )
assume i in Seg n ; :: thesis: f . i in [.(((@ q) . i) - r),(((@ q) . i) + r).]
then ( y . i in [.((p . i) - ((n |-> r) . i)),((p . i) + ((n |-> r) . i)).] & (n |-> r) . i = r ) by FINSEQ_2:57, A9, TIETZE_2:def 2;
hence f . i in [.(((@ q) . i) - r),(((@ q) . i) + r).] by A1; :: thesis: verum
end;
end;
hence x in cl_Ball (q,r) by Th69; :: thesis: verum
end;
hence cl_Ball (q,r) = ClosedHypercube (p,(n |-> r)) by A8; :: thesis: verum