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