let N, M be non empty MetrSpace; for f being Function of N,M
for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st g = f & TopSpaceMetr N is compact & g is continuous holds
f is uniformly_continuous
let f be Function of N,M; for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st g = f & TopSpaceMetr N is compact & g is continuous holds
f is uniformly_continuous
let g be Function of (TopSpaceMetr N),(TopSpaceMetr M); ( g = f & TopSpaceMetr N is compact & g is continuous implies f is uniformly_continuous )
assume that
A1:
g = f
and
A2:
TopSpaceMetr N is compact
and
A3:
g is continuous
; f is uniformly_continuous
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for u1, u2 being Element of N st dist u1,u2 < s holds
dist (f /. u1),(f /. u2) < r ) )
proof
let r be
Real;
( 0 < r implies ex s being Real st
( 0 < s & ( for u1, u2 being Element of N st dist u1,u2 < s holds
dist (f /. u1),(f /. u2) < r ) ) )
set G =
{ P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st
( P = Ball w,s & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist w,w1 < s holds
dist w2,w3 < r / 2 ) ) } ;
A4:
the
carrier of
(TopSpaceMetr N) = the
carrier of
N
by TOPMETR:16;
{ P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st
( P = Ball w,s & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist w,w1 < s holds
dist w2,w3 < r / 2 ) ) } c= bool the
carrier of
N
proof
let x be
set ;
TARSKI:def 3 ( not x in { P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st
( P = Ball w,s & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist w,w1 < s holds
dist w2,w3 < r / 2 ) ) } or x in bool the carrier of N )
assume
x in { P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st
( P = Ball w,s & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist w,w1 < s holds
dist w2,w3 < r / 2 ) ) }
;
x in bool the carrier of N
then
ex
P being
Subset of
(TopSpaceMetr N) st
(
x = P & ex
w being
Element of
N ex
s being
Real st
(
P = Ball w,
s & ( for
w1 being
Element of
N for
w2,
w3 being
Element of
M st
w2 = f . w &
w3 = f . w1 &
dist w,
w1 < s holds
dist w2,
w3 < r / 2 ) ) )
;
hence
x in bool the
carrier of
N
;
verum
end;
then reconsider G1 =
{ P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st
( P = Ball w,s & ( for w1 being Element of N
for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist w,w1 < s holds
dist w2,w3 < r / 2 ) ) } as
Subset-Family of
(TopSpaceMetr N) by TOPMETR:16;
for
P3 being
Subset of
(TopSpaceMetr N) st
P3 in G1 holds
P3 is
open
then A5:
G1 is
open
by TOPS_2:def 1;
assume
0 < r
;
ex s being Real st
( 0 < s & ( for u1, u2 being Element of N st dist u1,u2 < s holds
dist (f /. u1),(f /. u2) < r ) )
then A6:
0 < r / 2
by XREAL_1:217;
A7:
the
carrier of
N c= union G1
proof
let x be
set ;
TARSKI:def 3 ( not x in the carrier of N or x in union G1 )
assume
x in the
carrier of
N
;
x in union G1
then reconsider w0 =
x as
Element of
N ;
g . w0 = f /. w0
by A1;
then reconsider w4 =
g . w0 as
Element of
M ;
consider s4 being
Real such that A8:
s4 > 0
and A9:
for
u5 being
Element of
N for
w5 being
Element of
M st
w5 = g . u5 &
dist w0,
u5 < s4 holds
dist w4,
w5 < r / 2
by A3, A6, Th5;
reconsider P2 =
Ball w0,
s4 as
Subset of
(TopSpaceMetr N) by TOPMETR:16;
for
w1 being
Element of
N for
w2,
w3 being
Element of
M st
w2 = f . w0 &
w3 = f . w1 &
dist w0,
w1 < s4 holds
dist w2,
w3 < r / 2
by A1, A9;
then
ex
w being
Element of
N ex
s being
Real st
(
P2 = Ball w,
s & ( for
w1 being
Element of
N for
w2,
w3 being
Element of
M st
w2 = f . w &
w3 = f . w1 &
dist w,
w1 < s holds
dist w2,
w3 < r / 2 ) )
;
then A10:
Ball w0,
s4 in G1
;
x in Ball w0,
s4
by A8, GOBOARD6:4;
hence
x in union G1
by A10, TARSKI:def 4;
verum
end;
the
carrier of
(TopSpaceMetr N) = the
carrier of
N
by TOPMETR:16;
then
the
carrier of
N = union G1
by A7, XBOOLE_0:def 10;
then
G1 is
Cover of
(TopSpaceMetr N)
by A4, SETFAM_1:60;
then consider s1 being
Real such that A11:
s1 > 0
and A12:
for
w1,
w2 being
Element of
N st
dist w1,
w2 < s1 holds
ex
Ga being
Subset of
(TopSpaceMetr N) st
(
w1 in Ga &
w2 in Ga &
Ga in G1 )
by A2, A5, Th7;
for
u1,
u2 being
Element of
N st
dist u1,
u2 < s1 holds
dist (f /. u1),
(f /. u2) < r
proof
let u1,
u2 be
Element of
N;
( dist u1,u2 < s1 implies dist (f /. u1),(f /. u2) < r )
assume
dist u1,
u2 < s1
;
dist (f /. u1),(f /. u2) < r
then consider Ga being
Subset of
(TopSpaceMetr N) such that A13:
u1 in Ga
and A14:
u2 in Ga
and A15:
Ga in G1
by A12;
consider P being
Subset of
(TopSpaceMetr N) such that A16:
Ga = P
and A17:
ex
w being
Element of
N ex
s2 being
Real st
(
P = Ball w,
s2 & ( for
w1 being
Element of
N for
w2,
w3 being
Element of
M st
w2 = f . w &
w3 = f . w1 &
dist w,
w1 < s2 holds
dist w2,
w3 < r / 2 ) )
by A15;
consider w being
Element of
N,
s2 being
Real such that A18:
P = Ball w,
s2
and A19:
for
w1 being
Element of
N for
w2,
w3 being
Element of
M st
w2 = f . w &
w3 = f . w1 &
dist w,
w1 < s2 holds
dist w2,
w3 < r / 2
by A17;
dist w,
u2 < s2
by A14, A16, A18, METRIC_1:12;
then A20:
dist (f /. w),
(f /. u2) < r / 2
by A19;
dist w,
u1 < s2
by A13, A16, A18, METRIC_1:12;
then
dist (f /. w),
(f /. u1) < r / 2
by A19;
then
(
dist (f /. u1),
(f /. u2) <= (dist (f /. u1),(f /. w)) + (dist (f /. w),(f /. u2)) &
(dist (f /. w),(f /. u1)) + (dist (f /. w),(f /. u2)) < (r / 2) + (r / 2) )
by A20, METRIC_1:4, XREAL_1:10;
hence
dist (f /. u1),
(f /. u2) < r
by XXREAL_0:2;
verum
end;
hence
ex
s being
Real st
(
0 < s & ( for
u1,
u2 being
Element of
N st
dist u1,
u2 < s holds
dist (f /. u1),
(f /. u2) < r ) )
by A11;
verum
end;
hence
f is uniformly_continuous
by Def1; verum