let M be non empty MetrSpace; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( min_dist_min P,Q <= dist x1,x2 & dist x1,x2 <= max_dist_max P,Q )
dist_max P is continuous by A1, A3, Th30;
then [#] ((dist_max P) .: Q) is bounded by A2, Th14, Th17;
then A5: [#] ((dist_max P) .: Q) is bounded_above by XXREAL_2:def 11;
x2 in the carrier of M ;
then x2 in the carrier of (TopSpaceMetr M) by TOPMETR:16;
then (dist_min P) . x2 in the carrier of R^1 by FUNCT_2:7;
then consider z being Real such that
A6: z = (dist_min P) . x2 by TOPMETR:24;
dist_min P is continuous by A1, A3, Th33;
then [#] ((dist_min P) .: Q) is bounded by A2, Th14, Th17;
then A7: [#] ((dist_min P) .: Q) is bounded_below by XXREAL_2:def 11;
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 12;
then A8: lower_bound ((dist_min P) .: Q) <= z by A7, SEQ_4:def 5;
x2 in the carrier of M ;
then x2 in the carrier of (TopSpaceMetr M) by TOPMETR:16;
then (dist_max P) . x2 in the carrier of R^1 by FUNCT_2:7;
then consider y being Real such that
A9: y = (dist_max P) . x2 by TOPMETR:24;
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 12;
then A10: y <= upper_bound ((dist_max P) .: Q) by A5, SEQ_4:def 4;
A11: lower_bound ((dist x2) .: P) = z by A6, Def8;
A12: upper_bound ((dist x2) .: P) = y by A9, Def7;
( dist x1,x2 <= upper_bound ((dist x2) .: P) & lower_bound ((dist x2) .: P) <= dist x1,x2 ) by A1, A3, Th25;
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; :: thesis: verum