let M be non empty MetrSpace; for P, Q being Subset of (TopSpaceMetr M) st P is compact & Q is compact holds
for x1, x2 being Point of M st x1 in P & x2 in Q holds
( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) )
let P, Q be Subset of (TopSpaceMetr M); ( P is compact & Q is compact implies for x1, x2 being Point of M st x1 in P & x2 in Q holds
( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) ) )
assume that
A1:
P is compact
and
A2:
Q is compact
; for x1, x2 being Point of M st x1 in P & x2 in Q holds
( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) )
let x1, x2 be Point of M; ( x1 in P & x2 in Q implies ( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) ) )
assume that
A3:
x1 in P
and
A4:
x2 in Q
; ( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) )
dist_max P is continuous
by A1, A3, Th24;
then
[#] ((dist_max P) .: Q) is real-bounded
by A2, Th8, Th11;
then A5:
[#] ((dist_max P) .: Q) is bounded_above
;
x2 in the carrier of M
;
then
x2 in the carrier of (TopSpaceMetr M)
by TOPMETR:12;
then
(dist_min P) . x2 in the carrier of R^1
by FUNCT_2:5;
then consider z being Real such that
A6:
z = (dist_min P) . x2
;
dist_min P is continuous
by A1, A3, Th27;
then
[#] ((dist_min P) .: Q) is real-bounded
by A2, Th8, Th11;
then A7:
[#] ((dist_min P) .: Q) is bounded_below
;
dom (dist_min P) = the carrier of (TopSpaceMetr M)
by FUNCT_2:def 1;
then
z in [#] ((dist_min P) .: Q)
by A4, A6, FUNCT_1:def 6;
then A8:
lower_bound ((dist_min P) .: Q) <= z
by A7, SEQ_4:def 2;
x2 in the carrier of M
;
then
x2 in the carrier of (TopSpaceMetr M)
by TOPMETR:12;
then
(dist_max P) . x2 in the carrier of R^1
by FUNCT_2:5;
then consider y being Real such that
A9:
y = (dist_max P) . x2
;
dom (dist_max P) = the carrier of (TopSpaceMetr M)
by FUNCT_2:def 1;
then
y in [#] ((dist_max P) .: Q)
by A4, A9, FUNCT_1:def 6;
then A10:
y <= upper_bound ((dist_max P) .: Q)
by A5, SEQ_4:def 1;
A11:
lower_bound ((dist x2) .: P) = z
by A6, Def6;
A12:
upper_bound ((dist x2) .: P) = y
by A9, Def5;
( dist (x1,x2) <= upper_bound ((dist x2) .: P) & lower_bound ((dist x2) .: P) <= dist (x1,x2) )
by A1, A3, Th19;
hence
( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) )
by A12, A10, A11, A8, XXREAL_0:2; verum