let M be non empty MetrSpace; :: thesis: for P, Q, R being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact & R is compact holds
max_dist_min P,R <= (HausDist P,Q) + (HausDist Q,R)
let P, Q, R be non empty Subset of (TopSpaceMetr M); :: thesis: ( P is compact & Q is compact & R is compact implies max_dist_min P,R <= (HausDist P,Q) + (HausDist Q,R) )
assume that
A1:
( P is compact & Q is compact )
and
A2:
R is compact
; :: thesis: max_dist_min P,R <= (HausDist P,Q) + (HausDist Q,R)
reconsider DPR = (dist_min P) .: R as non empty Subset of REAL by TOPMETR:24;
A3: sup DPR =
upper_bound ([#] ((dist_min P) .: R))
by WEIERSTR:def 3
.=
upper_bound ((dist_min P) .: R)
by WEIERSTR:def 4
.=
max_dist_min P,R
by WEIERSTR:def 10
;
for w being real number st w in DPR holds
w <= (HausDist P,Q) + (HausDist Q,R)
proof
let w be
real number ;
:: thesis: ( w in DPR implies w <= (HausDist P,Q) + (HausDist Q,R) )
assume
w in DPR
;
:: thesis: w <= (HausDist P,Q) + (HausDist Q,R)
then consider y being
set such that
y in dom (dist_min P)
and A4:
y in R
and A5:
w = (dist_min P) . y
by FUNCT_1:def 12;
reconsider y =
y as
Point of
M by A4, TOPMETR:16;
for
z being
Point of
M st
z in Q holds
dist y,
z >= ((dist_min P) . y) - (HausDist Q,P)
proof
let z be
Point of
M;
:: thesis: ( z in Q implies dist y,z >= ((dist_min P) . y) - (HausDist Q,P) )
assume A6:
z in Q
;
:: thesis: dist y,z >= ((dist_min P) . y) - (HausDist Q,P)
A7:
(dist_min P) . y <= (dist y,z) + ((dist_min P) . z)
by Th17;
(dist_min P) . z <= HausDist Q,
P
by A1, A6, Th34;
then
(dist y,z) + ((dist_min P) . z) <= (dist y,z) + (HausDist Q,P)
by XREAL_1:8;
then
(dist_min P) . y <= (dist y,z) + (HausDist Q,P)
by A7, XXREAL_0:2;
hence
dist y,
z >= ((dist_min P) . y) - (HausDist Q,P)
by XREAL_1:22;
:: thesis: verum
end;
then
((dist_min P) . y) - (HausDist Q,P) <= (dist_min Q) . y
by Th16;
then A8:
(dist_min P) . y <= (HausDist Q,P) + ((dist_min Q) . y)
by XREAL_1:22;
(dist_min Q) . y <= HausDist R,
Q
by A1, A2, A4, Th34;
then
(HausDist Q,P) + ((dist_min Q) . y) <= (HausDist Q,P) + (HausDist Q,R)
by XREAL_1:8;
hence
w <= (HausDist P,Q) + (HausDist Q,R)
by A5, A8, XXREAL_0:2;
:: thesis: verum
end;
hence
max_dist_min P,R <= (HausDist P,Q) + (HausDist Q,R)
by A3, SEQ_4:62; :: thesis: verum