let T be non empty TopSpace; for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) holds
for x being Point of T holds dist (pmet,x) is continuous
set cT = the carrier of T;
let pmet be Function of [: the carrier of T, the carrier of T:],REAL; ( ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) implies for x being Point of T holds dist (pmet,x) is continuous )
assume A1:
for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous
; for x being Point of T holds dist (pmet,x) is continuous
[: the carrier of T, the carrier of T:] = the carrier of [:T,T:]
by BORSUK_1:def 2;
then reconsider pmet9 = pmet as RealMap of [:T,T:] ;
reconsider pmetR = pmet9 as Function of [:T,T:],R^1 by TOPMETR:17;
let x be Point of T; dist (pmet,x) is continuous
reconsider distx = dist (pmet,x) as Function of T,R^1 by TOPMETR:17;
pmet9 is continuous
by A1;
then A2:
pmetR is continuous
by JORDAN5A:27;
now for t being Point of T holds distx is_continuous_at tlet t be
Point of
T;
distx is_continuous_at t
for
R being
Subset of
R^1 st
R is
open &
distx . t in R holds
ex
U being
Subset of
T st
(
U is
open &
t in U &
distx .: U c= R )
proof
reconsider xt =
[x,t] as
Point of
[:T,T:] by BORSUK_1:def 2;
A3:
dom (pr2 ( the carrier of T, the carrier of T)) = [: the carrier of T, the carrier of T:]
by FUNCT_3:def 5;
A4:
(
pmetR is_continuous_at xt &
distx . t = pmet . (
x,
t) )
by A2, Def2, TMAP_1:50;
let R be
Subset of
R^1;
( R is open & distx . t in R implies ex U being Subset of T st
( U is open & t in U & distx .: U c= R ) )
assume
(
R is
open &
distx . t in R )
;
ex U being Subset of T st
( U is open & t in U & distx .: U c= R )
then consider XU being
Subset of
[:T,T:] such that A5:
XU is
open
and A6:
xt in XU
and A7:
pmetR .: XU c= R
by A4, TMAP_1:43;
set U =
(pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:]);
[x,t] in [:{x}, the carrier of T:]
by ZFMISC_1:105;
then
[x,t] in XU /\ [:{x}, the carrier of T:]
by A6, XBOOLE_0:def 4;
then
(pr2 ( the carrier of T, the carrier of T)) . (
x,
t)
in (pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:])
by A3, FUNCT_1:def 6;
then A8:
t in (pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:])
by FUNCT_3:def 5;
A9:
distx .: ((pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:])) c= R
proof
let du be
object ;
TARSKI:def 3 ( not du in distx .: ((pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:])) or du in R )
assume
du in distx .: ((pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:]))
;
du in R
then consider u being
object such that A10:
u in dom distx
and A11:
u in (pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:])
and A12:
distx . u = du
by FUNCT_1:def 6;
reconsider u =
u as
Point of
T by A10;
consider xu being
object such that A13:
xu in dom (pr2 ( the carrier of T, the carrier of T))
and A14:
xu in XU /\ [:{x}, the carrier of T:]
and A15:
(pr2 ( the carrier of T, the carrier of T)) . xu = u
by A11, FUNCT_1:def 6;
consider x9,
u9 being
object such that A16:
(
x9 in the
carrier of
T &
u9 in the
carrier of
T )
and A17:
xu = [x9,u9]
by A13, ZFMISC_1:def 2;
reconsider x9 =
x9,
u9 =
u9 as
Point of
T by A16;
[x9,u9] in [:{x}, the carrier of T:]
by A14, A17, XBOOLE_0:def 4;
then
(
(pr2 ( the carrier of T, the carrier of T)) . (
x9,
u9)
= u9 &
x9 = x )
by FUNCT_3:def 5, ZFMISC_1:105;
then A18:
pmet . (
x9,
u9)
= du
by A12, A15, A17, Def2;
A19:
dom pmetR = the
carrier of
[:T,T:]
by FUNCT_2:def 1;
[x9,u9] in XU
by A14, A17, XBOOLE_0:def 4;
then
du in pmetR .: XU
by A18, A19, FUNCT_1:def 6;
hence
du in R
by A7;
verum
end;
(pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:]) is
open
by A5, Th3;
hence
ex
U being
Subset of
T st
(
U is
open &
t in U &
distx .: U c= R )
by A8, A9;
verum
end; hence
distx is_continuous_at t
by TMAP_1:43;
verum end;
then
distx is continuous
by TMAP_1:50;
hence
dist (pmet,x) is continuous
by JORDAN5A:27; verum