let T be non empty TopSpace; for f being RealMap of T st f is continuous holds
for F being RealMap of [:T,T:] st ( for x, y being Element of T holds F . x,y = abs ((f . x) - (f . y)) ) holds
F is continuous
let f be RealMap of T; ( f is continuous implies for F being RealMap of [:T,T:] st ( for x, y being Element of T holds F . x,y = abs ((f . x) - (f . y)) ) holds
F is continuous )
assume A1:
f is continuous
; for F being RealMap of [:T,T:] st ( for x, y being Element of T holds F . x,y = abs ((f . x) - (f . y)) ) holds
F is continuous
set TT = [:T,T:];
set cT = the carrier of T;
reconsider f9 = f as Function of T,R^1 by TOPMETR:24;
let F be RealMap of [:T,T:]; ( ( for x, y being Element of T holds F . x,y = abs ((f . x) - (f . y)) ) implies F is continuous )
assume A2:
for x, y being Element of T holds F . x,y = abs ((f . x) - (f . y))
; F is continuous
reconsider F9 = F as Function of [:T,T:],R^1 by TOPMETR:24;
A3:
f9 is continuous
by A1, TOPREAL6:83;
now let tt be
Point of
[:T,T:];
F9 is_continuous_at tt
tt in the
carrier of
[:T,T:]
;
then
tt in [:the carrier of T,the carrier of T:]
by BORSUK_1:def 5;
then consider t1,
t2 being
set such that A4:
(
t1 in the
carrier of
T &
t2 in the
carrier of
T )
and A5:
[t1,t2] = tt
by ZFMISC_1:def 2;
reconsider t1 =
t1,
t2 =
t2 as
Point of
T by A4;
for
R being
Subset of
R^1 st
R is
open &
F9 . tt in R holds
ex
H being
Subset of
[:T,T:] st
(
H is
open &
tt in H &
F9 .: H c= R )
proof
reconsider ft1 =
f . t1,
ft2 =
f . t2 as
Point of
RealSpace by METRIC_1:def 14;
reconsider Ftt =
F . tt as
Point of
RealSpace by METRIC_1:def 14;
let R be
Subset of
R^1 ;
( R is open & F9 . tt in R implies ex H being Subset of [:T,T:] st
( H is open & tt in H & F9 .: H c= R ) )
assume
(
R is
open &
F9 . tt in R )
;
ex H being Subset of [:T,T:] st
( H is open & tt in H & F9 .: H c= R )
then consider r being
real number such that A6:
r > 0
and A7:
Ball Ftt,
r c= R
by TOPMETR:22, TOPMETR:def 7;
reconsider r9 =
r as
Real by XREAL_0:def 1;
reconsider A =
Ball ft1,
(r9 / 2),
B =
Ball ft2,
(r9 / 2) as
Subset of
R^1 by METRIC_1:def 14, TOPMETR:24;
A8:
(
A is
open &
f9 is_continuous_at t1 )
by A3, TMAP_1:55, TOPMETR:21, TOPMETR:def 7;
f . t1 in A
by A6, Lm7, XREAL_1:141;
then consider T1 being
Subset of
T such that A9:
T1 is
open
and A10:
t1 in T1
and A11:
f9 .: T1 c= A
by A8, TMAP_1:48;
A12:
(
B is
open &
f9 is_continuous_at t2 )
by A3, TMAP_1:55, TOPMETR:21, TOPMETR:def 7;
f . t2 in B
by A6, Lm7, XREAL_1:141;
then consider T2 being
Subset of
T such that A13:
T2 is
open
and A14:
t2 in T2
and A15:
f9 .: T2 c= B
by A12, TMAP_1:48;
F . tt = F . t1,
t2
by A5;
then A16:
abs ((f9 . t1) - (f9 . t2)) = F . tt
by A2;
A17:
F .: [:T1,T2:] c= R
proof
let Fxy be
set ;
TARSKI:def 3 ( not Fxy in F .: [:T1,T2:] or Fxy in R )
assume
Fxy in F .: [:T1,T2:]
;
Fxy in R
then consider xy being
set such that
xy in dom F
and A18:
xy in [:T1,T2:]
and A19:
Fxy = F . xy
by FUNCT_1:def 12;
consider x,
y being
set such that A20:
x in T1
and A21:
y in T2
and A22:
xy = [x,y]
by A18, ZFMISC_1:def 2;
reconsider x =
x,
y =
y as
Point of
T by A20, A21;
reconsider fx =
f . x,
fy =
f . y as
Point of
RealSpace by METRIC_1:def 14;
y in the
carrier of
T
;
then
y in dom f
by FUNCT_2:def 1;
then
f . y in f .: T2
by A21, FUNCT_1:def 12;
then A23:
dist fy,
ft2 < r9 / 2
by A15, METRIC_1:12;
reconsider Fxy1 =
F . [x,y] as
Point of
RealSpace by METRIC_1:def 14;
A24:
abs ((f . x) - (f . y)) = F . x,
y
by A2;
then
F . [x,y] <= ((abs ((f . x) - (f . t1))) + (F . tt)) + (abs ((f . t2) - (f . y)))
by A16, Lm2;
then
F . [x,y] <= ((abs ((f . x) - (f . t1))) + (F . tt)) + (dist ft2,fy)
by TOPMETR:15;
then A25:
(F . [x,y]) + 0 <= ((F . tt) + (dist fx,ft1)) + (dist ft2,fy)
by TOPMETR:15;
F . tt <= ((abs ((f . t1) - (f . x))) + (F . [x,y])) + (abs ((f . y) - (f . t2)))
by A16, A24, Lm2;
then
F . tt <= ((dist fx,ft1) + (F . [x,y])) + (abs ((f . y) - (f . t2)))
by TOPMETR:15;
then A26:
F . tt <= ((F . [x,y]) + (dist fx,ft1)) + (dist fy,ft2)
by TOPMETR:15;
x in the
carrier of
T
;
then
x in dom f
by FUNCT_2:def 1;
then
f . x in f .: T1
by A20, FUNCT_1:def 12;
then
dist fx,
ft1 < r9 / 2
by A11, METRIC_1:12;
then A27:
(dist fx,ft1) + (dist fy,ft2) < (r9 / 2) + (r9 / 2)
by A23, XREAL_1:10;
then
(F . [x,y]) + ((dist fx,ft1) + (dist fy,ft2)) < (F . [x,y]) + r9
by XREAL_1:10;
then
F . tt < - ((- (F . [x,y])) - r9)
by A26, XXREAL_0:2;
then
(- (F . tt)) - 0 > (- r9) - (F . [x,y])
by XREAL_1:28;
then A28:
(- (F . tt)) + (F . [x,y]) > (- r9) + 0
by XREAL_1:23;
(F . tt) + ((dist fx,ft1) + (dist ft2,fy)) < (F . tt) + r9
by A27, XREAL_1:10;
then
(F . [x,y]) + 0 < (F . tt) + r9
by A25, XXREAL_0:2;
then
(F . [x,y]) - (F . tt) < r9 - 0
by XREAL_1:23;
then
abs ((F . [x,y]) - (F . tt)) < r9
by A28, SEQ_2:9;
then
dist Ftt,
Fxy1 < r9
by TOPMETR:15;
then
Fxy1 in Ball Ftt,
r
by METRIC_1:12;
hence
Fxy in R
by A7, A19, A22;
verum
end;
tt in [:T1,T2:]
by A5, A10, A14, ZFMISC_1:def 2;
hence
ex
H being
Subset of
[:T,T:] st
(
H is
open &
tt in H &
F9 .: H c= R )
by A9, A13, A17, BORSUK_1:46;
verum
end; hence
F9 is_continuous_at tt
by TMAP_1:48;
verum end;
then
F9 is continuous
by TMAP_1:55;
hence
F is continuous
by TOPREAL6:83; verum