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