let PM be non empty MetrSpace; TopSpaceMetr PM is T_2
set TPS = TopSpaceMetr PM;
for x, y being Element of (TopSpaceMetr PM) st not x = y holds
ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V )
proof
let x,
y be
Element of
(TopSpaceMetr PM);
( not x = y implies ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V ) )
assume A1:
not
x = y
;
ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V )
reconsider x =
x,
y =
y as
Element of
PM ;
set r =
(dist (x,y)) / 2;
dist (
x,
y)
<> 0
by A1, METRIC_1:2;
then
dist (
x,
y)
> 0
by METRIC_1:5;
then A2:
(dist (x,y)) / 2
> 0
by XREAL_1:139;
ex
W,
V being
Subset of
(TopSpaceMetr PM) st
(
W is
open &
V is
open &
x in W &
y in V &
W misses V )
proof
set V =
Ball (
y,
((dist (x,y)) / 2));
set W =
Ball (
x,
((dist (x,y)) / 2));
A3:
(
Ball (
x,
((dist (x,y)) / 2))
in Family_open_set PM &
Ball (
y,
((dist (x,y)) / 2))
in Family_open_set PM )
by Th29;
reconsider W =
Ball (
x,
((dist (x,y)) / 2)),
V =
Ball (
y,
((dist (x,y)) / 2)) as
Subset of
(TopSpaceMetr PM) ;
A4:
for
z being
object holds not
z in W /\ V
proof
let z be
object ;
not z in W /\ V
assume A5:
z in W /\ V
;
contradiction
then reconsider z =
z as
Element of
PM ;
z in V
by A5, XBOOLE_0:def 4;
then A6:
dist (
y,
z)
< (dist (x,y)) / 2
by METRIC_1:11;
z in W
by A5, XBOOLE_0:def 4;
then
dist (
x,
z)
< (dist (x,y)) / 2
by METRIC_1:11;
then
(dist (x,z)) + (dist (y,z)) < ((dist (x,y)) / 2) + ((dist (x,y)) / 2)
by A6, XREAL_1:8;
hence
contradiction
by METRIC_1:4;
verum
end;
take
W
;
ex V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V )
take
V
;
( W is open & V is open & x in W & y in V & W misses V )
(
dist (
x,
x)
= 0 &
dist (
y,
y)
= 0 )
by METRIC_1:1;
hence
(
W is
open &
V is
open &
x in W &
y in V &
W misses V )
by A2, A3, A4, METRIC_1:11, PRE_TOPC:def 2, XBOOLE_0:4;
verum
end;
hence
ex
W,
V being
Subset of
(TopSpaceMetr PM) st
(
W is
open &
V is
open &
x in W &
y in V &
W misses V )
;
verum
end;
hence
TopSpaceMetr PM is T_2
by PRE_TOPC:def 10; verum