let M be non empty MetrSpace; :: thesis: for A being non empty SubSpace of M holds TopSpaceMetr A is SubSpace of TopSpaceMetr M
let A be non empty SubSpace of M; :: thesis: TopSpaceMetr A is SubSpace of TopSpaceMetr M
set T = TopSpaceMetr M;
set R = TopSpaceMetr A;
A1:
( [#] (TopSpaceMetr A) = the carrier of A & [#] (TopSpaceMetr M) = the carrier of M )
by Th16;
hence
[#] (TopSpaceMetr A) c= [#] (TopSpaceMetr M)
by Def1; :: according to PRE_TOPC:def 9 :: thesis: 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); :: thesis: ( ( 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)) ) )
:: thesis: ( 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
assume
P in the
topology of
(TopSpaceMetr A)
;
:: thesis: 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
by Th16;
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;
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;
:: thesis: ( x in Q implies ex r being Real st
( r > 0 & Ball x,r c= Q ) )
assume
x in Q
;
:: thesis: ex r being Real st
( r > 0 & Ball x,r c= Q )
then consider Y being
set such that A3:
(
x in Y &
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 A4:
Y = Ball x',
r
and
(
x' in P &
r > 0 &
(Ball x',r) /\ the
carrier of
A c= P )
by A3;
consider p being
Real such that A5:
(
p > 0 &
Ball x,
p c= Ball x',
r )
by A3, A4, PCOMPS_1:30;
take
p
;
:: thesis: ( p > 0 & Ball x,p c= Q )
thus
p > 0
by A5;
:: thesis: Ball x,p c= Q
Y c= Q
by A3, ZFMISC_1:92;
hence
Ball x,
p c= Q
by A4, A5, XBOOLE_1:1;
:: thesis: verum
end;
then A6:
Q in Family_open_set M
by PCOMPS_1:def 5;
reconsider Q' =
Q as
Subset of
(TopSpaceMetr M) by Th16;
take
Q'
;
:: thesis: ( Q' in the topology of (TopSpaceMetr M) & P = Q' /\ ([#] (TopSpaceMetr A)) )
thus
Q' in the
topology of
(TopSpaceMetr M)
by A6, Th16;
:: thesis: P = Q' /\ ([#] (TopSpaceMetr A))
thus
P = Q' /\ ([#] (TopSpaceMetr A))
:: thesis: verumproof
A7:
P c= Q' /\ ([#] (TopSpaceMetr A))
proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in P or a in Q' /\ ([#] (TopSpaceMetr A)) )
assume A8:
a in P
;
:: thesis: a in Q' /\ ([#] (TopSpaceMetr A))
then reconsider x =
a as
Point of
A by Th16;
reconsider P' =
P as
Subset of
A by Th16;
consider r being
Real such that A9:
(
r > 0 &
Ball x,
r c= P' )
by A2, A8, PCOMPS_1:def 5;
reconsider x' =
x as
Point of
M by Th12;
Ball x,
r = (Ball x',r) /\ the
carrier of
A
by Th13;
then
(
Ball x',
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 ) } &
x' in Ball x',
r )
by A8, A9, TBSP_1:16;
then
a in Q'
by TARSKI:def 4;
hence
a in Q' /\ ([#] (TopSpaceMetr A))
by A8, XBOOLE_0:def 4;
:: thesis: verum
end;
Q' /\ ([#] (TopSpaceMetr A)) c= P
proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in Q' /\ ([#] (TopSpaceMetr A)) or a in P )
assume A10:
a in Q' /\ ([#] (TopSpaceMetr A))
;
:: thesis: a in P
then
a in Q'
by XBOOLE_0:def 4;
then consider Y being
set such that A11:
(
a in Y &
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 A12:
Y = Ball x,
r
and
x in P
and
r > 0
and A13:
(Ball x,r) /\ the
carrier of
A c= P
by A11;
a in (Ball x,r) /\ the
carrier of
A
by A1, A10, A11, A12, XBOOLE_0:def 4;
hence
a in P
by A13;
:: thesis: verum
end;
hence
P = Q' /\ ([#] (TopSpaceMetr A))
by A7, XBOOLE_0:def 10;
:: thesis: verum
end;
end;
given Q being Subset of (TopSpaceMetr M) such that A14:
( Q in the topology of (TopSpaceMetr M) & P = Q /\ ([#] (TopSpaceMetr A)) )
; :: thesis: P in the topology of (TopSpaceMetr A)
reconsider Q' = Q as Subset of M by Th16;
reconsider P' = P as Subset of A by Th16;
for p being Point of A st p in P' holds
ex r being Real st
( r > 0 & Ball p,r c= P' )
proof
let p be
Point of
A;
:: thesis: ( p in P' implies ex r being Real st
( r > 0 & Ball p,r c= P' ) )
reconsider p' =
p as
Point of
M by Th12;
assume
p in P'
;
:: thesis: ex r being Real st
( r > 0 & Ball p,r c= P' )
then
(
p' in Q' &
Q' in Family_open_set M )
by A14, Th16, XBOOLE_0:def 4;
then consider r being
Real such that A15:
(
r > 0 &
Ball p',
r c= Q' )
by PCOMPS_1:def 5;
Ball p,
r = (Ball p',r) /\ the
carrier of
A
by Th13;
then
Ball p,
r c= Q /\ the
carrier of
A
by A15, XBOOLE_1:26;
then
Ball p,
r c= Q /\ the
carrier of
(TopSpaceMetr A)
by Th16;
hence
ex
r being
Real st
(
r > 0 &
Ball p,
r c= P' )
by A14, A15;
:: thesis: verum
end;
then
P in Family_open_set A
by PCOMPS_1:def 5;
hence
P in the topology of (TopSpaceMetr A)
by Th16; :: thesis: verum