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 4 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:76;
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 A1:
P in Family_open_set A
;
A2:
P c= Q9 /\ ([#] (TopSpaceMetr A))
proof
reconsider P9 =
P as
Subset of
A ;
let a be
object ;
TARSKI:def 3 ( not a in P or a in Q9 /\ ([#] (TopSpaceMetr A)) )
assume A3:
a in P
;
a in Q9 /\ ([#] (TopSpaceMetr A))
then reconsider x =
a as
Point of
A ;
reconsider x9 =
x as
Point of
M by Th8;
consider r being
Real such that A4:
r > 0
and A5:
Ball (
x,
r)
c= P9
by A1, A3, PCOMPS_1:def 4;
Ball (
x,
r)
= (Ball (x9,r)) /\ the
carrier of
A
by Th9;
then A6:
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 A3, A4, A5;
x9 in Ball (
x9,
r)
by A4, TBSP_1:11;
then
a in Q9
by A6, TARSKI:def 4;
hence
a in Q9 /\ ([#] (TopSpaceMetr A))
by A3, 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 A7:
x in Y
and A8:
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 A9:
Y = Ball (
x9,
r)
and
x9 in P
and
r > 0
and
(Ball (x9,r)) /\ the
carrier of
A c= P
by A8;
consider p being
Real such that A10:
p > 0
and A11:
Ball (
x,
p)
c= Ball (
x9,
r)
by A7, A9, PCOMPS_1:27;
take
p
;
( p > 0 & Ball (x,p) c= Q )
thus
p > 0
by A10;
Ball (x,p) c= Q
Y c= Q
by A8, ZFMISC_1:74;
hence
Ball (
x,
p)
c= Q
by A9, A11;
verum
end;
then
Q in Family_open_set M
by PCOMPS_1:def 4;
hence
Q9 in the
topology of
(TopSpaceMetr M)
;
P = Q9 /\ ([#] (TopSpaceMetr A))
Q9 /\ ([#] (TopSpaceMetr A)) c= P
proof
let a be
object ;
TARSKI:def 3 ( not a in Q9 /\ ([#] (TopSpaceMetr A)) or a in P )
assume A12:
a in Q9 /\ ([#] (TopSpaceMetr A))
;
a in P
then
a in Q9
by XBOOLE_0:def 4;
then consider Y being
set such that A13:
a in Y
and A14:
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 A15:
Y = Ball (
x,
r)
and
x in P
and
r > 0
and A16:
(Ball (x,r)) /\ the
carrier of
A c= P
by A14;
a in (Ball (x,r)) /\ the
carrier of
A
by A12, A13, A15, XBOOLE_0:def 4;
hence
a in P
by A16;
verum
end;
hence
P = Q9 /\ ([#] (TopSpaceMetr A))
by A2, XBOOLE_0:def 10;
verum
end;
reconsider P9 = P as Subset of A ;
given Q being Subset of (TopSpaceMetr M) such that A17:
Q in the topology of (TopSpaceMetr M)
and
A18:
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 Th8;
assume
p in P9
;
ex r being Real st
( r > 0 & Ball (p,r) c= P9 )
then A19:
p9 in Q9
by A18, XBOOLE_0:def 4;
Q9 in Family_open_set M
by A17;
then consider r being
Real such that A20:
r > 0
and A21:
Ball (
p9,
r)
c= Q9
by A19, PCOMPS_1:def 4;
Ball (
p,
r)
= (Ball (p9,r)) /\ the
carrier of
A
by Th9;
then
Ball (
p,
r)
c= Q /\ the
carrier of
A
by A21, 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 A18, A20;
verum
end;
then
P in Family_open_set A
by PCOMPS_1:def 4;
hence
P in the topology of (TopSpaceMetr A)
; verum