let n be Nat; for p, q being Point of (TOP-REAL n)
for r being Real holds
( q in OpenHypercube (p,r) iff for i being Nat st i in Seg n holds
q . i in ].((p . i) - r),((p . i) + r).[ )
let p, q be Point of (TOP-REAL n); for r being Real holds
( q in OpenHypercube (p,r) iff for i being Nat st i in Seg n holds
q . i in ].((p . i) - r),((p . i) + r).[ )
let r be Real; ( q in OpenHypercube (p,r) iff for i being Nat st i in Seg n holds
q . i in ].((p . i) - r),((p . i) + r).[ )
A1:
len q = n
by CARD_1:def 7;
thus
( q in OpenHypercube (p,r) implies for i being Nat st i in Seg n holds
q . i in ].((p . i) - r),((p . i) + r).[ )
( ( for i being Nat st i in Seg n holds
q . i in ].((p . i) - r),((p . i) + r).[ ) implies q in OpenHypercube (p,r) )proof
assume A2:
q in OpenHypercube (
p,
r)
;
for i being Nat st i in Seg n holds
q . i in ].((p . i) - r),((p . i) + r).[
let i be
Nat;
( i in Seg n implies q . i in ].((p . i) - r),((p . i) + r).[ )
assume A3:
i in Seg n
;
q . i in ].((p . i) - r),((p . i) + r).[
set P =
PROJ (
n,
i);
dom (PROJ (n,i)) = the
carrier of
(TOP-REAL n)
by FUNCT_2:def 1;
then A4:
(PROJ (n,i)) . q in (PROJ (n,i)) .: (OpenHypercube (p,r))
by A2, FUNCT_1:def 6;
A5:
(PROJ (n,i)) . q = q /. i
by TOPREALC:def 6;
len q = n
by CARD_1:def 7;
then
dom q = Seg n
by FINSEQ_1:def 3;
then
q /. i = q . i
by A3, PARTFUN1:def 6;
hence
q . i in ].((p . i) - r),((p . i) + r).[
by A5, Th2, A3, A4;
verum
end;
assume A6:
for i being Nat st i in Seg n holds
q . i in ].((p . i) - r),((p . i) + r).[
; q in OpenHypercube (p,r)
consider e being Point of (Euclid n) such that
A7:
p = e
and
A8:
OpenHypercube (p,r) = OpenHypercube (e,r)
by Def1;
set I = Intervals (e,r);
A9:
dom (Intervals (e,r)) = dom e
by EUCLID_9:def 3;
len p = n
by CARD_1:def 7;
then A10:
dom p = dom q
by A1, FINSEQ_3:29;
A11:
dom q = Seg n
by A1, FINSEQ_1:def 3;
product (Intervals (e,r)) = OpenHypercube (p,r)
by A8, EUCLID_9:def 4;
hence
q in OpenHypercube (p,r)
by A12, A7, A10, A9, CARD_3:9; verum