let n, k be Nat; :: thesis: 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); :: thesis: 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)); :: thesis: ( 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 } ; :: thesis: 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); :: thesis: ( 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 ) } ; :: thesis: ( 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;

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 )

then Ak in the topology of (TOP-REAL k) by A2, PRE_TOPC:def 2;

hence Ak is open by PRE_TOPC:def 2; :: thesis: verum

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); :: thesis: 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)); :: thesis: ( 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 } ; :: thesis: 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); :: thesis: ( 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 ) } ; :: thesis: ( 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 :: thesis: ( B is open implies Ak is open )

assume
B is open
; :: thesis: Ak is open set PP = { v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } ;

{ v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } c= [#] (TOP-REAL (k + n))

A6: PP /\ A c= B

then PP is open by A5, Th7;

then PP in the topology of (TOP-REAL (k + n)) by PRE_TOPC:def 2;

then A9: PP /\ ([#] ((TOP-REAL (k + n)) | A)) in the topology of ((TOP-REAL (k + n)) | A) by PRE_TOPC:def 4;

B c= PP /\ A

hence B is open by A4, A9, PRE_TOPC:def 2; :: thesis: verum

end;{ v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } c= [#] (TOP-REAL (k + n))

proof

then reconsider PP = { v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } as Subset of (TOP-REAL (k + n)) ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } or x in [#] (TOP-REAL (k + n)) )

assume x in { v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } ; :: thesis: x in [#] (TOP-REAL (k + n))

then ex v being Element of (TOP-REAL (k + n)) st

( x = v & v | k in Ak ) ;

hence x in [#] (TOP-REAL (k + n)) ; :: thesis: verum

end;assume x in { v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } ; :: thesis: x in [#] (TOP-REAL (k + n))

then ex v being Element of (TOP-REAL (k + n)) st

( x = v & v | k in Ak ) ;

hence x in [#] (TOP-REAL (k + n)) ; :: thesis: verum

A6: PP /\ A c= B

proof

assume
Ak is open
; :: thesis: B is open
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PP /\ A or x in B )

assume A7: x in PP /\ A ; :: thesis: x in B

then x in PP by XBOOLE_0:def 4;

then consider v being Element of (TOP-REAL (k + n)) such that

A8: ( x = v & v | k in Ak ) ;

x in A by A7, XBOOLE_0:def 4;

hence x in B by A3, A8; :: thesis: verum

end;assume A7: x in PP /\ A ; :: thesis: x in B

then x in PP by XBOOLE_0:def 4;

then consider v being Element of (TOP-REAL (k + n)) such that

A8: ( x = v & v | k in Ak ) ;

x in A by A7, XBOOLE_0:def 4;

hence x in B by A3, A8; :: thesis: verum

then PP is open by A5, Th7;

then PP in the topology of (TOP-REAL (k + n)) by PRE_TOPC:def 2;

then A9: PP /\ ([#] ((TOP-REAL (k + n)) | A)) in the topology of ((TOP-REAL (k + n)) | A) by PRE_TOPC:def 4;

B c= PP /\ A

proof

then
B = PP /\ A
by A6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in PP /\ A )

assume x in B ; :: thesis: x in PP /\ A

then consider v being Element of (TOP-REAL (k + n)) such that

A10: x = v and

A11: v | k in Ak and

A12: v in A by A3;

v in PP by A11;

hence x in PP /\ A by A10, A12, XBOOLE_0:def 4; :: thesis: verum

end;assume x in B ; :: thesis: x in PP /\ A

then consider v being Element of (TOP-REAL (k + n)) such that

A10: x = v and

A11: v | k in Ak and

A12: v in A by A3;

v in PP by A11;

hence x in PP /\ A by A10, A12, XBOOLE_0:def 4; :: thesis: verum

hence B is open by A4, A9, PRE_TOPC:def 2; :: thesis: verum

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

then
p is open
by EUCLID_9:24;
let e be Point of (Euclid k); :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 1 / m > 0 & OpenHypercube (e,(1 / m)) c= p )

thus 1 / m > 0 by XREAL_1:139; :: thesis: OpenHypercube (e,(1 / m)) c= p

let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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)) ; :: thesis: 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; :: thesis: verum

end;( 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 ; :: thesis: 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 ; :: thesis: ( 1 / m > 0 & OpenHypercube (e,(1 / m)) c= p )

thus 1 / m > 0 by XREAL_1:139; :: thesis: OpenHypercube (e,(1 / m)) c= p

let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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)) ; :: thesis: 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; :: thesis: verum

then Ak in the topology of (TOP-REAL k) by A2, PRE_TOPC:def 2;

hence Ak is open by PRE_TOPC:def 2; :: thesis: verum