let n, k be Nat; :: thesis: for An being Subset of (TOP-REAL n)

for Ak being Subset of (TOP-REAL k) st k <= n & An = { v where v is Element of (TOP-REAL n) : v | k in Ak } holds

( An is open iff Ak is open )

let An be Subset of (TOP-REAL n); :: thesis: for Ak being Subset of (TOP-REAL k) st k <= n & An = { v where v is Element of (TOP-REAL n) : v | k in Ak } holds

( An is open iff Ak is open )

let Ak be Subset of (TOP-REAL k); :: thesis: ( k <= n & An = { v where v is Element of (TOP-REAL n) : v | k in Ak } implies ( An is open iff Ak is open ) )

assume k <= n ; :: thesis: ( not An = { v where v is Element of (TOP-REAL n) : v | k in Ak } or ( An is open iff Ak is open ) )

then reconsider nk = n - k as Element of NAT by NAT_1:21;

A1: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;

then reconsider an = An as Subset of (TopSpaceMetr (Euclid n)) ;

A2: TopStruct(# the carrier of (TOP-REAL k), the topology of (TOP-REAL k) #) = TopSpaceMetr (Euclid k) by EUCLID:def 8;

then reconsider ak = Ak as Subset of (TopSpaceMetr (Euclid k)) ;

assume A3: An = { v where v is Element of (TOP-REAL n) : v | k in Ak } ; :: thesis: ( An is open iff Ak is open )

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

then A12: ak is open by A2, PRE_TOPC:def 2;

for e being Point of (Euclid n) st e in an holds

ex r being Real st

( r > 0 & OpenHypercube (e,r) c= an )

then an in the topology of (TOP-REAL n) by A1, PRE_TOPC:def 2;

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

for Ak being Subset of (TOP-REAL k) st k <= n & An = { v where v is Element of (TOP-REAL n) : v | k in Ak } holds

( An is open iff Ak is open )

let An be Subset of (TOP-REAL n); :: thesis: for Ak being Subset of (TOP-REAL k) st k <= n & An = { v where v is Element of (TOP-REAL n) : v | k in Ak } holds

( An is open iff Ak is open )

let Ak be Subset of (TOP-REAL k); :: thesis: ( k <= n & An = { v where v is Element of (TOP-REAL n) : v | k in Ak } implies ( An is open iff Ak is open ) )

assume k <= n ; :: thesis: ( not An = { v where v is Element of (TOP-REAL n) : v | k in Ak } or ( An is open iff Ak is open ) )

then reconsider nk = n - k as Element of NAT by NAT_1:21;

A1: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;

then reconsider an = An as Subset of (TopSpaceMetr (Euclid n)) ;

A2: TopStruct(# the carrier of (TOP-REAL k), the topology of (TOP-REAL k) #) = TopSpaceMetr (Euclid k) by EUCLID:def 8;

then reconsider ak = Ak as Subset of (TopSpaceMetr (Euclid k)) ;

assume A3: An = { v where v is Element of (TOP-REAL n) : v | k in Ak } ; :: thesis: ( An is open iff Ak is open )

hereby :: thesis: ( Ak is open implies An is open )

assume
Ak is open
; :: thesis: An is open assume
An is open
; :: thesis: Ak is open

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

then A4: an is open by A1, PRE_TOPC:def 2;

for e being Point of (Euclid k) st e in ak holds

ex r being Real st

( r > 0 & OpenHypercube (e,r) c= ak )

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

end;then an in the topology of (TOP-REAL n) by PRE_TOPC:def 2;

then A4: an is open by A1, PRE_TOPC:def 2;

for e being Point of (Euclid k) st e in ak holds

ex r being Real st

( r > 0 & OpenHypercube (e,r) c= ak )

proof

then
ak is open
by EUCLID_9:24;
( len (nk |-> 0) = nk & @ (@ (nk |-> 0)) = nk |-> 0 )
by CARD_1:def 7;

then reconsider nk0 = nk |-> 0 as Point of (Euclid nk) by TOPREAL3:45;

let e be Point of (Euclid k); :: thesis: ( e in ak implies ex r being Real st

( r > 0 & OpenHypercube (e,r) c= ak ) )

A5: ( @ (@ (e ^ (nk |-> 0))) = e ^ (nk |-> 0) & len (e ^ nk0) = n ) by CARD_1:def 7;

then reconsider en = e ^ nk0 as Point of (Euclid n) by TOPREAL3:45;

reconsider En = e ^ nk0 as Point of (TOP-REAL n) by A5, TOPREAL3:46;

len e = k by CARD_1:def 7;

then dom e = Seg k by FINSEQ_1:def 3;

then A6: e = En | k by FINSEQ_1:21;

assume e in ak ; :: thesis: ex r being Real st

( r > 0 & OpenHypercube (e,r) c= ak )

then en in an by A3, A6;

then consider m being non zero Element of NAT such that

A7: OpenHypercube (en,(1 / m)) c= an by A4, EUCLID_9:23;

take r = 1 / m; :: thesis: ( r > 0 & OpenHypercube (e,r) c= ak )

thus r > 0 by XREAL_1:139; :: thesis: OpenHypercube (e,r) c= ak

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in OpenHypercube (e,r) or y in ak )

assume A8: y in OpenHypercube (e,r) ; :: thesis: y in ak

then reconsider p = y as Point of (TopSpaceMetr (Euclid k)) ;

A9: p in product (Intervals (e,r)) by A8, EUCLID_9:def 4;

reconsider P = p as Point of (TOP-REAL k) by A2;

nk0 in OpenHypercube (nk0,r) by EUCLID_9:11, XREAL_1:139;

then A10: nk0 in product (Intervals (nk0,r)) by EUCLID_9:def 4;

(Intervals (e,r)) ^ (Intervals (nk0,r)) = Intervals (en,r) by Th1;

then P ^ nk0 in product (Intervals (en,r)) by A10, A9, Th2;

then P ^ nk0 in OpenHypercube (en,r) by EUCLID_9:def 4;

then P ^ nk0 in an by A7;

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

A11: ( v = P ^ nk0 & v | k in Ak ) by A3;

len P = k by CARD_1:def 7;

then dom P = Seg k by FINSEQ_1:def 3;

hence y in ak by A11, FINSEQ_1:21; :: thesis: verum

end;then reconsider nk0 = nk |-> 0 as Point of (Euclid nk) by TOPREAL3:45;

let e be Point of (Euclid k); :: thesis: ( e in ak implies ex r being Real st

( r > 0 & OpenHypercube (e,r) c= ak ) )

A5: ( @ (@ (e ^ (nk |-> 0))) = e ^ (nk |-> 0) & len (e ^ nk0) = n ) by CARD_1:def 7;

then reconsider en = e ^ nk0 as Point of (Euclid n) by TOPREAL3:45;

reconsider En = e ^ nk0 as Point of (TOP-REAL n) by A5, TOPREAL3:46;

len e = k by CARD_1:def 7;

then dom e = Seg k by FINSEQ_1:def 3;

then A6: e = En | k by FINSEQ_1:21;

assume e in ak ; :: thesis: ex r being Real st

( r > 0 & OpenHypercube (e,r) c= ak )

then en in an by A3, A6;

then consider m being non zero Element of NAT such that

A7: OpenHypercube (en,(1 / m)) c= an by A4, EUCLID_9:23;

take r = 1 / m; :: thesis: ( r > 0 & OpenHypercube (e,r) c= ak )

thus r > 0 by XREAL_1:139; :: thesis: OpenHypercube (e,r) c= ak

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in OpenHypercube (e,r) or y in ak )

