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

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

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

then A4:
Cl infA c= Cl Z
by PRE_TOPC:19;
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;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

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