let X be non empty set ; :: thesis: for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds
( f is bounded_below & ( for A being non empty Subset of X
for x being Element of X holds
( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) )
let f be Function of [:X,X:],REAL; :: thesis: ( f is_a_pseudometric_of X implies ( f is bounded_below & ( for A being non empty Subset of X
for x being Element of X holds
( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) ) )
assume A1: f is_a_pseudometric_of X ; :: thesis: ( f is bounded_below & ( for A being non empty Subset of X
for x being Element of X holds
( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) )
A2: now :: thesis: for A being non empty Subset of X
for x being Element of X holds
( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below )
let A be non empty Subset of X; :: thesis: for x being Element of X holds
( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below )
let x be Element of X; :: thesis: ( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below )
A3: 0 is LowerBound of (dist (f,x)) .: A
proof
let rn be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not rn in (dist (f,x)) .: A or 0 <= rn )
assume rn in (dist (f,x)) .: A ; :: thesis: 0 <= rn
then consider y being object such that
A4: y in dom (dist (f,x)) and
y in A and
A5: rn = (dist (f,x)) . y by FUNCT_1:def 6;
reconsider y = y as Element of X by A4;
f . (x,y) >= 0 by A1, NAGATA_1:29;
hence rn >= 0 by A5, Def2; :: thesis: verum
end;
dom (dist (f,x)) = X by FUNCT_2:def 1;
hence ( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) by A3; :: thesis: verum
end;
now :: thesis: for xy being object st xy in dom f holds
f . xy > - 1
let xy be object ; :: thesis: ( xy in dom f implies f . xy > - 1 )
assume xy in dom f ; :: thesis: f . xy > - 1
then consider x, y being object such that
A6: ( x in X & y in X ) and
A7: [x,y] = xy by ZFMISC_1:def 2;
reconsider x = x, y = y as Element of X by A6;
( f . (x,y) >= 0 & 0 > - 1 ) by A1, NAGATA_1:29;
hence f . xy > - 1 by A7; :: thesis: verum
end;
hence ( f is bounded_below & ( for A being non empty Subset of X
for x being Element of X holds
( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) ) by A2, SEQ_2:def 2; :: thesis: verum