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;

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

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

then
infR is continuous
by TMAP_1:50;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 )

end;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

hence
infR is_continuous_at t
by TMAP_1:43; :: thesis: verum
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

( U is open & t in U & infR .: U c= R ) by A6; :: thesis: verum

end;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

hence
ex U being Subset of T st
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;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

( U is open & t in U & infR .: U c= R ) by A6; :: thesis: verum

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