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 : (lower_bound (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 : (lower_bound (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 : (lower_bound (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:36;
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
object ;
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:4;
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:4;
consider r being
Real such that A8:
r > 0
and A9:
Ball (
xP,
r)
c= AT
by A5, A7, PCOMPS_1:def 4;
reconsider xT =
x as
Element of
T by A7;
A10:
ex
y being
object st
y in AT `
by A6;
reconsider B =
Ball (
xP,
r) as
Subset of
T by A1, PCOMPS_2:4;
set Inf =
{ p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } ;
AT ` c= B `
by A9, SUBSET_1:12;
then consider b being
set such that A11:
b in B `
by A10;
B ` = { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 }
proof
thus
B ` c= { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 }
XBOOLE_0:def 10 { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } c= B `
let y be
object ;
TARSKI:def 3 ( not y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } or y in B ` )
assume
y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 }
;
y in B `
then consider yT being
Point of
T such that A13:
y = yT
and A14:
(lower_bound (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:4;
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:29;
then consider s being
Real such that A17:
s > 0
and A18:
Ball (
yP,
s)
c= Ball (
xP,
r)
by A15, PCOMPS_1:def 4;
lower_bound ((dist (pmet,yT)) .: (B `)) = 0
by A14, Def3;
then consider rn being
Real such that A19:
rn in (dist (pmet,yT)) .: (B `)
and A20:
rn < 0 + s
by A17, A16, SEQ_4:def 2;
consider z being
object 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 6;
reconsider zT =
z as
Point of
T by A21;
reconsider zP =
z as
Point of
PM by A1, A21, PCOMPS_2:4;
pmet . (
yT,
zT)
< s
by A20, A23, Def2;
then
dist (
yP,
zP)
< s
by A3;
then
zP in Ball (
yP,
s)
by METRIC_1:11;
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:4;
pmet . (
xT,
xT)
= 0
by A1, PCOMPS_1:def 6;
then
dist (
xP,
xP)
< r
by A3, A8;
then
xP in B
by METRIC_1:11;
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:25;
hence
A in the
topology of
T
by PRE_TOPC:def 2;
verum end; end;
end;
the topology of T c= Family_open_set PM
proof
let A be
object ;
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:4;
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:4;
take r =
(lower_bound (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
object ;
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:11;
reconsider yT =
yP as
Point of
T by A1, PCOMPS_2:4;
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 6;
then A34:
lower_bound ((dist (pmet,xT)) .: (AT `)) <= (dist (pmet,xT)) . yT
by A29, SEQ_4:def 2;
(
(dist (pmet,xT)) . yT = pmet . (
xT,
yT) &
lower_bound ((dist (pmet,xT)) .: (AT `)) = (lower_bound (pmet,(AT `))) . xT )
by Def2, Def3;
hence
contradiction
by A3, A32, A34;
verum
end;
AT is
open
by A25, PRE_TOPC:def 2;
then
AT ` = Cl (AT `)
by PRE_TOPC:22;
then A35:
AT ` = { p where p is Point of T : (lower_bound (pmet,(AT `))) . p = 0 }
by A2, A26;
(lower_bound (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 4;
verum end; end;
end;
then
the topology of T = Family_open_set PM
by A4;
hence
T is metrizable
by A1, PCOMPS_1:def 8; verum