let T be non empty TopSpace; for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_a_pseudometric_of the carrier of T holds
for x, y being Point of T
for A being non empty Subset of T holds |.(((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)).| <= pmet . (x,y)
let pmet be Function of [: the carrier of T, the carrier of T:],REAL; ( pmet is_a_pseudometric_of the carrier of T implies for x, y being Point of T
for A being non empty Subset of T holds |.(((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)).| <= pmet . (x,y) )
assume A1:
pmet is_a_pseudometric_of the carrier of T
; for x, y being Point of T
for A being non empty Subset of T holds |.(((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)).| <= pmet . (x,y)
A2:
pmet is symmetric
by A1, NAGATA_1:def 10;
let x, y be Point of T; for A being non empty Subset of T holds |.(((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)).| <= pmet . (x,y)
let A be non empty Subset of T; |.(((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)).| <= pmet . (x,y)
A3:
for x1, y1 being Point of T holds ((lower_bound (pmet,A)) . y1) - ((lower_bound (pmet,A)) . x1) >= - (pmet . (x1,y1))
proof
let x1,
y1 be
Point of
T;
((lower_bound (pmet,A)) . y1) - ((lower_bound (pmet,A)) . x1) >= - (pmet . (x1,y1))
A4:
( not
(dist (pmet,x1)) .: A is
empty &
(dist (pmet,x1)) .: A is
bounded_below )
by A1, Lm1;
A5:
for
rn being
Real st
rn in (dist (pmet,y1)) .: A holds
rn >= (lower_bound ((dist (pmet,x1)) .: A)) - (pmet . (x1,y1))
proof
let rn be
Real;
( rn in (dist (pmet,y1)) .: A implies rn >= (lower_bound ((dist (pmet,x1)) .: A)) - (pmet . (x1,y1)) )
assume
rn in (dist (pmet,y1)) .: A
;
rn >= (lower_bound ((dist (pmet,x1)) .: A)) - (pmet . (x1,y1))
then consider z being
object such that A6:
z in dom (dist (pmet,y1))
and A7:
z in A
and A8:
(dist (pmet,y1)) . z = rn
by FUNCT_1:def 6;
reconsider z =
z as
Point of
T by A6;
A9:
(dist (pmet,x1)) . z = pmet . (
x1,
z)
by Def2;
pmet is
triangle
by A1, NAGATA_1:def 10;
then A10:
(pmet . (x1,y1)) + (pmet . (y1,z)) >= pmet . (
x1,
z)
by METRIC_1:def 5;
dom (dist (pmet,x1)) = the
carrier of
T
by FUNCT_2:def 1;
then
(dist (pmet,x1)) . z in (dist (pmet,x1)) .: A
by A7, FUNCT_1:def 6;
then
pmet . (
x1,
z)
>= lower_bound ((dist (pmet,x1)) .: A)
by A4, A9, SEQ_4:def 2;
then
(pmet . (x1,y1)) + (pmet . (y1,z)) >= (lower_bound ((dist (pmet,x1)) .: A)) + 0
by A10, XXREAL_0:2;
then
(pmet . (y1,z)) - 0 >= (lower_bound ((dist (pmet,x1)) .: A)) - (pmet . (x1,y1))
by XREAL_1:21;
hence
rn >= (lower_bound ((dist (pmet,x1)) .: A)) - (pmet . (x1,y1))
by A8, Def2;
verum
end;
( not
(dist (pmet,y1)) .: A is
empty &
(dist (pmet,y1)) .: A is
bounded_below )
by A1, Lm1;
then
(lower_bound ((dist (pmet,y1)) .: A)) - 0 >= (lower_bound ((dist (pmet,x1)) .: A)) - (pmet . (x1,y1))
by A5, SEQ_4:43;
then A11:
(lower_bound ((dist (pmet,y1)) .: A)) - (lower_bound ((dist (pmet,x1)) .: A)) >= 0 - (pmet . (x1,y1))
by XREAL_1:17;
lower_bound ((dist (pmet,y1)) .: A) = (lower_bound (pmet,A)) . y1
by Def3;
hence
((lower_bound (pmet,A)) . y1) - ((lower_bound (pmet,A)) . x1) >= - (pmet . (x1,y1))
by A11, Def3;
verum
end;
then
((lower_bound (pmet,A)) . y) - ((lower_bound (pmet,A)) . x) >= - (pmet . (x,y))
;
then
- (((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)) >= - (pmet . (x,y))
;
then A12:
((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y) <= pmet . (x,y)
by XREAL_1:24;
((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y) >= - (pmet . (y,x))
by A3;
then
((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y) >= - (pmet . (x,y))
by A2, METRIC_1:def 4;
hence
|.(((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)).| <= pmet . (x,y)
by A12, ABSVALUE:5; verum