assume A8: y in OpenHypercube (e,r) ; :: thesis: y in ak

then reconsider p = y as Point of (TopSpaceMetr (Euclid k)) ;

A9: p in product (Intervals (e,r)) by A8, EUCLID_9:def 4;

reconsider P = p as Point of (TOP-REAL k) by A2;

nk0 in OpenHypercube (nk0,r) by EUCLID_9:11, XREAL_1:139;

then A10: nk0 in product (Intervals (nk0,r)) by EUCLID_9:def 4;

(Intervals (e,r)) ^ (Intervals (nk0,r)) = Intervals (en,r) by Th1;

then P ^ nk0 in product (Intervals (en,r)) by A10, A9, Th2;

then P ^ nk0 in OpenHypercube (en,r) by EUCLID_9:def 4;

then P ^ nk0 in an by A7;

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

A11: ( v = P ^ nk0 & v | k in Ak ) by A3;

len P = k by CARD_1:def 7;

then dom P = Seg k by FINSEQ_1:def 3;

hence y in ak by A11, FINSEQ_1:21; :: 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

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

then A12: ak is open by A2, PRE_TOPC:def 2;

for e being Point of (Euclid n) st e in an holds

ex r being Real st

( r > 0 & OpenHypercube (e,r) c= an )

proof

then
an is open
by EUCLID_9:24;
let e be Point of (Euclid n); :: thesis: ( e in an implies ex r being Real st

( r > 0 & OpenHypercube (e,r) c= an ) )

