let N, M be non empty MetrSpace; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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 ) )

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; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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

hence
f is uniformly_continuous
; :: thesis: verum
let r be Real; :: thesis: ( 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

( 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

assume 0 < r ; :: thesis: 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

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

( 0 < s & ( for u1, u2 being Element of N st dist (u1,u2) < s holds

dist ((f /. u1),(f /. u2)) < r ) ) by A11; :: thesis: verum

end;( 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

then reconsider G1 = { P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ) ) } ; :: thesis: 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 ; :: thesis: verum

end;( 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 ) ) } ; :: thesis: 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 ; :: thesis: verum

( 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

proof

then A5:
G1 is open
by TOPS_2:def 1;
let P3 be Subset of (TopSpaceMetr N); :: thesis: ( P3 in G1 implies P3 is open )

assume P3 in G1 ; :: thesis: P3 is open

then ex P being Subset of (TopSpaceMetr N) st

( P3 = 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 P3 is open by TOPMETR:14; :: thesis: verum

end;assume P3 in G1 ; :: thesis: P3 is open

then ex P being Subset of (TopSpaceMetr N) st

( P3 = 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 P3 is open by TOPMETR:14; :: thesis: verum

assume 0 < r ; :: thesis: 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

the carrier of (TopSpaceMetr N) = the carrier of N
by TOPMETR:12;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of N or x in union G1 )

assume x in the carrier of N ; :: thesis: 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; :: thesis: verum

end;assume x in the carrier of N ; :: thesis: 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; :: thesis: verum

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

hence
ex s being Real st
let u1, u2 be Element of N; :: thesis: ( dist (u1,u2) < s1 implies dist ((f /. u1),(f /. u2)) < r )

assume dist (u1,u2) < s1 ; :: thesis: 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; :: thesis: verum

end;assume dist (u1,u2) < s1 ; :: thesis: 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; :: thesis: verum

( 0 < s & ( for u1, u2 being Element of N st dist (u1,u2) < s holds

dist ((f /. u1),(f /. u2)) < r ) ) by A11; :: thesis: verum