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 R,P <= (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 R,P <= (HausDist P,Q) + (HausDist Q,R) )
assume that
A1:
( P is compact & Q is compact )
and
A2:
R is compact
; :: thesis: max_dist_min R,P <= (HausDist P,Q) + (HausDist Q,R)
reconsider DPR = (dist_min R) .: P as non empty Subset of REAL by TOPMETR:24;
A3: sup DPR =
upper_bound ([#] ((dist_min R) .: P))
by WEIERSTR:def 3
.=
upper_bound ((dist_min R) .: P)
by WEIERSTR:def 4
.=
max_dist_min R,P
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 R)
and A4:
y in P
and A5:
w = (dist_min R) . 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 R) . y) - (HausDist Q,R)
proof
let z be
Point of
M;
:: thesis: ( z in Q implies dist y,z >= ((dist_min R) . y) - (HausDist Q,R) )
assume A6:
z in Q
;
:: thesis: dist y,z >= ((dist_min R) . y) - (HausDist Q,R)
A7:
(dist_min R) . y <= (dist y,z) + ((dist_min R) . z)
by Th17;
(dist_min R) . z <= HausDist Q,
R
by A1, A2, A6, Th34;
then
(dist y,z) + ((dist_min R) . z) <= (dist y,z) + (HausDist Q,R)
by XREAL_1:8;
then
(dist_min R) . y <= (dist y,z) + (HausDist Q,R)
by A7, XXREAL_0:2;
hence
dist y,
z >= ((dist_min R) . y) - (HausDist Q,R)
by XREAL_1:22;
:: thesis: verum
end;
then A8:
((dist_min R) . y) - (HausDist Q,R) <= (dist_min Q) . y
by Th16;
(dist_min Q) . y <= HausDist P,
Q
by A1, A4, Th34;
then
((dist_min R) . y) - (HausDist Q,R) <= HausDist P,
Q
by A8, XXREAL_0:2;
hence
w <= (HausDist P,Q) + (HausDist Q,R)
by A5, XREAL_1:22;
:: thesis: verum
end;
hence
max_dist_min R,P <= (HausDist P,Q) + (HausDist Q,R)
by A3, SEQ_4:62; :: thesis: verum