let N, M be non empty MetrSpace; for f being Function of N,M
for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f = g & f is uniformly_continuous holds
g is continuous
let f be Function of N,M; for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f = g & f is uniformly_continuous holds
g is continuous
let g be Function of (TopSpaceMetr N),(TopSpaceMetr M); ( f = g & f is uniformly_continuous implies g is continuous )
assume that
A1:
f = g
and
A2:
f is uniformly_continuous
; g is continuous
for r being Real
for u being Element of N
for u1 being Element of M st r > 0 & u1 = g . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
proof
let r be
Real;
for u being Element of N
for u1 being Element of M st r > 0 & u1 = g . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist (u,w) < s holds
dist (u1,w1) < r ) )let u be
Element of
N;
for u1 being Element of M st r > 0 & u1 = g . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist (u,w) < s holds
dist (u1,w1) < r ) )let u1 be
Element of
M;
( r > 0 & u1 = g . u implies ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) )
reconsider r9 =
r as
Real ;
assume that A3:
r > 0
and A4:
u1 = g . u
;
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = g . w & dist (u,w) < s holds
dist (u1,w1) < r ) )
consider s being
Real such that A5:
0 < s
and A6:
for
wu1,
wu2 being
Element of
N st
dist (
wu1,
wu2)
< s holds
dist (
(f /. wu1),
(f /. wu2))
< r
by A2, A3;
for
w being
Element of
N for
w1 being
Element of
M st
w1 = g . w &
dist (
u,
w)
< s holds
dist (
u1,
w1)
< r
proof
let w be
Element of
N;
for w1 being Element of M st w1 = g . w & dist (u,w) < s holds
dist (u1,w1) < rlet w1 be
Element of
M;
( w1 = g . w & dist (u,w) < s implies dist (u1,w1) < r )
assume that A7:
w1 = g . w
and A8:
dist (
u,
w)
< s
;
dist (u1,w1) < r
A9:
u1 = f /. u
by A1, A4;
w1 = f /. w
by A1, A7;
hence
dist (
u1,
w1)
< r
by A6, A8, A9;
verum
end;
hence
ex
s being
Real st
(
s > 0 & ( for
w being
Element of
N for
w1 being
Element of
M st
w1 = g . w &
dist (
u,
w)
< s holds
dist (
u1,
w1)
< r ) )
by A5;
verum
end;
hence
g is continuous
by Th3; verum