let X be set ; for f being Function of [:X,X:],REAL holds
( f is_a_pseudometric_of X iff for a, b, c being Element of X holds
( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) )
let f be Function of [:X,X:],REAL; ( f is_a_pseudometric_of X iff for a, b, c being Element of X holds
( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) )
thus
( f is_a_pseudometric_of X implies for a, b, c being Element of X holds
( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) )
( ( for a, b, c being Element of X holds
( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ) implies f is_a_pseudometric_of X )proof
assume A1:
f is_a_pseudometric_of X
;
for a, b, c being Element of X holds
( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) )
let a,
b,
c be
Element of
X;
( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) )
f . (
a,
c)
<= (f . (a,b)) + (f . (b,c))
by A1, Lm8;
hence
(
f . (
a,
a)
= 0 &
f . (
a,
c)
<= (f . (a,b)) + (f . (c,b)) )
by A1, Lm8;
verum
end;
thus
( ( for a, b, c being Element of X holds
( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) ) implies f is_a_pseudometric_of X )
verumproof
assume A2:
for
a,
b,
c being
Element of
X holds
(
f . (
a,
a)
= 0 &
f . (
a,
c)
<= (f . (a,b)) + (f . (c,b)) )
;
f is_a_pseudometric_of X
A3:
for
a,
b being
Element of
X holds
f . (
a,
b)
= f . (
b,
a)
proof
let a,
b be
Element of
X;
f . (a,b) = f . (b,a)
A4:
(
f . (
b,
a)
<= (f . (b,b)) + (f . (a,b)) &
f . (
b,
b)
= 0 )
by A2;
(
f . (
a,
b)
<= (f . (a,a)) + (f . (b,a)) &
f . (
a,
a)
= 0 )
by A2;
hence
f . (
a,
b)
= f . (
b,
a)
by A4, XXREAL_0:1;
verum
end;
for
a,
b,
c being
Element of
X holds
f . (
a,
c)
<= (f . (a,b)) + (f . (b,c))
proof
let x,
y,
z be
Element of
X;
f . (x,z) <= (f . (x,y)) + (f . (y,z))
f . (
x,
z)
<= (f . (x,y)) + (f . (z,y))
by A2;
hence
f . (
x,
z)
<= (f . (x,y)) + (f . (y,z))
by A3;
verum
end;
then
(
f is
Reflexive &
f is
symmetric &
f is
triangle )
by A2, A3, METRIC_1:def 2, METRIC_1:def 4, METRIC_1:def 5;
hence
f is_a_pseudometric_of X
;
verum
end;