let M be non empty MetrSpace; :: thesis: for Q, R being non empty Subset of (TopSpaceMetr M)
for y being Point of M st Q is compact & R is compact & y in Q holds
(dist_min R) . y <= max_dist_min (R,Q)
let Q, R be non empty Subset of (TopSpaceMetr M); :: thesis: for y being Point of M st Q is compact & R is compact & y in Q holds
(dist_min R) . y <= max_dist_min (R,Q)
let y be Point of M; :: thesis: ( Q is compact & R is compact & y in Q implies (dist_min R) . y <= max_dist_min (R,Q) )
assume that
A1: ( Q is compact & R is compact ) and
A2: y in Q ; :: thesis: (dist_min R) . y <= max_dist_min (R,Q)
set A = (dist_min R) .: Q;
consider X being non empty Subset of REAL such that
A3: (dist_min R) .: Q = X and
A4: upper_bound ((dist_min R) .: Q) = upper_bound X by Th11;
dom (dist_min R) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
then A5: (dist_min R) . y in X by A2, A3, FUNCT_1:def 6;
( max_dist_min (R,Q) = upper_bound ((dist_min R) .: Q) & X is bounded_above ) by A1, A3, Th25, WEIERSTR:def 8;
hence (dist_min R) . y <= max_dist_min (R,Q) by A4, A5, SEQ_4:def 1; :: thesis: verum