let T be non empty TopSpace; :: thesis: for pmet being Function of [:the carrier of T,the carrier of T:],REAL st pmet is_a_pseudometric_of the carrier of T & ( for p being Point of T holds dist pmet,p is continuous ) holds
for A being non empty Subset of T holds inf pmet,A is continuous
let pmet be Function of [:the carrier of T,the carrier of T:],REAL ; :: thesis: ( pmet is_a_pseudometric_of the carrier of T & ( for p being Point of T holds dist pmet,p is continuous ) implies for A being non empty Subset of T holds inf pmet,A is continuous )
assume that
A1: pmet is_a_pseudometric_of the carrier of T and
A2: for p being Point of T holds dist pmet,p is continuous ; :: thesis: for A being non empty Subset of T holds inf pmet,A is continuous
let A be non empty Subset of T; :: thesis: inf pmet,A is continuous
reconsider infR = inf pmet,A as Function of T,R^1 by TOPMETR:24;

now

let t be Point of T; :: thesis: infR is_continuous_at t
reconsider dR = dist pmet,t as Function of T,R^1 by TOPMETR:24;
for R being Subset of R^1 st R is open & infR . t in R holds
ex U being Subset of T st
( U is open & t in U & infR .: U c= R )

proof

reconsider infRt = infR . t, dRt = dR . t as Point of RealSpace by METRIC_1:def 14;
let R be Subset of R^1 ; :: thesis: ( R is open & infR . t in R implies ex U being Subset of T st
( U is open & t in U & infR .: U c= R ) )
assume ( R is open & infR . t in R ) ; :: thesis: ex U being Subset of T st
( U is open & t in U & infR .: U c= R )
then consider r being real number such that
A3: r > 0 and
A4: Ball infRt,r c= R by TOPMETR:22, TOPMETR:def 7;
reconsider dB = Ball dRt,r as Subset of R^1 by METRIC_1:def 14, TOPMETR:24;
abs ((dR . t) - (dR . t)) = 0 by ABSVALUE:7;
then dist dRt,dRt < r by A3, TOPMETR:15;
then A5: dRt in dB by METRIC_1:12;
dist pmet,t is continuous by A2;
then dR is continuous by TOPREAL6:83;
then ( dB is open & dR is_continuous_at t ) by TMAP_1:55, TOPMETR:21, TOPMETR:def 7;
then consider B being Subset of T such that
A6: ( B is open & t in B ) and
A7: dR .: B c= dB by A5, TMAP_1:48;
infR .: B c= R

proof

let Ib be set ; :: according to TARSKI:def 3 :: thesis: ( not Ib in infR .: B or Ib in R )
assume Ib in infR .: B ; :: thesis: Ib in R
then consider b being set such that
A8: b in dom infR and
A9: b in B and
A10: infR . b = Ib by FUNCT_1:def 12;
reconsider b = b as Point of T by A8;
reconsider infRb = infR . b, dRb = dR . b as Point of RealSpace by METRIC_1:def 14;
pmet . t,b >= 0 by A1, NAGATA_1:29;
then A11: dR . b >= 0 by Def2;
dR . t = pmet . t,t by Def2;
then dR . t = 0 by A1, NAGATA_1:28;
then A12: dist dRt,dRb = abs (0 - (dR . b)) by TOPMETR:15;
dom dR = the carrier of T by FUNCT_2:def 1;
then dR . b in dR .: B by A9, FUNCT_1:def 12;
then dist dRt,dRb < r by A7, METRIC_1:12;
then abs (- (0 - (dR . b))) < r by A12, COMPLEX1:138;
then dR . b < r by A11, ABSVALUE:def 1;
then A13: pmet . t,b < r by Def2;
( abs (((inf pmet,A) . t) - ((inf pmet,A) . b)) <= pmet . t,b & dist infRt,infRb = abs (((inf pmet,A) . t) - ((inf pmet,A) . b)) ) by A1, Th7, TOPMETR:15;
then dist infRt,infRb < r by A13, XXREAL_0:2;
then infRb in Ball infRt,r by METRIC_1:12;
hence Ib in R by A4, A10; :: thesis: verum

end;

hence ex U being Subset of T st
( U is open & t in U & infR .: U c= R ) by A6; :: thesis: verum

end;

hence infR is_continuous_at t by TMAP_1:48; :: thesis: verum

end;

then infR is continuous by TMAP_1:55;
hence inf pmet,A is continuous by TOPREAL6:83; :: thesis: verum