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 : (lower_bound (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 : (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 } ; :: 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:36;
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 7;
hence pmet . (x,y) = dist (x,y) by METRIC_1:def 1; :: thesis: verum
end;
A4: Family_open_set PM c= the topology of T
proof
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in Family_open_set PM or A in the topology of T )
assume A5: 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:4;
per cases ( AT ` is empty or not AT ` is empty ) ;
suppose A6: 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 A7: x in AT ; :: thesis: 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 } :: according to XBOOLE_0:def 10 :: thesis: { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } c= B `
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in B ` or y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } )
assume A12: y in B ` ; :: thesis: y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 }
(lower_bound (pmet,(B `))) . y = 0 by A1, A12, Th6, Th9;
hence y in { p where p is Point of T : (lower_bound (pmet,(B `))) . p = 0 } by A12; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( 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 } ; :: thesis: 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 ` ; :: thesis: 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; :: thesis: 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; :: 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:25;
hence A in the topology of T by PRE_TOPC:def 2; :: thesis: verum
end;
end;
end;
the topology of T c= Family_open_set PM
proof
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in the topology of T or A in Family_open_set PM )
assume A25: 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, A25, PCOMPS_2:4;
per cases ( AT ` is empty or not AT ` is empty ) ;
suppose A26: 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 A27: 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:4;
take r = (lower_bound (pmet,(AT `))) . xT; :: thesis: ( 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 ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball (xP,r) or y in AP )
assume that
A30: y in Ball (xP,r) and
A31: not y in AP ; :: thesis: 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; :: thesis: 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
proof
assume (lower_bound (pmet,(AT `))) . xT <= 0 ; :: thesis: contradiction
then (lower_bound (pmet,(AT `))) . xT = 0 by A1, A26, Th5, Th9;
then xT in AT ` by A35;
then AT ` meets AT by A27, XBOOLE_0:3;
hence contradiction by XBOOLE_1:79; :: thesis: verum
end;
hence ( r > 0 & Ball (xP,r) c= AP ) by A28; :: thesis: verum
end;
hence A in Family_open_set PM by PCOMPS_1:def 4; :: thesis: 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; :: thesis: verum