set d = dist_min A;
set TM = TopSpaceMetr M;
A1:
for P being Subset of R^1 st P is open holds
(dist_min A) " P is open
proof
let P be
Subset of
R^1;
( P is open implies (dist_min A) " P is open )
assume A2:
P is
open
;
(dist_min A) " P is open
for
p being
Point of
M st
p in (dist_min A) " P holds
ex
r being
Real st
(
r > 0 &
Ball (
p,
r)
c= (dist_min A) " P )
proof
reconsider P9 =
P as
open Subset of
(TopSpaceMetr RealSpace) by A2, TOPMETR:def 6;
let p be
Point of
M;
( p in (dist_min A) " P implies ex r being Real st
( r > 0 & Ball (p,r) c= (dist_min A) " P ) )
assume
p in (dist_min A) " P
;
ex r being Real st
( r > 0 & Ball (p,r) c= (dist_min A) " P )
then A3:
(dist_min A) . p in P
by FUNCT_1:def 7;
then reconsider dp =
(dist_min A) . p as
Point of
RealSpace by TOPMETR:def 6;
consider r being
Real such that A4:
r > 0
and A5:
Ball (
dp,
r)
c= P9
by A3, TOPMETR:15;
take
r
;
( r > 0 & Ball (p,r) c= (dist_min A) " P )
thus
r > 0
by A4;
Ball (p,r) c= (dist_min A) " P
thus
Ball (
p,
r)
c= (dist_min A) " P
verumproof
let x be
object ;
TARSKI:def 3 ( not x in Ball (p,r) or x in (dist_min A) " P )
assume A6:
x in Ball (
p,
r)
;
x in (dist_min A) " P
then reconsider q =
x as
Point of
M ;
A7:
dist (
p,
q)
< r
by A6, METRIC_1:11;
A8:
dom (dist_min A) = [#] M
by FUNCT_2:def 1;
then
(dist_min A) . q in rng (dist_min A)
by FUNCT_1:def 3;
then reconsider dq =
(dist_min A) . q as
Point of
RealSpace by TOPMETR:def 6;
(dist_min A) . q <= (dist (q,p)) + ((dist_min A) . p)
by HAUSDORF:15;
then
((dist_min A) . q) - ((dist_min A) . p) <= dist (
p,
q)
by XREAL_1:20;
then A9:
- (dist (p,q)) <= - (((dist_min A) . q) - ((dist_min A) . p))
by XREAL_1:24;
(dist_min A) . p <= (dist (p,q)) + ((dist_min A) . q)
by HAUSDORF:15;
then
((dist_min A) . p) - ((dist_min A) . q) <= dist (
p,
q)
by XREAL_1:20;
then
|.(((dist_min A) . p) - ((dist_min A) . q)).| <= dist (
p,
q)
by A9, ABSVALUE:5;
then
|.(((dist_min A) . p) - ((dist_min A) . q)).| < r
by A7, XXREAL_0:2;
then
dist (
dp,
dq)
< r
by METRIC_1:def 12;
then
dq in Ball (
dp,
r)
by METRIC_1:11;
hence
x in (dist_min A) " P
by A5, A8, FUNCT_1:def 7;
verum
end;
end;
hence
(dist_min A) " P is
open
by TOPMETR:15;
verum
end;
( [#] R^1 = {} implies [#] (TopSpaceMetr M) = {} )
;
hence
dist_min A is continuous
by A1, TOPS_2:43; verum