let r be Real; :: thesis: for M being non empty MetrSpace
for A, B being non empty Subset of (TopSpaceMetr M) st ( for p, q being Point of M st p in A & q in B holds
dist (p,q) >= r ) holds
min_dist_min (A,B) >= r
let M be non empty MetrSpace; :: thesis: for A, B being non empty Subset of (TopSpaceMetr M) st ( for p, q being Point of M st p in A & q in B holds
dist (p,q) >= r ) holds
min_dist_min (A,B) >= r
let A, B be non empty Subset of (TopSpaceMetr M); :: thesis: ( ( for p, q being Point of M st p in A & q in B holds
dist (p,q) >= r ) implies min_dist_min (A,B) >= r )
assume A1: for p, q being Point of M st p in A & q in B holds
dist (p,q) >= r ; :: thesis: min_dist_min (A,B) >= r
set X = [#] ((dist_min A) .: B);
A2: [#] ((dist_min A) .: B) = (dist_min A) .: B by WEIERSTR:def 1;
A3: for s being Real st s in [#] ((dist_min A) .: B) holds
r <= s
proof
let s be Real; :: thesis: ( s in [#] ((dist_min A) .: B) implies r <= s )
assume s in [#] ((dist_min A) .: B) ; :: thesis: r <= s
then consider y being object such that
y in dom (dist_min A) and
A4: y in B and
A5: s = (dist_min A) . y by A2, FUNCT_1:def 6;
reconsider y = y as Point of (TopSpaceMetr M) by A4;
reconsider p = y as Point of M by TOPMETR:12;
for q being Point of M st q in A holds
dist (p,q) >= r by A1, A4;
hence r <= s by A5, Th10; :: thesis: verum
end;
dom (dist_min A) = the carrier of (TopSpaceMetr M) by FUNCT_2:def 1;
then lower_bound ([#] ((dist_min A) .: B)) >= r by A2, A3, SEQ_4:43;
then lower_bound ((dist_min A) .: B) >= r by WEIERSTR:def 3;
hence min_dist_min (A,B) >= r by WEIERSTR:def 7; :: thesis: verum