let n, k be Nat; for Ak being Subset of (TOP-REAL k)
for A being Subset of (TOP-REAL (k + n)) st A = { (v ^ (n |-> 0)) where v is Element of (TOP-REAL k) : verum } holds
for B being Subset of ((TOP-REAL (k + n)) | A) st B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } holds
( Ak is open iff B is open )
let Ak be Subset of (TOP-REAL k); for A being Subset of (TOP-REAL (k + n)) st A = { (v ^ (n |-> 0)) where v is Element of (TOP-REAL k) : verum } holds
for B being Subset of ((TOP-REAL (k + n)) | A) st B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } holds
( Ak is open iff B is open )
set kn = k + n;
set TRn = TOP-REAL (k + n);
set TRk = TOP-REAL k;
let A be Subset of (TOP-REAL (k + n)); ( A = { (v ^ (n |-> 0)) where v is Element of (TOP-REAL k) : verum } implies for B being Subset of ((TOP-REAL (k + n)) | A) st B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } holds
( Ak is open iff B is open ) )
assume A1:
A = { (v ^ (n |-> 0)) where v is Element of (TOP-REAL k) : verum }
; for B being Subset of ((TOP-REAL (k + n)) | A) st B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } holds
( Ak is open iff B is open )
A2:
TopStruct(# the carrier of (TOP-REAL k), the topology of (TOP-REAL k) #) = TopSpaceMetr (Euclid k)
by EUCLID:def 8;
then reconsider p = Ak as Subset of (TopSpaceMetr (Euclid k)) ;
set TRA = (TOP-REAL (k + n)) | A;
let B be Subset of ((TOP-REAL (k + n)) | A); ( B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } implies ( Ak is open iff B is open ) )
assume A3:
B = { v where v is Element of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) }
; ( Ak is open iff B is open )
A4:
[#] ((TOP-REAL (k + n)) | A) = A
by PRE_TOPC:def 5;
A5:
k + n >= k
by NAT_1:11;
hereby ( B is open implies Ak is open )
end;
assume
B is open
; Ak is open
then
B in the topology of ((TOP-REAL (k + n)) | A)
by PRE_TOPC:def 2;
then consider Q being Subset of (TOP-REAL (k + n)) such that
A13:
Q in the topology of (TOP-REAL (k + n))
and
A14:
Q /\ ([#] ((TOP-REAL (k + n)) | A)) = B
by PRE_TOPC:def 4;
A15:
TopStruct(# the carrier of (TOP-REAL (k + n)), the topology of (TOP-REAL (k + n)) #) = TopSpaceMetr (Euclid (k + n))
by EUCLID:def 8;
then reconsider q = Q as Subset of (TopSpaceMetr (Euclid (k + n))) ;
A16:
q is open
by A13, A15, PRE_TOPC:def 2;
for e being Point of (Euclid k) st e in p holds
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= p )
proof
let e be
Point of
(Euclid k);
( e in p implies ex r being Real st
( r > 0 & OpenHypercube (e,r) c= p ) )
A17:
len (n |-> 0) = n
by CARD_1:def 7;
A18:
@ (@ (e ^ (n |-> 0))) = e ^ (n |-> 0)
;
A19:
len e = k
by CARD_1:def 7;
then
len (e ^ (n |-> 0)) = k + n
by A17, FINSEQ_1:22;
then reconsider e0 =
e ^ (n |-> 0) as
Point of
(Euclid (k + n)) by A18, TOPREAL3:45;
dom e = Seg k
by A19, FINSEQ_1:def 3;
then A20:
e = e0 | k
by FINSEQ_1:21;
n |-> 0 = @ (@ (n |-> 0))
;
then reconsider N =
n |-> 0 as
Element of
(Euclid n) by A17, TOPREAL3:45;
e is
Element of
(TOP-REAL k)
by Lm1;
then A21:
e0 in A
by A1;
assume
e in p
;
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= p )
then
e0 in B
by A3, A21, A20;
then
e0 in q
by A14, XBOOLE_0:def 4;
then consider m being non
zero Element of
NAT such that A22:
OpenHypercube (
e0,
(1 / m))
c= q
by A16, EUCLID_9:23;
set r = 1
/ m;
take
1
/ m
;
( 1 / m > 0 & OpenHypercube (e,(1 / m)) c= p )
thus
1
/ m > 0
by XREAL_1:139;
OpenHypercube (e,(1 / m)) c= p
let x be
object ;
TARSKI:def 3 ( not x in OpenHypercube (e,(1 / m)) or x in p )
N in OpenHypercube (
N,
(1 / m))
by EUCLID_9:11, XREAL_1:139;
then A23:
N in product (Intervals (N,(1 / m)))
by EUCLID_9:def 4;
assume A24:
x in OpenHypercube (
e,
(1 / m))
;
x in p
then reconsider w =
x as
Point of
(TOP-REAL k) by A2;
A25:
(Intervals (e,(1 / m))) ^ (Intervals (N,(1 / m))) = Intervals (
(e ^ N),
(1 / m))
by Th1;
w in product (Intervals (e,(1 / m)))
by A24, EUCLID_9:def 4;
then
w ^ N in product (Intervals (e0,(1 / m)))
by A23, A25, Th2;
then A26:
w ^ N in OpenHypercube (
e0,
(1 / m))
by EUCLID_9:def 4;
w ^ N in A
by A1;
then
w ^ N in B
by A4, A14, A22, A26, XBOOLE_0:def 4;
then A27:
ex
v being
Element of
(TOP-REAL (k + n)) st
(
w ^ N = v &
v | k in Ak &
v in A )
by A3;
len w = k
by CARD_1:def 7;
then (w ^ N) | k =
(w ^ N) | (dom w)
by FINSEQ_1:def 3
.=
w
by FINSEQ_1:21
;
hence
x in p
by A27;
verum
end;
then
p is open
by EUCLID_9:24;
then
Ak in the topology of (TOP-REAL k)
by A2, PRE_TOPC:def 2;
hence
Ak is open
by PRE_TOPC:def 2; verum