let T be non empty TopSpace; ( T is metrizable implies ( T is regular & T is T_1 ) )
assume
T is metrizable
; ( T is regular & T is T_1 )
then consider metr being Function of [: the carrier of T, the carrier of T:],REAL such that
A1:
metr is_metric_of the carrier of T
and
A2:
Family_open_set (SpaceMetr ( the carrier of T,metr)) = the topology of T
;
set PM = SpaceMetr ( the carrier of T,metr);
reconsider PM = SpaceMetr ( the carrier of T,metr) as non empty MetrSpace by A1, PCOMPS_1:36;
set TPM = TopSpaceMetr PM;
A3:
for p being Element of T
for D being Subset of T st D <> {} & D is closed & p in D ` holds
ex A, B being Subset of T st
( A is open & B is open & p in A & D c= B & A misses B )
proof
let p be
Element of
T;
for D being Subset of T st D <> {} & D is closed & p in D ` holds
ex A, B being Subset of T st
( A is open & B is open & p in A & D c= B & A misses B )let D be
Subset of
T;
( D <> {} & D is closed & p in D ` implies ex A, B being Subset of T st
( A is open & B is open & p in A & D c= B & A misses B ) )
assume that
D <> {}
and A4:
D is
closed
and A5:
p in D `
;
ex A, B being Subset of T st
( A is open & B is open & p in A & D c= B & A misses B )
A6:
([#] T) \ D in the
topology of
T
by A4, A5, PRE_TOPC:def 2;
reconsider p =
p as
Element of
PM by A1, PCOMPS_2:4;
A7:
D misses D `
by XBOOLE_1:79;
reconsider D =
D as
Subset of
(TopSpaceMetr PM) by A1, PCOMPS_2:4;
([#] (TopSpaceMetr PM)) \ D in Family_open_set PM
by A1, A2, A6, PCOMPS_2:4;
then
([#] (TopSpaceMetr PM)) \ D is
open
by PRE_TOPC:def 2;
then A8:
D is
closed
by PRE_TOPC:def 3;
A9:
not
p in D
by A5, A7, XBOOLE_0:3;
ex
r1 being
Real st
(
r1 > 0 &
Ball (
p,
r1)
misses D )
then consider r1 being
Real such that A15:
r1 > 0
and A16:
Ball (
p,
r1)
misses D
;
set r2 =
r1 / 2;
A17:
r1 / 2
< (r1 / 2) + (r1 / 2)
by A15, XREAL_1:29;
A18:
D c= ([#] PM) \ (cl_Ball (p,(r1 / 2)))
proof
assume
not
D c= ([#] PM) \ (cl_Ball (p,(r1 / 2)))
;
contradiction
then consider x being
object such that A19:
x in D
and A20:
not
x in ([#] PM) \ (cl_Ball (p,(r1 / 2)))
;
reconsider x =
x as
Element of
PM by A19;
x in cl_Ball (
p,
(r1 / 2))
by A20, XBOOLE_0:def 5;
then
dist (
p,
x)
<= r1 / 2
by METRIC_1:12;
then
dist (
p,
x)
< r1
by A17, XXREAL_0:2;
then
x in Ball (
p,
r1)
by METRIC_1:11;
hence
contradiction
by A16, A19, XBOOLE_0:3;
verum
end;
set r4 =
(r1 / 2) / 2;
A21:
r1 / 2
> 0
by A15, XREAL_1:139;
then A22:
(r1 / 2) / 2
< ((r1 / 2) / 2) + ((r1 / 2) / 2)
by XREAL_1:29;
A23:
Ball (
p,
((r1 / 2) / 2))
misses ([#] PM) \ (cl_Ball (p,(r1 / 2)))
proof
assume
Ball (
p,
((r1 / 2) / 2))
meets ([#] PM) \ (cl_Ball (p,(r1 / 2)))
;
contradiction
then consider x being
object such that A24:
x in Ball (
p,
((r1 / 2) / 2))
and A25:
x in ([#] PM) \ (cl_Ball (p,(r1 / 2)))
by XBOOLE_0:3;
reconsider x =
x as
Element of
PM by A24;
not
x in cl_Ball (
p,
(r1 / 2))
by A25, XBOOLE_0:def 5;
then A26:
dist (
p,
x)
> r1 / 2
by METRIC_1:12;
dist (
p,
x)
< (r1 / 2) / 2
by A24, METRIC_1:11;
hence
contradiction
by A22, A26, XXREAL_0:2;
verum
end;
set A =
Ball (
p,
((r1 / 2) / 2));
set B =
([#] PM) \ (cl_Ball (p,(r1 / 2)));
A27:
(
([#] PM) \ (cl_Ball (p,(r1 / 2))) in Family_open_set PM &
Ball (
p,
((r1 / 2) / 2))
in Family_open_set PM )
by Th14, PCOMPS_1:29;
then reconsider A =
Ball (
p,
((r1 / 2) / 2)),
B =
([#] PM) \ (cl_Ball (p,(r1 / 2))) as
Subset of
T by A2;
take
A
;
ex B being Subset of T st
( A is open & B is open & p in A & D c= B & A misses B )
take
B
;
( A is open & B is open & p in A & D c= B & A misses B )
(r1 / 2) / 2
> 0
by A21, XREAL_1:139;
then
dist (
p,
p)
< (r1 / 2) / 2
by METRIC_1:1;
hence
(
A is
open &
B is
open &
p in A &
D c= B &
A misses B )
by A2, A18, A23, A27, METRIC_1:11, PRE_TOPC:def 2;
verum
end;
for p, q being Point of T st not p = q holds
ex A, B being Subset of T st
( A is open & B is open & p in A & not q in A & q in B & not p in B )
proof
let p,
q be
Point of
T;
( not p = q implies ex A, B being Subset of T st
( A is open & B is open & p in A & not q in A & q in B & not p in B ) )
assume A28:
not
p = q
;
ex A, B being Subset of T st
( A is open & B is open & p in A & not q in A & q in B & not p in B )
reconsider p =
p,
q =
q as
Element of
(TopSpaceMetr PM) by A1, PCOMPS_2:4;
TopSpaceMetr PM is
T_2
by PCOMPS_1:34;
then consider A,
B being
Subset of
(TopSpaceMetr PM) such that A29:
A is
open
and A30:
B is
open
and A31:
(
p in A &
q in B )
and A32:
A misses B
by A28, PRE_TOPC:def 10;
reconsider A =
A,
B =
B as
Subset of
T by A1, PCOMPS_2:4;
A in the
topology of
T
by A2, A29, PRE_TOPC:def 2;
then A33:
A is
open
by PRE_TOPC:def 2;
B in the
topology of
T
by A2, A30, PRE_TOPC:def 2;
then A34:
B is
open
by PRE_TOPC:def 2;
( not
q in A & not
p in B )
by A31, A32, XBOOLE_0:3;
hence
ex
A,
B being
Subset of
T st
(
A is
open &
B is
open &
p in A & not
q in A &
q in B & not
p in B )
by A31, A33, A34;
verum
end;
hence
( T is regular & T is T_1 )
by A3, URYSOHN1:def 7; verum