let n be Nat; for p being Point of (TOP-REAL n)
for r being Real st r > 0 holds
Int (ClosedHypercube (p,(n |-> r))) = OpenHypercube (p,r)
let p be Point of (TOP-REAL n); for r being Real st r > 0 holds
Int (ClosedHypercube (p,(n |-> r))) = OpenHypercube (p,r)
let r be Real; ( r > 0 implies Int (ClosedHypercube (p,(n |-> r))) = OpenHypercube (p,r) )
assume
r > 0
; Int (ClosedHypercube (p,(n |-> r))) = OpenHypercube (p,r)
set O = OpenHypercube (p,r);
set C = ClosedHypercube (p,(n |-> r));
set TR = TOP-REAL n;
set R = n |-> r;
A1:
Int (ClosedHypercube (p,(n |-> r))) c= ClosedHypercube (p,(n |-> r))
by TOPS_1:16;
consider e being Point of (Euclid n) such that
A2:
p = e
and
A3:
OpenHypercube (p,r) = OpenHypercube (e,r)
by Def1;
set I = Intervals (e,r);
A4:
OpenHypercube (p,r) = product (Intervals (e,r))
by A3, EUCLID_9:def 4;
thus
Int (ClosedHypercube (p,(n |-> r))) c= OpenHypercube (p,r)
XBOOLE_0:def 10 OpenHypercube (p,r) c= Int (ClosedHypercube (p,(n |-> r)))proof
let x be
object ;
TARSKI:def 3 ( not x in Int (ClosedHypercube (p,(n |-> r))) or x in OpenHypercube (p,r) )
A5:
len p = n
by CARD_1:def 7;
then A6:
dom p = Seg n
by FINSEQ_1:def 3;
assume A7:
x in Int (ClosedHypercube (p,(n |-> r)))
;
x in OpenHypercube (p,r)
then reconsider q =
x as
Point of
(TOP-REAL n) ;
A8:
dom p = dom (Intervals (e,r))
by A2, EUCLID_9:def 3;
A9:
not
q in Fr (ClosedHypercube (p,(n |-> r)))
by TOPS_1:39, A7, XBOOLE_0:3;
A10:
for
z being
object st
z in dom (Intervals (e,r)) holds
q . z in (Intervals (e,r)) . z
proof
let z be
object ;
( z in dom (Intervals (e,r)) implies q . z in (Intervals (e,r)) . z )
assume A11:
z in dom (Intervals (e,r))
;
q . z in (Intervals (e,r)) . z
then A12:
(Intervals (e,r)) . z = ].((e . z) - r),((e . z) + r).[
by A2, A8, EUCLID_9:def 3;
reconsider z =
z as
Nat by A11;
A13:
(n |-> r) . z = r
by FINSEQ_2:57, A8, A6, A11;
A14:
q . z in [.((p . z) - ((n |-> r) . z)),((p . z) + ((n |-> r) . z)).]
by A1, A7, A8, A6, A11, Def2;
then
(p . z) - r <= q . z
by A13, XXREAL_1:1;
then A15:
(p . z) - r < q . z
by A13, A9, A1, A7, Th9, A8, A6, A11, XXREAL_0:1;
q . z <= (p . z) + r
by A14, A13, XXREAL_1:1;
then
q . z < (p . z) + r
by A13, A9, A1, A7, Th9, A8, A6, A11, XXREAL_0:1;
hence
q . z in (Intervals (e,r)) . z
by A15, A2, A12, XXREAL_1:4;
verum
end;
len q = n
by CARD_1:def 7;
then
dom q = dom p
by A5, FINSEQ_3:29;
hence
x in OpenHypercube (
p,
r)
by A10, CARD_3:9, A8, A4;
verum
end;
let x be object ; TARSKI:def 3 ( not x in OpenHypercube (p,r) or x in Int (ClosedHypercube (p,(n |-> r))) )
assume A16:
x in OpenHypercube (p,r)
; x in Int (ClosedHypercube (p,(n |-> r)))
then reconsider q = x as Point of (TOP-REAL n) ;
len q = n
by CARD_1:def 7;
then A17:
dom q = Seg n
by FINSEQ_1:def 3;
for i being Nat st i in Seg n holds
q . i in [.((p . i) - ((n |-> r) . i)),((p . i) + ((n |-> r) . i)).]
proof
let i be
Nat;
( i in Seg n implies q . i in [.((p . i) - ((n |-> r) . i)),((p . i) + ((n |-> r) . i)).] )
A18:
dom (PROJ (n,i)) = [#] (TOP-REAL n)
by FUNCT_2:def 1;
assume A19:
i in Seg n
;
q . i in [.((p . i) - ((n |-> r) . i)),((p . i) + ((n |-> r) . i)).]
then A20:
(n |-> r) . i = r
by FINSEQ_2:57;
(PROJ (n,i)) .: (OpenHypercube (p,r)) = ].((e . i) - r),((e . i) + r).[
by A19, A2, Th2;
then A21:
(PROJ (n,i)) . q in ].((e . i) - r),((e . i) + r).[
by A18, A16, FUNCT_1:def 6;
A22:
(PROJ (n,i)) . q = q /. i
by TOPREALC:def 6;
A23:
q /. i = q . i
by A19, A17, PARTFUN1:def 6;
then A24:
q . i <= (p . i) + ((n |-> r) . i)
by A20, A22, A21, A2, XXREAL_1:4;
q . i >= (p . i) - ((n |-> r) . i)
by A20, A23, A22, A21, A2, XXREAL_1:4;
hence
q . i in [.((p . i) - ((n |-> r) . i)),((p . i) + ((n |-> r) . i)).]
by A24, XXREAL_1:1;
verum
end;
then A25:
q in ClosedHypercube (p,(n |-> r))
by Def2;
assume
not x in Int (ClosedHypercube (p,(n |-> r)))
; contradiction
then
q in (ClosedHypercube (p,(n |-> r))) \ (Int (ClosedHypercube (p,(n |-> r))))
by A25, XBOOLE_0:def 5;
then
q in Fr (ClosedHypercube (p,(n |-> r)))
by TOPS_1:43;
then consider i being Nat such that
A26:
i in Seg n
and
A27:
( q . i = (p . i) - ((n |-> r) . i) or q . i = (p . i) + ((n |-> r) . i) )
by Th9;
A28:
dom (PROJ (n,i)) = [#] (TOP-REAL n)
by FUNCT_2:def 1;
(PROJ (n,i)) .: (OpenHypercube (p,r)) = ].((e . i) - r),((e . i) + r).[
by A2, A26, Th2;
then A29:
(PROJ (n,i)) . q in ].((e . i) - r),((e . i) + r).[
by A28, A16, FUNCT_1:def 6;
A30:
(n |-> r) . i = r
by A26, FINSEQ_2:57;
(PROJ (n,i)) . q = q /. i
by TOPREALC:def 6;
then
q . i in ].((e . i) - r),((e . i) + r).[
by A17, A26, PARTFUN1:def 6, A29;
hence
contradiction
by A2, A30, XXREAL_1:4, A27; verum
reconsider oo = OpenHypercube (p,r) as Subset of (TOP-REAL n) ;