let M be non empty MetrSpace; :: thesis: for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
( P misses Q iff min_dist_min (P,Q) > 0 )
let P, Q be Subset of (TopSpaceMetr M); :: thesis: ( P <> {} & P is compact & Q <> {} & Q is compact implies ( P misses Q iff min_dist_min (P,Q) > 0 ) )
assume that
A1: P <> {} and
A2: P is compact and
A3: Q <> {} and
A4: Q is compact ; :: thesis: ( P misses Q iff min_dist_min (P,Q) > 0 )
A5: now :: thesis: ( P /\ Q <> {} implies not min_dist_min (P,Q) > 0 )
set p = the Element of P /\ Q;
assume A6: P /\ Q <> {} ; :: thesis: not min_dist_min (P,Q) > 0
then A7: the Element of P /\ Q in P by XBOOLE_0:def 4;
then reconsider p9 = the Element of P /\ Q as Element of (TopSpaceMetr M) ;
reconsider q = p9 as Point of M by TOPMETR:12;
the distance of M is Reflexive by METRIC_1:def 6;
then the distance of M . (q,q) = 0 by METRIC_1:def 2;
then A8: dist (q,q) = 0 by METRIC_1:def 1;
the Element of P /\ Q in Q by A6, XBOOLE_0:def 4;
hence not min_dist_min (P,Q) > 0 by A2, A4, A7, A8, WEIERSTR:34; :: thesis: verum
end;
consider x1, x2 being Point of M such that
A9: ( x1 in P & x2 in Q ) and
A10: dist (x1,x2) = min_dist_min (P,Q) by A1, A2, A3, A4, WEIERSTR:30;
A11: the distance of M is discerning by METRIC_1:def 7;
now :: thesis: ( not min_dist_min (P,Q) > 0 implies P /\ Q <> {} )
assume not min_dist_min (P,Q) > 0 ; :: thesis: P /\ Q <> {}
then dist (x1,x2) = 0 by A1, A2, A3, A4, A10, Th36;
then the distance of M . (x1,x2) = 0 by METRIC_1:def 1;
then x1 = x2 by A11, METRIC_1:def 3;
hence P /\ Q <> {} by A9, XBOOLE_0:def 4; :: thesis: verum
end;
hence ( P misses Q iff min_dist_min (P,Q) > 0 ) by A5; :: thesis: verum