assume e in an ; :: thesis: ex r being Real st

( r > 0 & OpenHypercube (e,r) c= an )

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

A13: e = v and

A14: v | k in Ak by A3;

reconsider vk = v | k as Point of (TOP-REAL k) by A14;

A15: len vk = k by CARD_1:def 7;

@ (@ vk) = vk ;

then reconsider Vk = vk as Point of (Euclid k) by A15, TOPREAL3:45;

consider m being non zero Element of NAT such that

A16: OpenHypercube (Vk,(1 / m)) c= ak by A12, A14, EUCLID_9:23;

take r = 1 / m; :: thesis: ( r > 0 & OpenHypercube (e,r) c= an )

thus r > 0 by XREAL_1:139; :: thesis: OpenHypercube (e,r) c= an

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in OpenHypercube (e,r) or y in an )

assume A17: y in OpenHypercube (e,r) ; :: thesis: y in an

then A18: y in product (Intervals (e,r)) by EUCLID_9:def 4;

reconsider Y = y as Point of (TOP-REAL n) by A1, A17;

A19: len v = n by CARD_1:def 7;

consider q being FinSequence such that

A20: @ (@ v) = vk ^ q by FINSEQ_1:80;

reconsider q = q as FinSequence of REAL by A20, FINSEQ_1:36;

len v = (len vk) + (len q) by A20, FINSEQ_1:22;

then reconsider Q = q as Point of (Euclid nk) by A15, A19, TOPREAL3:45;

(Intervals (Vk,r)) ^ (Intervals (Q,r)) = Intervals (e,r) by A13, A20, Th1;

then consider p1, p2 being FinSequence such that

A21: y = p1 ^ p2 and

A22: p1 in product (Intervals (Vk,r)) and

p2 in product (Intervals (Q,r)) by A18, Th2;

A23: p1 in OpenHypercube (Vk,(1 / m)) by A22, EUCLID_9:def 4;

then len p1 = k by A2, CARD_1:def 7;

then Y | k = Y | (dom p1) by FINSEQ_1:def 3

.= p1 by A21, FINSEQ_1:21 ;

hence y in an by A3, A16, A23; :: thesis: verum

end;( r > 0 & OpenHypercube (e,r) c= an ) )

assume e in an ; :: thesis: ex r being Real st

( r > 0 & OpenHypercube (e,r) c= an )

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

A13: e = v and

A14: v | k in Ak by A3;

reconsider vk = v | k as Point of (TOP-REAL k) by A14;

A15: len vk = k by CARD_1:def 7;

@ (@ vk) = vk ;

then reconsider Vk = vk as Point of (Euclid k) by A15, TOPREAL3:45;

consider m being non zero Element of NAT such that

A16: OpenHypercube (Vk,(1 / m)) c= ak by A12, A14, EUCLID_9:23;

take r = 1 / m; :: thesis: ( r > 0 & OpenHypercube (e,r) c= an )

thus r > 0 by XREAL_1:139; :: thesis: OpenHypercube (e,r) c= an

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in OpenHypercube (e,r) or y in an )

assume A17: y in OpenHypercube (e,r) ; :: thesis: y in an

then A18: y in product (Intervals (e,r)) by EUCLID_9:def 4;

reconsider Y = y as Point of (TOP-REAL n) by A1, A17;

A19: len v = n by CARD_1:def 7;

consider q being FinSequence such that

A20: @ (@ v) = vk ^ q by FINSEQ_1:80;

reconsider q = q as FinSequence of REAL by A20, FINSEQ_1:36;

len v = (len vk) + (len q) by A20, FINSEQ_1:22;

then reconsider Q = q as Point of (Euclid nk) by A15, A19, TOPREAL3:45;

(Intervals (Vk,r)) ^ (Intervals (Q,r)) = Intervals (e,r) by A13, A20, Th1;

then consider p1, p2 being FinSequence such that

A21: y = p1 ^ p2 and

A22: p1 in product (Intervals (Vk,r)) and

p2 in product (Intervals (Q,r)) by A18, Th2;

A23: p1 in OpenHypercube (Vk,(1 / m)) by A22, EUCLID_9:def 4;

then len p1 = k by A2, CARD_1:def 7;

then Y | k = Y | (dom p1) by FINSEQ_1:def 3

.= p1 by A21, FINSEQ_1:21 ;

hence y in an by A3, A16, A23; :: thesis: verum

then an in the topology of (TOP-REAL n) by A1, PRE_TOPC:def 2;

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