let M be non empty MetrSpace; for P being non empty Subset of (TopSpaceMetr M)
for x, y being Point of M holds (dist_min P) . x <= (dist (x,y)) + ((dist_min P) . y)
let P be non empty Subset of (TopSpaceMetr M); for x, y being Point of M holds (dist_min P) . x <= (dist (x,y)) + ((dist_min P) . y)
let x, y be Point of M; (dist_min P) . x <= (dist (x,y)) + ((dist_min P) . y)
now for z being Point of M st z in P holds
dist (y,z) >= ((dist_min P) . x) - (dist (x,y))let z be
Point of
M;
( z in P implies dist (y,z) >= ((dist_min P) . x) - (dist (x,y)) )assume
z in P
;
dist (y,z) >= ((dist_min P) . x) - (dist (x,y))then
(dist_min P) . x <= dist (
x,
z)
by Th13;
then A1:
(dist (x,z)) - (dist (x,y)) >= ((dist_min P) . x) - (dist (x,y))
by XREAL_1:13;
dist (
x,
z)
<= (dist (x,y)) + (dist (y,z))
by METRIC_1:4;
then
dist (
y,
z)
>= (dist (x,z)) - (dist (x,y))
by XREAL_1:20;
hence
dist (
y,
z)
>= ((dist_min P) . x) - (dist (x,y))
by A1, XXREAL_0:2;
verum end;
then
(dist_min P) . y >= ((dist_min P) . x) - (dist (x,y))
by Th14;
hence
(dist_min P) . x <= (dist (x,y)) + ((dist_min P) . y)
by XREAL_1:20; verum