let n, k be Nat; 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); 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); ( 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
; ( 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 }
; ( An is open iff Ak is open )
hereby ( Ak is open implies An is open )
assume
An is
open
;
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 )
proof
(
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);
( 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
;
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;
( r > 0 & OpenHypercube (e,r) c= ak )
thus
r > 0
by XREAL_1:139;
OpenHypercube (e,r) c= ak
let y be
object ;
TARSKI:def 3 ( not y in OpenHypercube (e,r) or y in ak )
assume A8:
y in OpenHypercube (
e,
r)
;
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;
verum
end; then
ak 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
end;
assume
Ak is open
; An 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 )
proof
let e be
Point of
(Euclid n);
( e in an implies ex r being Real st
( r > 0 & OpenHypercube (e,r) c= an ) )
assume
e in an
;
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;
( r > 0 & OpenHypercube (e,r) c= an )
thus
r > 0
by XREAL_1:139;
OpenHypercube (e,r) c= an
let y be
object ;
TARSKI:def 3 ( not y in OpenHypercube (e,r) or y in an )
assume A17:
y in OpenHypercube (
e,
r)
;
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;
verum
end;
then
an is open
by EUCLID_9:24;
then
an in the topology of (TOP-REAL n)
by A1, PRE_TOPC:def 2;
hence
An is open
by PRE_TOPC:def 2; verum