let M be non empty MetrSpace; for A being non empty SubSpace of M holds TopSpaceMetr A is SubSpace of TopSpaceMetr M
let A be non empty SubSpace of M; TopSpaceMetr A is SubSpace of TopSpaceMetr M
set T = TopSpaceMetr M;
set R = TopSpaceMetr A;
thus
[#] (TopSpaceMetr A) c= [#] (TopSpaceMetr M)
by Def1; PRE_TOPC:def 9 for b1 being Element of bool the carrier of (TopSpaceMetr A) holds
( ( not b1 in the topology of (TopSpaceMetr A) or ex b2 being Element of bool the carrier of (TopSpaceMetr M) st
( b2 in the topology of (TopSpaceMetr M) & b1 = b2 /\ ([#] (TopSpaceMetr A)) ) ) & ( for b2 being Element of bool the carrier of (TopSpaceMetr M) holds
( not b2 in the topology of (TopSpaceMetr M) or not b1 = b2 /\ ([#] (TopSpaceMetr A)) ) or b1 in the topology of (TopSpaceMetr A) ) )
let P be Subset of (TopSpaceMetr A); ( ( not P in the topology of (TopSpaceMetr A) or ex b1 being Element of bool the carrier of (TopSpaceMetr M) st
( b1 in the topology of (TopSpaceMetr M) & P = b1 /\ ([#] (TopSpaceMetr A)) ) ) & ( for b1 being Element of bool the carrier of (TopSpaceMetr M) holds
( not b1 in the topology of (TopSpaceMetr M) or not P = b1 /\ ([#] (TopSpaceMetr A)) ) or P in the topology of (TopSpaceMetr A) ) )
thus
( P in the topology of (TopSpaceMetr A) implies ex Q being Subset of (TopSpaceMetr M) st
( Q in the topology of (TopSpaceMetr M) & P = Q /\ ([#] (TopSpaceMetr A)) ) )
( for b1 being Element of bool the carrier of (TopSpaceMetr M) holds
( not b1 in the topology of (TopSpaceMetr M) or not P = b1 /\ ([#] (TopSpaceMetr A)) ) or P in the topology of (TopSpaceMetr A) )proof
set QQ =
{ (Ball x,r) where x is Point of M, r is Real : ( x in P & r > 0 & (Ball x,r) /\ the carrier of A c= P ) } ;
for
X being
set st
X in { (Ball x,r) where x is Point of M, r is Real : ( x in P & r > 0 & (Ball x,r) /\ the carrier of A c= P ) } holds
X c= the
carrier of
M
then reconsider Q =
union { (Ball x,r) where x is Point of M, r is Real : ( x in P & r > 0 & (Ball x,r) /\ the carrier of A c= P ) } as
Subset of
M by ZFMISC_1:94;
reconsider Q9 =
Q as
Subset of
(TopSpaceMetr M) ;
assume
P in the
topology of
(TopSpaceMetr A)
;
ex Q being Subset of (TopSpaceMetr M) st
( Q in the topology of (TopSpaceMetr M) & P = Q /\ ([#] (TopSpaceMetr A)) )
then A2:
P in Family_open_set A
;
A3:
P c= Q9 /\ ([#] (TopSpaceMetr A))
proof
reconsider P9 =
P as
Subset of
A ;
let a be
set ;
TARSKI:def 3 ( not a in P or a in Q9 /\ ([#] (TopSpaceMetr A)) )
assume A4:
a in P
;
a in Q9 /\ ([#] (TopSpaceMetr A))
then reconsider x =
a as
Point of
A ;
reconsider x9 =
x as
Point of
M by Th12;
consider r being
Real such that A5:
r > 0
and A6:
Ball x,
r c= P9
by A2, A4, PCOMPS_1:def 5;
Ball x,
r = (Ball x9,r) /\ the
carrier of
A
by Th13;
then A7:
Ball x9,
r in { (Ball x,r) where x is Point of M, r is Real : ( x in P & r > 0 & (Ball x,r) /\ the carrier of A c= P ) }
by A4, A5, A6;
x9 in Ball x9,
r
by A5, TBSP_1:16;
then
a in Q9
by A7, TARSKI:def 4;
hence
a in Q9 /\ ([#] (TopSpaceMetr A))
by A4, XBOOLE_0:def 4;
verum
end;
take
Q9
;
( Q9 in the topology of (TopSpaceMetr M) & P = Q9 /\ ([#] (TopSpaceMetr A)) )
for
x being
Point of
M st
x in Q holds
ex
r being
Real st
(
r > 0 &
Ball x,
r c= Q )
proof
let x be
Point of
M;
( x in Q implies ex r being Real st
( r > 0 & Ball x,r c= Q ) )
assume
x in Q
;
ex r being Real st
( r > 0 & Ball x,r c= Q )
then consider Y being
set such that A8:
x in Y
and A9:
Y in { (Ball x,r) where x is Point of M, r is Real : ( x in P & r > 0 & (Ball x,r) /\ the carrier of A c= P ) }
by TARSKI:def 4;
consider x9 being
Point of
M,
r being
Real such that A10:
Y = Ball x9,
r
and
x9 in P
and
r > 0
and
(Ball x9,r) /\ the
carrier of
A c= P
by A9;
consider p being
Real such that A11:
p > 0
and A12:
Ball x,
p c= Ball x9,
r
by A8, A10, PCOMPS_1:30;
take
p
;
( p > 0 & Ball x,p c= Q )
thus
p > 0
by A11;
Ball x,p c= Q
Y c= Q
by A9, ZFMISC_1:92;
hence
Ball x,
p c= Q
by A10, A12, XBOOLE_1:1;
verum
end;
then
Q in Family_open_set M
by PCOMPS_1:def 5;
hence
Q9 in the
topology of
(TopSpaceMetr M)
;
P = Q9 /\ ([#] (TopSpaceMetr A))
Q9 /\ ([#] (TopSpaceMetr A)) c= P
proof
let a be
set ;
TARSKI:def 3 ( not a in Q9 /\ ([#] (TopSpaceMetr A)) or a in P )
assume A13:
a in Q9 /\ ([#] (TopSpaceMetr A))
;
a in P
then
a in Q9
by XBOOLE_0:def 4;
then consider Y being
set such that A14:
a in Y
and A15:
Y in { (Ball x,r) where x is Point of M, r is Real : ( x in P & r > 0 & (Ball x,r) /\ the carrier of A c= P ) }
by TARSKI:def 4;
consider x being
Point of
M,
r being
Real such that A16:
Y = Ball x,
r
and
x in P
and
r > 0
and A17:
(Ball x,r) /\ the
carrier of
A c= P
by A15;
a in (Ball x,r) /\ the
carrier of
A
by A13, A14, A16, XBOOLE_0:def 4;
hence
a in P
by A17;
verum
end;
hence
P = Q9 /\ ([#] (TopSpaceMetr A))
by A3, XBOOLE_0:def 10;
verum
end;
reconsider P9 = P as Subset of A ;
given Q being Subset of (TopSpaceMetr M) such that A18:
Q in the topology of (TopSpaceMetr M)
and
A19:
P = Q /\ ([#] (TopSpaceMetr A))
; P in the topology of (TopSpaceMetr A)
reconsider Q9 = Q as Subset of M ;
for p being Point of A st p in P9 holds
ex r being Real st
( r > 0 & Ball p,r c= P9 )
proof
let p be
Point of
A;
( p in P9 implies ex r being Real st
( r > 0 & Ball p,r c= P9 ) )
reconsider p9 =
p as
Point of
M by Th12;
assume
p in P9
;
ex r being Real st
( r > 0 & Ball p,r c= P9 )
then A20:
p9 in Q9
by A19, XBOOLE_0:def 4;
Q9 in Family_open_set M
by A18;
then consider r being
Real such that A21:
r > 0
and A22:
Ball p9,
r c= Q9
by A20, PCOMPS_1:def 5;
Ball p,
r = (Ball p9,r) /\ the
carrier of
A
by Th13;
then
Ball p,
r c= Q /\ the
carrier of
A
by A22, XBOOLE_1:26;
then
Ball p,
r c= Q /\ the
carrier of
(TopSpaceMetr A)
;
hence
ex
r being
Real st
(
r > 0 &
Ball p,
r c= P9 )
by A19, A21;
verum
end;
then
P in Family_open_set A
by PCOMPS_1:def 5;
hence
P in the topology of (TopSpaceMetr A)
; verum