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