let n be Nat; for p being Point of (TOP-REAL n)
for r being Real
for R being real-valued FinSequence st n <= len R & r <= inf (rng R) holds
OpenHypercube (p,r) c= ClosedHypercube (p,R)
let p be Point of (TOP-REAL n); for r being Real
for R being real-valued FinSequence st n <= len R & r <= inf (rng R) holds
OpenHypercube (p,r) c= ClosedHypercube (p,R)
let r be Real; for R being real-valued FinSequence st n <= len R & r <= inf (rng R) holds
OpenHypercube (p,r) c= ClosedHypercube (p,R)
let R be real-valued FinSequence; ( n <= len R & r <= inf (rng R) implies OpenHypercube (p,r) c= ClosedHypercube (p,R) )
set H = ClosedHypercube (p,R);
assume that
A1:
n <= len R
and
A2:
r <= inf (rng R)
; OpenHypercube (p,r) c= ClosedHypercube (p,R)
A3:
Seg n c= Seg (len R)
by A1, FINSEQ_1:5;
set E = Euclid n;
set TE = TopSpaceMetr (Euclid n);
set TR = TOP-REAL n;
let x be object ; TARSKI:def 3 ( not x in OpenHypercube (p,r) or x in ClosedHypercube (p,R) )
A4:
Seg (len R) = dom R
by FINSEQ_1:def 3;
assume A5:
x in OpenHypercube (p,r)
; x in ClosedHypercube (p,R)
then reconsider q = x as Point of (TOP-REAL n) ;
consider e being Point of (Euclid n) such that
A6:
p = e
and
A7:
OpenHypercube (p,r) = OpenHypercube (e,r)
by Def1;
set I = Intervals (e,r);
A8:
x in product (Intervals (e,r))
by A5, A7, EUCLID_9:def 4;
now for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).]let i be
Nat;
( i in Seg n implies q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] )A9:
dom (Intervals (e,r)) = dom e
by EUCLID_9:def 3;
assume A10:
i in Seg n
;
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).]then
R . i in rng R
by A3, A4, FUNCT_1:def 3;
then
inf (rng R) <= R . i
by XXREAL_2:3;
then A11:
r <= R . i
by A2, XXREAL_0:2;
then A12:
(e . i) + r <= (e . i) + (R . i)
by XREAL_1:6;
A13:
dom p = Seg (len p)
by FINSEQ_1:def 3;
A14:
(e . i) - r >= (e . i) - (R . i)
by A11, XREAL_1:10;
A15:
len p = n
by CARD_1:def 7;
then
(Intervals (e,r)) . i = ].((e . i) - r),((e . i) + r).[
by A13, A6, A10, EUCLID_9:def 3;
then A16:
q . i in ].((e . i) - r),((e . i) + r).[
by A9, CARD_3:9, A6, A10, A15, A13, A8;
then
(e . i) - r < q . i
by XXREAL_1:4;
then A17:
(p . i) - (R . i) < q . i
by A14, A6, XXREAL_0:2;
q . i < (e . i) + r
by A16, XXREAL_1:4;
then
q . i < (p . i) + (R . i)
by A12, A6, XXREAL_0:2;
hence
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).]
by A17, XXREAL_1:1;
verum end;
hence
x in ClosedHypercube (p,R)
by Def2; verum