let M be non empty MetrSpace; :: thesis: for X being Subset of (TopSpaceMetr M) st X <> {} & X is compact holds
dist_min X is continuous
let X be Subset of (TopSpaceMetr M); :: thesis: ( X <> {} & X is compact implies dist_min X is continuous )
assume A1:
( X <> {} & X is compact )
; :: thesis: dist_min X is continuous
for P being Subset of R^1 st P is open holds
(dist_min X) " P is open
proof
let P be
Subset of
R^1 ;
:: thesis: ( P is open implies (dist_min X) " P is open )
assume A2:
P is
open
;
:: thesis: (dist_min X) " P is open
thus
(dist_min X) " P is
open
:: thesis: verumproof
for
p being
Point of
M st
p in (dist_min X) " P holds
ex
r being
real number st
(
r > 0 &
Ball p,
r c= (dist_min X) " P )
proof
let p be
Point of
M;
:: thesis: ( p in (dist_min X) " P implies ex r being real number st
( r > 0 & Ball p,r c= (dist_min X) " P ) )
assume A3:
p in (dist_min X) " P
;
:: thesis: ex r being real number st
( r > 0 & Ball p,r c= (dist_min X) " P )
ex
r being
Real st
(
r > 0 &
Ball p,
r c= (dist_min X) " P )
proof
A4:
(
p in dom (dist_min X) &
(dist_min X) . p in P )
by A3, FUNCT_1:def 13;
consider y being
Point of
RealSpace such that A5:
y = lower_bound ((dist p) .: X)
by METRIC_1:def 14;
reconsider P =
P as
Subset of
(TopSpaceMetr RealSpace ) by TOPMETR:def 7;
y in P
by A4, A5, Def8;
then consider r being
real number such that A6:
(
r > 0 &
Ball y,
r c= P )
by A2, TOPMETR:22, TOPMETR:def 7;
reconsider r =
r as
Real by XREAL_0:def 1;
A7:
Ball p,
r c= (dist_min X) " P
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in Ball p,r or z in (dist_min X) " P )
assume A8:
z in Ball p,
r
;
:: thesis: z in (dist_min X) " P
then reconsider z =
z as
Point of
M ;
dist p,
z < r
by A8, METRIC_1:12;
then
(abs ((lower_bound ((dist p) .: X)) - (lower_bound ((dist z) .: X)))) + (dist p,z) < r + (dist p,z)
by A1, Th28, XREAL_1:10;
then A9:
abs ((lower_bound ((dist p) .: X)) - (lower_bound ((dist z) .: X))) < r
by XREAL_1:8;
consider q being
Point of
RealSpace such that A10:
q = lower_bound ((dist z) .: X)
by METRIC_1:def 14;
A11:
q = (dist_min X) . z
by A10, Def8;
dist y,
q < r
by A5, A9, A10, TOPMETR:15;
then A12:
q in Ball y,
r
by METRIC_1:12;
dom (dist_min X) = the
carrier of
(TopSpaceMetr M)
by FUNCT_2:def 1;
then
dom (dist_min X) = the
carrier of
M
by TOPMETR:16;
hence
z in (dist_min X) " P
by A6, A11, A12, FUNCT_1:def 13;
:: thesis: verum
end;
take
r
;
:: thesis: ( r > 0 & Ball p,r c= (dist_min X) " P )
thus
(
r > 0 &
Ball p,
r c= (dist_min X) " P )
by A6, A7;
:: thesis: verum
end;
hence
ex
r being
real number st
(
r > 0 &
Ball p,
r c= (dist_min X) " P )
;
:: thesis: verum
end;
hence
(dist_min X) " P is
open
by TOPMETR:22;
:: thesis: verum
end;
end;
hence
dist_min X is continuous
by Lm2, TOPS_2:55; :: thesis: verum