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 5;
then reconsider pmet9 = pmet as RealMap of [:T,T:] ;
reconsider pmetR = pmet9 as Function of [:T,T:],R^1 by TOPMETR:24;
let x be Point of T; dist pmet,x is continuous
reconsider distx = dist pmet,x as Function of T,R^1 by TOPMETR:24;
pmet9 is continuous
by A1;
then A2:
pmetR is continuous
by TOPREAL6:83;
now let 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 5;
A3:
dom (pr2 the carrier of T,the carrier of T) = [:the carrier of T,the carrier of T:]
by FUNCT_3:def 6;
A4:
(
pmetR is_continuous_at xt &
distx . t = pmet . x,
t )
by A2, Def2, TMAP_1:55;
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:48;
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:128;
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 12;
then A8:
t in (pr2 the carrier of T,the carrier of T) .: (XU /\ [:{x},the carrier of T:])
by FUNCT_3:def 6;
A9:
distx .: ((pr2 the carrier of T,the carrier of T) .: (XU /\ [:{x},the carrier of T:])) c= R
proof
let du be
set ;
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
set 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 12;
reconsider u =
u as
Point of
T by A10;
consider xu being
set 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 12;
consider x9,
u9 being
set 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 6, ZFMISC_1:128;
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 12;
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:48;
verum end;
then
distx is continuous
by TMAP_1:55;
hence
dist pmet,x is continuous
by TOPREAL6:83; verum