let M be non empty MetrSpace; 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); ( X <> {} & X is compact implies dist_min X is continuous )
assume A1:
( X <> {} & X is compact )
; 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;
( P is open implies (dist_min X) " P is open )
assume A2:
P is
open
;
(dist_min X) " P is open
for
p being
Point of
M st
p in (dist_min X) " P holds
ex
r being
Real st
(
r > 0 &
Ball (
p,
r)
c= (dist_min X) " P )
proof
let p be
Point of
M;
( p in (dist_min X) " P implies ex r being Real st
( r > 0 & Ball (p,r) c= (dist_min X) " P ) )
assume A3:
p in (dist_min X) " P
;
ex r being Real 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:
(dist_min X) . p in P
by A3, FUNCT_1:def 7;
reconsider P =
P as
Subset of
(TopSpaceMetr RealSpace) by TOPMETR:def 6;
set y =
lower_bound ((dist p) .: X);
lower_bound ((dist p) .: X) in REAL
by XREAL_0:def 1;
then reconsider y =
lower_bound ((dist p) .: X) as
Point of
RealSpace by METRIC_1:def 13;
y in P
by A4, Def6;
then consider r being
Real such that A5:
r > 0
and A6:
Ball (
y,
r)
c= P
by A2, TOPMETR:15, TOPMETR:def 6;
reconsider r =
r as
Real ;
take
r
;
( r > 0 & Ball (p,r) c= (dist_min X) " P )
Ball (
p,
r)
c= (dist_min X) " P
proof
let z be
object ;
TARSKI:def 3 ( not z in Ball (p,r) or z in (dist_min X) " P )
assume A7:
z in Ball (
p,
r)
;
z in (dist_min X) " P
then reconsider z =
z as
Point of
M ;
set q =
lower_bound ((dist z) .: X);
lower_bound ((dist z) .: X) in REAL
by XREAL_0:def 1;
then reconsider q =
lower_bound ((dist z) .: X) as
Point of
RealSpace by METRIC_1:def 13;
dist (
p,
z)
< r
by A7, METRIC_1:11;
then
|.((lower_bound ((dist p) .: X)) - (lower_bound ((dist z) .: X))).| + (dist (p,z)) < r + (dist (p,z))
by A1, Th22, XREAL_1:8;
then
|.((lower_bound ((dist p) .: X)) - (lower_bound ((dist z) .: X))).| < r
by XREAL_1:6;
then
dist (
y,
q)
< r
by TOPMETR:11;
then A8:
q in Ball (
y,
r)
by METRIC_1:11;
dom (dist_min X) = the
carrier of
(TopSpaceMetr M)
by FUNCT_2:def 1;
then A9:
dom (dist_min X) = the
carrier of
M
by TOPMETR:12;
q = (dist_min X) . z
by Def6;
hence
z in (dist_min X) " P
by A6, A8, A9, FUNCT_1:def 7;
verum
end;
hence
(
r > 0 &
Ball (
p,
r)
c= (dist_min X) " P )
by A5;
verum
end;
hence
ex
r being
Real st
(
r > 0 &
Ball (
p,
r)
c= (dist_min X) " P )
;
verum
end;
hence
(dist_min X) " P is
open
by TOPMETR:15;
verum
end;
hence
dist_min X is continuous
by Lm2, TOPS_2:43; verum