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 lower_bound (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 lower_bound (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 lower_bound (pmet,A) is continuous
let A be non empty Subset of T; :: thesis: lower_bound (pmet,A) is continuous
reconsider infR = lower_bound (pmet,A) as Function of T,R^1 by TOPMETR:17;

now :: thesis: for t being Point of T holds infR is_continuous_at t

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:17;
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 13, XREAL_0:def 1;
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 such that
A3: r > 0 and
A4: Ball (infRt,r) c= R by TOPMETR:15, TOPMETR:def 6;
reconsider dB = Ball (dRt,r) as Subset of R^1 by METRIC_1:def 13, TOPMETR:17;
|.((dR . t) - (dR . t)).| = 0 by ABSVALUE:2;
then dist (dRt,dRt) < r by A3, TOPMETR:11;
then A5: dRt in dB by METRIC_1:11;
dist (pmet,t) is continuous by A2;
then dR is continuous by JORDAN5A:27;
then ( dB is open & dR is_continuous_at t ) by TMAP_1:50, TOPMETR:14, TOPMETR:def 6;
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:43;
infR .: B c= R

proof

let Ib be object ; :: 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 object such that
A8: b in dom infR and
A9: b in B and
A10: infR . b = Ib by FUNCT_1:def 6;
reconsider b = b as Point of T by A8;
reconsider infRb = infR . b, dRb = dR . b as Point of RealSpace by METRIC_1:def 13, XREAL_0:def 1;
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) = |.(0 - (dR . b)).| by TOPMETR:11;
dom dR = the carrier of T by FUNCT_2:def 1;
then dR . b in dR .: B by A9, FUNCT_1:def 6;
then dist (dRt,dRb) < r by A7, METRIC_1:11;
then |.(- (0 - (dR . b))).| < r by A12, COMPLEX1:52;
then dR . b < r by A11, ABSVALUE:def 1;
then A13: pmet . (t,b) < r by Def2;
( |.(((lower_bound (pmet,A)) . t) - ((lower_bound (pmet,A)) . b)).| <= pmet . (t,b) & dist (infRt,infRb) = |.(((lower_bound (pmet,A)) . t) - ((lower_bound (pmet,A)) . b)).| ) by A1, Th7, TOPMETR:11;
then dist (infRt,infRb) < r by A13, XXREAL_0:2;
then infRb in Ball (infRt,r) by METRIC_1:11;
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:43; :: thesis: verum

end;

then infR is continuous by TMAP_1:50;
hence lower_bound (pmet,A) is continuous by JORDAN5A:27; :: thesis: verum