let M be non empty MetrSpace; 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); ( 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
and
A2:
Q is compact
and
A3:
R is compact
; 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:17;
A4:
for w being Real st w in DPR holds
w <= (HausDist (P,Q)) + (HausDist (Q,R))
proof
let w be
Real;
( w in DPR implies w <= (HausDist (P,Q)) + (HausDist (Q,R)) )
assume
w in DPR
;
w <= (HausDist (P,Q)) + (HausDist (Q,R))
then consider y being
object such that
y in dom (dist_min R)
and A5:
y in P
and A6:
w = (dist_min R) . y
by FUNCT_1:def 6;
reconsider y =
y as
Point of
M by A5, TOPMETR:12;
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;
( z in Q implies dist (y,z) >= ((dist_min R) . y) - (HausDist (Q,R)) )
assume
z in Q
;
dist (y,z) >= ((dist_min R) . y) - (HausDist (Q,R))
then
(dist_min R) . z <= HausDist (
Q,
R)
by A2, A3, Th32;
then A7:
(dist (y,z)) + ((dist_min R) . z) <= (dist (y,z)) + (HausDist (Q,R))
by XREAL_1:6;
(dist_min R) . y <= (dist (y,z)) + ((dist_min R) . z)
by Th15;
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:20;
verum
end;
then A8:
((dist_min R) . y) - (HausDist (Q,R)) <= (dist_min Q) . y
by Th14;
(dist_min Q) . y <= HausDist (
P,
Q)
by A1, A2, A5, Th32;
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 A6, XREAL_1:20;
verum
end;
upper_bound DPR =
upper_bound ([#] ((dist_min R) .: P))
by WEIERSTR:def 1
.=
upper_bound ((dist_min R) .: P)
by WEIERSTR:def 2
.=
max_dist_min (R,P)
by WEIERSTR:def 8
;
hence
max_dist_min (R,P) <= (HausDist (P,Q)) + (HausDist (Q,R))
by A4, SEQ_4:45; verum