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 pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) holds
for A being non empty Subset of T
for p being Point of T st p in Cl A holds
(lower_bound (pmet,A)) . p = 0
set rn = In (0,REAL);
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 pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) implies for A being non empty Subset of T
for p being Point of T st p in Cl A holds
(lower_bound (pmet,A)) . p = 0 )
assume that
A1: pmet is_a_pseudometric_of the carrier of T and
A2: for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ; :: thesis: for A being non empty Subset of T
for p being Point of T st p in Cl A holds
(lower_bound (pmet,A)) . p = 0
let A be non empty Subset of T; :: thesis: for p being Point of T st p in Cl A holds
(lower_bound (pmet,A)) . p = 0
let p be Point of T; :: thesis: ( p in Cl A implies (lower_bound (pmet,A)) . p = 0 )
A3: dom (lower_bound (pmet,A)) = the carrier of T by FUNCT_2:def 1;
reconsider Z = {(In (0,REAL))}, infA = (lower_bound (pmet,A)) .: A as Subset of R^1 by TOPMETR:17;
infA c= Z
proof
let infa be object ; :: according to TARSKI:def 3 :: thesis: ( not infa in infA or infa in Z )
assume infa in infA ; :: thesis: infa in Z
then ex a being object st
( a in dom (lower_bound (pmet,A)) & a in A & infa = (lower_bound (pmet,A)) . a ) by FUNCT_1:def 6;
then infa = 0 by A1, Th6;
hence infa in Z by TARSKI:def 1; :: thesis: verum
end;
then A4: Cl infA c= Cl Z by PRE_TOPC:19;
reconsider InfA = lower_bound (pmet,A) as Function of T,R^1 by TOPMETR:17;
for p being Point of T holds dist (pmet,p) is continuous by A2, Th4;
then lower_bound (pmet,A) is continuous by A1, Th8;
then InfA is continuous by JORDAN5A:27;
then A5: InfA .: (Cl A) c= Cl (InfA .: A) by TOPS_2:45;
assume p in Cl A ; :: thesis: (lower_bound (pmet,A)) . p = 0
then A6: (lower_bound (pmet,A)) . p in (lower_bound (pmet,A)) .: (Cl A) by A3, FUNCT_1:def 6;
Z is closed by PCOMPS_1:7, TOPMETR:17;
then Z = Cl Z by PRE_TOPC:22;
then InfA .: (Cl A) c= Z by A4, A5;
hence (lower_bound (pmet,A)) . p = 0 by A6, TARSKI:def 1; :: thesis: verum