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 <= HausDist (Q,R)
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 <= HausDist (Q,R)
let y be Point of M; :: thesis: ( Q is compact & R is compact & y in Q implies (dist_min R) . y <= HausDist (Q,R) )
assume ( Q is compact & R is compact & y in Q ) ; :: thesis: (dist_min R) . y <= HausDist (Q,R)
then ( max_dist_min (R,Q) <= max ((max_dist_min (R,Q)),(max_dist_min (Q,R))) & (dist_min R) . y <= max_dist_min (R,Q) ) by Th31, XXREAL_0:25;
hence (dist_min R) . y <= HausDist (Q,R) by XXREAL_0:2; :: thesis: verum