let T be non empty TopSpace; :: thesis: 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 ; :: thesis: ( 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 } ; :: thesis: 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
proof
let x, y be Element of PM; :: thesis: pmet . x,y = dist x,y
PM = MetrStruct(# the carrier of T,pmet #) by A1, PCOMPS_1:def 8;
hence pmet . x,y = dist x,y by METRIC_1:def 1; :: thesis: verum
end;
A4: the topology of T c= Family_open_set PM
proof
let A be set ; :: according to TARSKI:def 3 :: thesis: ( not A in the topology of T or A in Family_open_set PM )
assume A5: A in the topology of T ; :: thesis: A in Family_open_set PM
then reconsider AT = A as Subset of T ;
reconsider AP = A as Subset of PM by A1, A5, PCOMPS_2:8;
per cases ( AT ` is empty or not AT ` is empty ) ;
suppose A6: not AT ` is empty ; :: thesis: 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; :: thesis: ( xP in AP implies ex r being Real st
( r > 0 & Ball xP,r c= AP ) )
assume A7: xP in AP ; :: thesis: ex r being Real st
( r > 0 & Ball xP,r c= AP )
reconsider xT = xP as Element of T by A1, PCOMPS_2:8;
AT is open by A5, PRE_TOPC:def 5;
then AT ` is closed ;
then AT ` = Cl (AT ` ) by PRE_TOPC:52;
then A8: AT ` = { p where p is Point of T : (inf pmet,(AT ` )) . p = 0 } by A2, A6;
A9: (inf pmet,(AT ` )) . xT > 0
proof
assume (inf pmet,(AT ` )) . xT <= 0 ; :: thesis: contradiction
then (inf pmet,(AT ` )) . xT = 0 by A1, A6, Th5, Th9;
then ( xT in AT ` & xT in AT ) by A7, A8;
then AT ` meets AT by XBOOLE_0:3;
hence contradiction by XBOOLE_1:79; :: thesis: verum
end;
take r = (inf pmet,(AT ` )) . xT; :: thesis: ( r > 0 & Ball xP,r c= AP )
Ball xP,r c= AP
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball xP,r or y in AP )
assume A10: ( y in Ball xP,r & not y in AP ) ; :: thesis: contradiction
then reconsider yP = y as Point of PM ;
reconsider yT = yP as Point of T by A1, PCOMPS_2:8;
A11: dist xP,yP < r by A10, METRIC_1:12;
( yT in AT ` & dom (dist pmet,xT) = the carrier of T ) by A10, FUNCT_2:def 1, XBOOLE_0:def 5;
then ( (dist pmet,xT) . yT in (dist pmet,xT) .: (AT ` ) & pmet is_a_pseudometric_of the carrier of T ) by A1, Th9, FUNCT_1:def 12;
then ( (dist pmet,xT) . yT in (dist pmet,xT) .: (AT ` ) & not (dist pmet,xT) .: (AT ` ) is empty & (dist pmet,xT) .: (AT ` ) is bounded_below & pmet is bounded_below ) by A6, Lm1;
then ( inf ((dist pmet,xT) .: (AT ` )) <= (dist pmet,xT) . yT & (dist pmet,xT) . yT = pmet . xT,yT & inf ((dist pmet,xT) .: (AT ` )) = (inf pmet,(AT ` )) . xT ) by Def2, Def3, SEQ_4:def 5;
hence contradiction by A3, A11; :: thesis: verum
end;
hence ( r > 0 & Ball xP,r c= AP ) by A9; :: thesis: verum
end;
hence A in Family_open_set PM by PCOMPS_1:def 5; :: thesis: verum
end;
end;
end;
Family_open_set PM c= the topology of T
proof
let A be set ; :: according to TARSKI:def 3 :: thesis: ( not A in Family_open_set PM or A in the topology of T )
assume A12: A in Family_open_set PM ; :: thesis: 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 A13: not AT ` is empty ; :: thesis: 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 ; :: thesis: ( 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 A14: x in AT ; :: thesis: ex U being Subset of T st
( U is open & U c= AT & x in U )
then reconsider xT = x as Element of T ;
reconsider xP = x as Element of PM by A1, A14, PCOMPS_2:8;
consider r being Real such that
A15: ( r > 0 & Ball xP,r c= AT ) by A12, A14, PCOMPS_1:def 5;
pmet . xT,xT = 0 by A1, PCOMPS_1:def 7;
then A16: dist xP,xP < r by A3, A15;
reconsider B = Ball xP,r as Subset of T by A1, PCOMPS_2:8;
( AT ` c= B ` & ex y being set st y in AT ` ) by A13, A15, SUBSET_1:31, XBOOLE_0:def 1;
then consider b being set such that
A17: b in B ` ;
reconsider b = b as Point of T by A17;
set Inf = { p where p is Point of T : (inf pmet,(B ` )) . p = 0 } ;
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 } :: according to XBOOLE_0:def 10 :: thesis: { p where p is Point of T : (inf pmet,(B ` )) . p = 0 } c= B `
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in B ` or y in { p where p is Point of T : (inf pmet,(B ` )) . p = 0 } )
assume A18: y in B ` ; :: thesis: y in { p where p is Point of T : (inf pmet,(B ` )) . p = 0 }
(inf pmet,(B ` )) . y = 0 by A1, A18, Th6, Th9;
hence y in { p where p is Point of T : (inf pmet,(B ` )) . p = 0 } by A18; :: thesis: verum
end;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( 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 } ; :: thesis: y in B `
then consider yT being Point of T such that
A19: ( y = yT & (inf pmet,(B ` )) . yT = 0 ) ;
reconsider yP = yT as Point of PM by A1, PCOMPS_2:8;
assume not y in B ` ; :: thesis: contradiction
then A20: yT in B by A19, XBOOLE_0:def 5;
Ball xP,r in Family_open_set PM by PCOMPS_1:33;
then consider s being Real such that
A21: ( s > 0 & Ball yP,s c= Ball xP,r ) by A20, PCOMPS_1:def 5;
( b in B ` & dom (dist pmet,yT) = the carrier of T ) by A17, FUNCT_2:def 1;
then ( (dist pmet,yT) . b in (dist pmet,yT) .: (B ` ) & pmet is_a_pseudometric_of the carrier of T ) by A1, Th9, FUNCT_1:def 12;
then A22: ( not (dist pmet,yT) .: (B ` ) is empty & (dist pmet,yT) .: (B ` ) is bounded_below & pmet is bounded_below ) by A17, Lm1;
inf ((dist pmet,yT) .: (B ` )) = 0 by A19, Def3;
then consider rn being real number such that
A23: ( rn in (dist pmet,yT) .: (B ` ) & rn < 0 + s ) by A21, A22, SEQ_4:def 5;
consider z being set such that
A24: ( z in dom (dist pmet,yT) & z in B ` & rn = (dist pmet,yT) . z ) by A23, FUNCT_1:def 12;
reconsider zT = z as Point of T by A24;
reconsider zP = z as Point of PM by A1, A24, PCOMPS_2:8;
pmet . yT,zT < s by A23, A24, Def2;
then dist yP,zP < s by A3;
then zP in Ball yP,s by METRIC_1:12;
then B ` meets B by A21, A24, XBOOLE_0:3;
hence contradiction by XBOOLE_1:79; :: thesis: verum
end;
then B ` = Cl (B ` ) by A2, A17;
then ( B is open & xP in B ) by A16, METRIC_1:12, TOPS_1:30;
hence ex U being Subset of T st
( U is open & U c= AT & x in U ) by A15; :: thesis: verum
end;
hence ( x in AT iff ex U being Subset of T st
( U is open & U c= AT & x in U ) ) ; :: thesis: verum
end;
then AT is open by TOPS_1:57;
hence A in the topology of T by PRE_TOPC:def 5; :: thesis: verum
end;
end;
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; :: thesis: verum