let TM be metrizable TopSpace; for A, B being Subset of TM st A,B are_separated holds
ex U, W being open Subset of TM st
( A c= U & B c= W & U misses W )
let A, B be Subset of TM; ( A,B are_separated implies ex U, W being open Subset of TM st
( A c= U & B c= W & U misses W ) )
assume A1:
A,B are_separated
; ex U, W being open Subset of TM st
( A c= U & B c= W & U misses W )
set TOP = the topology of TM;
set cTM = the carrier of TM;
consider metr being Function of [: the carrier of TM, the carrier of TM:],REAL such that
A2:
metr is_metric_of the carrier of TM
and
A3:
Family_open_set (SpaceMetr ( the carrier of TM,metr)) = the topology of TM
by PCOMPS_1:def 8;
per cases
( A = {} TM or B = {} TM or ( A <> {} TM & B <> {} TM ) )
;
suppose A6:
(
A <> {} TM &
B <> {} TM )
;
ex U, W being open Subset of TM st
( A c= U & B c= W & U misses W )then A7:
not
TM is
empty
;
then reconsider Tm =
SpaceMetr ( the
carrier of
TM,
metr) as non
empty MetrSpace by A2, PCOMPS_1:36;
set TTm =
TopSpaceMetr Tm;
reconsider A9 =
A,
B9 =
B as
Subset of
(TopSpaceMetr Tm) by A2, A7, PCOMPS_2:4;
set dA =
dist_min A9;
set dB =
dist_min B9;
reconsider U =
{ p where p is Point of Tm : ((dist_min A9) . p) - ((dist_min B9) . p) < 0 } ,
W =
{ p where p is Point of Tm : ((dist_min B9) . p) - ((dist_min A9) . p) < 0 } as
open Subset of
(TopSpaceMetr Tm) by A6, Lm12;
(
U in Family_open_set Tm &
W in Family_open_set Tm )
by PRE_TOPC:def 2;
then reconsider U =
U,
W =
W as
open Subset of
TM by A3, PRE_TOPC:def 2;
take
U
;
ex W being open Subset of TM st
( A c= U & B c= W & U misses W )take
W
;
( A c= U & B c= W & U misses W )A8:
[#] TM = [#] (TopSpaceMetr Tm)
by A2, A7, PCOMPS_2:4;
thus
A c= U
( B c= W & U misses W )proof
let x be
object ;
TARSKI:def 3 ( not x in A or x in U )
assume A9:
x in A
;
x in U
then reconsider p =
x as
Point of
Tm by A2, A7, PCOMPS_2:4;
A misses Cl B
by A1, CONNSP_1:def 1;
then
not
x in Cl B
by A9, XBOOLE_0:3;
then
not
x in Cl B9
by A3, A8, TOPS_3:80;
then A10:
(dist_min B9) . p <> 0
by A6, HAUSDORF:8;
A11:
(dist_min B9) . p >= 0
by A6, JORDAN1K:9;
(dist_min A9) . p = 0
by A9, HAUSDORF:5;
then
((dist_min A9) . p) - ((dist_min B9) . p) < 0
by A10, A11;
hence
x in U
;
verum
end; thus
B c= W
U misses Wproof
let x be
object ;
TARSKI:def 3 ( not x in B or x in W )
assume A12:
x in B
;
x in W
then reconsider p =
x as
Point of
Tm by A2, A7, PCOMPS_2:4;
B misses Cl A
by A1, CONNSP_1:def 1;
then
not
x in Cl A
by A12, XBOOLE_0:3;
then
not
x in Cl A9
by A3, A8, TOPS_3:80;
then A13:
(dist_min A9) . p <> 0
by A6, HAUSDORF:8;
A14:
(dist_min A9) . p >= 0
by A6, JORDAN1K:9;
(dist_min B9) . p = 0
by A12, HAUSDORF:5;
then
((dist_min B9) . p) - ((dist_min A9) . p) < 0
by A13, A14;
hence
x in W
;
verum
end; thus
U misses W
verum end;