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:12;
{ 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
object ;
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:12;
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:215;
A7:
the
carrier of
N c= union G1
proof
let x be
object ;
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, Th4;
reconsider P2 =
Ball (
w0,
s4) as
Subset of
(TopSpaceMetr N) by TOPMETR:12;
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:1;
hence
x in union G1
by A10, TARSKI:def 4;
verum
end;
the
carrier of
(TopSpaceMetr N) = the
carrier of
N
by TOPMETR:12;
then
the
carrier of
N = union G1
by A7, XBOOLE_0:def 10;
then
G1 is
Cover of
(TopSpaceMetr N)
by A4, SETFAM_1:45;
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, Th6;
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:11;
then A20:
dist (
(f /. w),
(f /. u2))
< r / 2
by A19;
dist (
w,
u1)
< s2
by A13, A16, A18, METRIC_1:11;
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:8;
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
; verum