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

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 A3: ( 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 )
reconsider infRt = infR . t, dRt = dR . t as Point of RealSpace by METRIC_1:def 14;
consider r being real number such that
A4: ( r > 0 & Ball infRt,r c= R ) by A3, 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 & dist pmet,t is continuous ) by A2, ABSVALUE:7;
then ( dist dRt,dRt < r & dR is continuous ) by A4, TOPMETR:15, TOPREAL6:83;
then ( dRt in dB & dB is open & dR is_continuous_at t ) by METRIC_1:12, TMAP_1:55, TOPMETR:21, TOPMETR:def 7;
then consider B being Subset of T such that
A5: ( B is open & t in B & dR .: B c= dB ) by 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
A6: ( b in dom infR & b in B & infR . b = Ib ) by FUNCT_1:def 12;
reconsider b = b as Point of T by A6;
reconsider infRb = infR . b, dRb = dR . b as Point of RealSpace by METRIC_1:def 14;
dom dR = the carrier of T by FUNCT_2:def 1;
then ( dR . b in dR .: B & dR . t = pmet . t,t ) by A6, Def2, FUNCT_1:def 12;
then ( dR . b in dB & dR . t = 0 ) by A1, A5, NAGATA_1:28;
then ( dist dRt,dRb < r & dist dRt,dRb = abs (0 - (dR . b)) & pmet . t,b >= 0 ) by A1, METRIC_1:12, NAGATA_1:29, TOPMETR:15;
then ( abs (- (0 - (dR . b))) < r & dR . b >= 0 ) by Def2, COMPLEX1:138;
then dR . b < r by ABSVALUE:def 1;
then ( abs (((inf pmet,A) . t) - ((inf pmet,A) . b)) <= pmet . t,b & dist infRt,infRb = abs (((inf pmet,A) . t) - ((inf pmet,A) . b)) & pmet . t,b < r ) by A1, Def2, Th7, TOPMETR:15;
then dist infRt,infRb < r by XXREAL_0:2;
then infRb in Ball infRt,r by METRIC_1:12;
hence Ib in R by A4, A6; :: thesis: verum

end;

hence ex U being Subset of T st
( U is open & t in U & infR .: U c= R ) by A5; :: 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