let T be non empty TopSpace; for pmet being Function of [:the carrier of T,the carrier of T:],REAL st pmet is_metric_of the carrier of T & ( for A being non empty Subset of T holds Cl A = { p where p is Point of T : (inf pmet,A) . p = 0 } ) holds
T is metrizable
let pmet be Function of [:the carrier of T,the carrier of T:],REAL ; ( pmet is_metric_of the carrier of T & ( for A being non empty Subset of T holds Cl A = { p where p is Point of T : (inf pmet,A) . p = 0 } ) implies T is metrizable )
assume that
A1:
pmet is_metric_of the carrier of T
and
A2:
for A being non empty Subset of T holds Cl A = { p where p is Point of T : (inf pmet,A) . p = 0 }
; T is metrizable
set PM = SpaceMetr the carrier of T,pmet;
reconsider PM = SpaceMetr the carrier of T,pmet as non empty MetrSpace by A1, PCOMPS_1:40;
A3:
for x, y being Element of PM holds pmet . x,y = dist x,y
A4:
Family_open_set PM c= the topology of T
proof
let A be
set ;
TARSKI:def 3 ( not A in Family_open_set PM or A in the topology of T )
assume A5:
A in Family_open_set PM
;
A in the topology of T
then reconsider AT =
A as
Subset of
T by A1, PCOMPS_2:8;
per cases
( AT ` is empty or not AT ` is empty )
;
suppose A6:
not
AT ` is
empty
;
A in the topology of T
for
x being
set holds
(
x in AT iff ex
U being
Subset of
T st
(
U is
open &
U c= AT &
x in U ) )
proof
let x be
set ;
( x in AT iff ex U being Subset of T st
( U is open & U c= AT & x in U ) )
(
x in AT implies ex
U being
Subset of
T st
(
U is
open &
U c= AT &
x in U ) )
proof
assume A7:
x in AT
;
ex U being Subset of T st
( U is open & U c= AT & x in U )
then reconsider xP =
x as
Element of
PM by A1, PCOMPS_2:8;
consider r being
Real such that A8:
r > 0
and A9:
Ball xP,
r c= AT
by A5, A7, PCOMPS_1:def 5;
reconsider xT =
x as
Element of
T by A7;
A10:
ex
y being
set st
y in AT `
by A6, XBOOLE_0:def 1;
reconsider B =
Ball xP,
r as
Subset of
T by A1, PCOMPS_2:8;
set Inf =
{ p where p is Point of T : (inf pmet,(B ` )) . p = 0 } ;
AT ` c= B `
by A9, SUBSET_1:31;
then consider b being
set such that A11:
b in B `
by A10;
B ` = { p where p is Point of T : (inf pmet,(B ` )) . p = 0 }
proof
thus
B ` c= { p where p is Point of T : (inf pmet,(B ` )) . p = 0 }
XBOOLE_0:def 10 { p where p is Point of T : (inf pmet,(B ` )) . p = 0 } c= B `
let y be
set ;
TARSKI:def 3 ( not y in { p where p is Point of T : (inf pmet,(B ` )) . p = 0 } or y in B ` )
assume
y in { p where p is Point of T : (inf pmet,(B ` )) . p = 0 }
;
y in B `
then consider yT being
Point of
T such that A13:
y = yT
and A14:
(inf pmet,(B ` )) . yT = 0
;
assume
not
y in B `
;
contradiction
then A15:
yT in B
by A13, XBOOLE_0:def 5;
reconsider yP =
yT as
Point of
PM by A1, PCOMPS_2:8;
pmet is_a_pseudometric_of the
carrier of
T
by A1, Th9;
then A16:
( not
(dist pmet,yT) .: (B ` ) is
empty &
(dist pmet,yT) .: (B ` ) is
bounded_below )
by A11, Lm1;
Ball xP,
r in Family_open_set PM
by PCOMPS_1:33;
then consider s being
Real such that A17:
s > 0
and A18:
Ball yP,
s c= Ball xP,
r
by A15, PCOMPS_1:def 5;
inf ((dist pmet,yT) .: (B ` )) = 0
by A14, Def3;
then consider rn being
real number such that A19:
rn in (dist pmet,yT) .: (B ` )
and A20:
rn < 0 + s
by A17, A16, SEQ_4:def 5;
consider z being
set such that A21:
z in dom (dist pmet,yT)
and A22:
z in B `
and A23:
rn = (dist pmet,yT) . z
by A19, FUNCT_1:def 12;
reconsider zT =
z as
Point of
T by A21;
reconsider zP =
z as
Point of
PM by A1, A21, PCOMPS_2:8;
pmet . yT,
zT < s
by A20, A23, Def2;
then
dist yP,
zP < s
by A3;
then
zP in Ball yP,
s
by METRIC_1:12;
then
B ` meets B
by A18, A22, XBOOLE_0:3;
hence
contradiction
by XBOOLE_1:79;
verum
end;
then
B ` = Cl (B ` )
by A2, A11;
then A24:
B is
open
by TOPS_1:30;
reconsider b =
b as
Point of
T by A11;
pmet . xT,
xT = 0
by A1, PCOMPS_1:def 7;
then
dist xP,
xP < r
by A3, A8;
then
xP in B
by METRIC_1:12;
hence
ex
U being
Subset of
T st
(
U is
open &
U c= AT &
x in U )
by A9, A24;
verum
end;
hence
(
x in AT iff ex
U being
Subset of
T st
(
U is
open &
U c= AT &
x in U ) )
;
verum
end; then
AT is
open
by TOPS_1:57;
hence
A in the
topology of
T
by PRE_TOPC:def 5;
verum
end;
the topology of T c= Family_open_set PM
proof
let A be
set ;
TARSKI:def 3 ( not A in the topology of T or A in Family_open_set PM )
assume A25:
A in the
topology of
T
;
A in Family_open_set PM
then reconsider AT =
A as
Subset of
T ;
reconsider AP =
A as
Subset of
PM by A1, A25, PCOMPS_2:8;
per cases
( AT ` is empty or not AT ` is empty )
;
suppose A26:
not
AT ` is
empty
;
A in Family_open_set PM
for
xP being
Element of
PM st
xP in AP holds
ex
r being
Real st
(
r > 0 &
Ball xP,
r c= AP )
proof
let xP be
Element of
PM;
( xP in AP implies ex r being Real st
( r > 0 & Ball xP,r c= AP ) )
assume A27:
xP in AP
;
ex r being Real st
( r > 0 & Ball xP,r c= AP )
reconsider xT =
xP as
Element of
T by A1, PCOMPS_2:8;
take r =
(inf pmet,(AT ` )) . xT;
( r > 0 & Ball xP,r c= AP )
A28:
Ball xP,
r c= AP
proof
pmet is_a_pseudometric_of the
carrier of
T
by A1, Th9;
then A29:
( not
(dist pmet,xT) .: (AT ` ) is
empty &
(dist pmet,xT) .: (AT ` ) is
bounded_below )
by A26, Lm1;
let y be
set ;
TARSKI:def 3 ( not y in Ball xP,r or y in AP )
assume that A30:
y in Ball xP,
r
and A31:
not
y in AP
;
contradiction
reconsider yP =
y as
Point of
PM by A30;
A32:
dist xP,
yP < r
by A30, METRIC_1:12;
reconsider yT =
yP as
Point of
T by A1, PCOMPS_2:8;
A33:
dom (dist pmet,xT) = the
carrier of
T
by FUNCT_2:def 1;
yT in AT `
by A31, XBOOLE_0:def 5;
then
(dist pmet,xT) . yT in (dist pmet,xT) .: (AT ` )
by A33, FUNCT_1:def 12;
then A34:
inf ((dist pmet,xT) .: (AT ` )) <= (dist pmet,xT) . yT
by A29, SEQ_4:def 5;
(
(dist pmet,xT) . yT = pmet . xT,
yT &
inf ((dist pmet,xT) .: (AT ` )) = (inf pmet,(AT ` )) . xT )
by Def2, Def3;
hence
contradiction
by A3, A32, A34;
verum
end;
AT is
open
by A25, PRE_TOPC:def 5;
then
AT ` = Cl (AT ` )
by PRE_TOPC:52;
then A35:
AT ` = { p where p is Point of T : (inf pmet,(AT ` )) . p = 0 }
by A2, A26;
(inf pmet,(AT ` )) . xT > 0
hence
(
r > 0 &
Ball xP,
r c= AP )
by A28;
verum
end; hence
A in Family_open_set PM
by PCOMPS_1:def 5;
verum
end;
then
the topology of T = Family_open_set PM
by A4, XBOOLE_0:def 10;
hence
T is metrizable
by A1, PCOMPS_1:def 9; verum