let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T

for Y being Subset of S st Y is compact & f is_continuous_on Y holds

f is_uniformly_continuous_on Y

let f be PartFunc of S,T; :: thesis: for Y being Subset of S st Y is compact & f is_continuous_on Y holds

f is_uniformly_continuous_on Y

let Y be Subset of S; :: thesis: ( Y is compact & f is_continuous_on Y implies f is_uniformly_continuous_on Y )

assume that

A1: Y is compact and

A2: f is_continuous_on Y ; :: thesis: f is_uniformly_continuous_on Y

A3: Y c= dom f by A2, NFCONT_1:def 7;

assume not f is_uniformly_continuous_on Y ; :: thesis: contradiction

then consider r being Real such that

A4: 0 < r and

A5: for s being Real st 0 < s holds

ex x1, x2 being Point of S st

( x1 in Y & x2 in Y & ||.(x1 - x2).|| < s & not ||.((f /. x1) - (f /. x2)).|| < r ) by A3;

defpred S_{1}[ Nat, Point of S] means ( $2 in Y & ex x2 being Point of S st

( x2 in Y & ||.($2 - x2).|| < 1 / ($1 + 1) & not ||.((f /. $2) - (f /. x2)).|| < r ) );

A6: for n being Nat holds 0 < 1 / (n + 1) by XREAL_1:139;

A9: for n being Element of NAT holds S_{1}[n,s1 . n]
from FUNCT_2:sch 3(A7);

defpred S_{2}[ Nat, Point of S] means ( $2 in Y & ||.((s1 . $1) - $2).|| < 1 / ($1 + 1) & not ||.((f /. (s1 . $1)) - (f /. $2)).|| < r );

A10: for n being Element of NAT ex x2 being Point of S st S_{2}[n,x2]
by A9;

consider s2 being sequence of S such that

A11: for n being Element of NAT holds S_{2}[n,s2 . n]
from FUNCT_2:sch 3(A10);

then consider q1 being sequence of S such that

A14: q1 is subsequence of s1 and

A15: q1 is convergent and

A16: lim q1 in Y by A1, NFCONT_1:def 2;

consider Ns1 being increasing sequence of NAT such that

A17: q1 = s1 * Ns1 by A14, VALUED_0:def 17;

set q2 = q1 - ((s1 - s2) * Ns1);

A18: f | Y is_continuous_in lim q1 by A2, A16, NFCONT_1:def 7;

then rng (q1 - ((s1 - s2) * Ns1)) c= rng s2 by VALUED_0:21;

then A22: rng (q1 - ((s1 - s2) * Ns1)) c= Y by A20, XBOOLE_1:1;

then rng (q1 - ((s1 - s2) * Ns1)) c= dom f by A3, XBOOLE_1:1;

then rng (q1 - ((s1 - s2) * Ns1)) c= (dom f) /\ Y by A22, XBOOLE_1:19;

then A23: rng (q1 - ((s1 - s2) * Ns1)) c= dom (f | Y) by RELAT_1:61;

then A31: (s1 - s2) * Ns1 is convergent by LOPBAN_3:7;

then A32: q1 - ((s1 - s2) * Ns1) is convergent by A15, NORMSP_1:20;

rng q1 c= rng s1 by A14, VALUED_0:21;

then A33: rng q1 c= Y by A13, XBOOLE_1:1;

then rng q1 c= dom f by A3, XBOOLE_1:1;

then rng q1 c= (dom f) /\ Y by A33, XBOOLE_1:19;

then A34: rng q1 c= dom (f | Y) by RELAT_1:61;

then A35: (f | Y) /. (lim q1) = lim ((f | Y) /* q1) by A15, A18, NFCONT_1:def 5;

A36: (f | Y) /* q1 is convergent by A15, A18, A34, NFCONT_1:def 5;

lim (s1 - s2) = 0. S by A24, A30, NORMSP_1:def 7;

then lim ((s1 - s2) * Ns1) = 0. S by A30, LOPBAN_3:8;

then A37: lim (q1 - ((s1 - s2) * Ns1)) = (lim q1) - (0. S) by A15, A31, NORMSP_1:26

.= lim q1 by RLVECT_1:13 ;

then A38: (f | Y) /* (q1 - ((s1 - s2) * Ns1)) is convergent by A18, A32, A23, NFCONT_1:def 5;

then A39: ((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) is convergent by A36, NORMSP_1:20;

(f | Y) /. (lim q1) = lim ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) by A18, A32, A37, A23, NFCONT_1:def 5;

then A40: lim (((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) = ((f | Y) /. (lim q1)) - ((f | Y) /. (lim q1)) by A36, A35, A38, NORMSP_1:26

.= 0. T by RLVECT_1:15 ;

for Y being Subset of S st Y is compact & f is_continuous_on Y holds

f is_uniformly_continuous_on Y

let f be PartFunc of S,T; :: thesis: for Y being Subset of S st Y is compact & f is_continuous_on Y holds

f is_uniformly_continuous_on Y

let Y be Subset of S; :: thesis: ( Y is compact & f is_continuous_on Y implies f is_uniformly_continuous_on Y )

assume that

A1: Y is compact and

A2: f is_continuous_on Y ; :: thesis: f is_uniformly_continuous_on Y

A3: Y c= dom f by A2, NFCONT_1:def 7;

assume not f is_uniformly_continuous_on Y ; :: thesis: contradiction

then consider r being Real such that

A4: 0 < r and

A5: for s being Real st 0 < s holds

ex x1, x2 being Point of S st

( x1 in Y & x2 in Y & ||.(x1 - x2).|| < s & not ||.((f /. x1) - (f /. x2)).|| < r ) by A3;

defpred S

( x2 in Y & ||.($2 - x2).|| < 1 / ($1 + 1) & not ||.((f /. $2) - (f /. x2)).|| < r ) );

A6: for n being Nat holds 0 < 1 / (n + 1) by XREAL_1:139;

A7: now :: thesis: for n being Element of NAT ex x1 being Point of S st S_{1}[n,x1]

consider s1 being sequence of S such that let n be Element of NAT ; :: thesis: ex x1 being Point of S st S_{1}[n,x1]

consider x1 being Point of S such that

A8: ex x2 being Point of S st

( x1 in Y & x2 in Y & ||.(x1 - x2).|| < 1 / (n + 1) & not ||.((f /. x1) - (f /. x2)).|| < r ) by A5, A6;

take x1 = x1; :: thesis: S_{1}[n,x1]

thus S_{1}[n,x1]
by A8; :: thesis: verum

end;consider x1 being Point of S such that

A8: ex x2 being Point of S st

( x1 in Y & x2 in Y & ||.(x1 - x2).|| < 1 / (n + 1) & not ||.((f /. x1) - (f /. x2)).|| < r ) by A5, A6;

take x1 = x1; :: thesis: S

thus S

A9: for n being Element of NAT holds S

defpred S

A10: for n being Element of NAT ex x2 being Point of S st S

consider s2 being sequence of S such that

A11: for n being Element of NAT holds S

now :: thesis: for x being object st x in rng s1 holds

x in Y

then A13:
rng s1 c= Y
by TARSKI:def 3;x in Y

let x be object ; :: thesis: ( x in rng s1 implies x in Y )

assume x in rng s1 ; :: thesis: x in Y

then consider n being Nat such that

A12: x = s1 . n by NFCONT_1:6;

n in NAT by ORDINAL1:def 12;

hence x in Y by A9, A12; :: thesis: verum

end;assume x in rng s1 ; :: thesis: x in Y

then consider n being Nat such that

A12: x = s1 . n by NFCONT_1:6;

n in NAT by ORDINAL1:def 12;

hence x in Y by A9, A12; :: thesis: verum

then consider q1 being sequence of S such that

A14: q1 is subsequence of s1 and

A15: q1 is convergent and

A16: lim q1 in Y by A1, NFCONT_1:def 2;

consider Ns1 being increasing sequence of NAT such that

A17: q1 = s1 * Ns1 by A14, VALUED_0:def 17;

set q2 = q1 - ((s1 - s2) * Ns1);

A18: f | Y is_continuous_in lim q1 by A2, A16, NFCONT_1:def 7;

now :: thesis: for x being object st x in rng s2 holds

x in Y

then A20:
rng s2 c= Y
by TARSKI:def 3;x in Y

let x be object ; :: thesis: ( x in rng s2 implies x in Y )

assume x in rng s2 ; :: thesis: x in Y

then consider n being Nat such that

A19: x = s2 . n by NFCONT_1:6;

n in NAT by ORDINAL1:def 12;

hence x in Y by A11, A19; :: thesis: verum

end;assume x in rng s2 ; :: thesis: x in Y

then consider n being Nat such that

A19: x = s2 . n by NFCONT_1:6;

n in NAT by ORDINAL1:def 12;

hence x in Y by A11, A19; :: thesis: verum

now :: thesis: for n being Element of NAT holds (q1 - ((s1 - s2) * Ns1)) . n = (s2 * Ns1) . n

then A21:
q1 - ((s1 - s2) * Ns1) = s2 * Ns1
by FUNCT_2:63;let n be Element of NAT ; :: thesis: (q1 - ((s1 - s2) * Ns1)) . n = (s2 * Ns1) . n

thus (q1 - ((s1 - s2) * Ns1)) . n = ((s1 * Ns1) . n) - (((s1 - s2) * Ns1) . n) by A17, NORMSP_1:def 3

.= (s1 . (Ns1 . n)) - (((s1 - s2) * Ns1) . n) by FUNCT_2:15

.= (s1 . (Ns1 . n)) - ((s1 - s2) . (Ns1 . n)) by FUNCT_2:15

.= (s1 . (Ns1 . n)) - ((s1 . (Ns1 . n)) - (s2 . (Ns1 . n))) by NORMSP_1:def 3

.= ((s1 . (Ns1 . n)) - (s1 . (Ns1 . n))) + (s2 . (Ns1 . n)) by RLVECT_1:29

.= (0. S) + (s2 . (Ns1 . n)) by RLVECT_1:15

.= s2 . (Ns1 . n) by RLVECT_1:4

.= (s2 * Ns1) . n by FUNCT_2:15 ; :: thesis: verum

end;thus (q1 - ((s1 - s2) * Ns1)) . n = ((s1 * Ns1) . n) - (((s1 - s2) * Ns1) . n) by A17, NORMSP_1:def 3

.= (s1 . (Ns1 . n)) - (((s1 - s2) * Ns1) . n) by FUNCT_2:15

.= (s1 . (Ns1 . n)) - ((s1 - s2) . (Ns1 . n)) by FUNCT_2:15

.= (s1 . (Ns1 . n)) - ((s1 . (Ns1 . n)) - (s2 . (Ns1 . n))) by NORMSP_1:def 3

.= ((s1 . (Ns1 . n)) - (s1 . (Ns1 . n))) + (s2 . (Ns1 . n)) by RLVECT_1:29

.= (0. S) + (s2 . (Ns1 . n)) by RLVECT_1:15

.= s2 . (Ns1 . n) by RLVECT_1:4

.= (s2 * Ns1) . n by FUNCT_2:15 ; :: thesis: verum

then rng (q1 - ((s1 - s2) * Ns1)) c= rng s2 by VALUED_0:21;

then A22: rng (q1 - ((s1 - s2) * Ns1)) c= Y by A20, XBOOLE_1:1;

then rng (q1 - ((s1 - s2) * Ns1)) c= dom f by A3, XBOOLE_1:1;

then rng (q1 - ((s1 - s2) * Ns1)) c= (dom f) /\ Y by A22, XBOOLE_1:19;

then A23: rng (q1 - ((s1 - s2) * Ns1)) c= dom (f | Y) by RELAT_1:61;

A24: now :: thesis: for p being Real st 0 < p holds

ex k being Nat st

for m being Nat st k <= m holds

||.(((s1 - s2) . m) - (0. S)).|| < p

then A30:
s1 - s2 is convergent
by NORMSP_1:def 6;ex k being Nat st

for m being Nat st k <= m holds

||.(((s1 - s2) . m) - (0. S)).|| < p

let p be Real; :: thesis: ( 0 < p implies ex k being Nat st

for m being Nat st k <= m holds

||.(((s1 - s2) . m) - (0. S)).|| < p )

assume A25: 0 < p ; :: thesis: ex k being Nat st

for m being Nat st k <= m holds

||.(((s1 - s2) . m) - (0. S)).|| < p

consider k being Nat such that

A26: p " < k by SEQ_4:3;

take k = k; :: thesis: for m being Nat st k <= m holds

||.(((s1 - s2) . m) - (0. S)).|| < p

let m be Nat; :: thesis: ( k <= m implies ||.(((s1 - s2) . m) - (0. S)).|| < p )

A27: m in NAT by ORDINAL1:def 12;

assume k <= m ; :: thesis: ||.(((s1 - s2) . m) - (0. S)).|| < p

then k + 1 <= m + 1 by XREAL_1:6;

then 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118;

then A28: ||.((s1 . m) - (s2 . m)).|| < 1 / (k + 1) by A11, XXREAL_0:2, A27;

k < k + 1 by NAT_1:13;

then p " < k + 1 by A26, XXREAL_0:2;

then 1 / (k + 1) < 1 / (p ") by A25, XREAL_1:76;

then A29: 1 / (k + 1) < p by XCMPLX_1:216;

||.(((s1 - s2) . m) - (0. S)).|| = ||.(((s1 . m) - (s2 . m)) - (0. S)).|| by NORMSP_1:def 3

.= ||.((s1 . m) - (s2 . m)).|| by RLVECT_1:13 ;

hence ||.(((s1 - s2) . m) - (0. S)).|| < p by A29, A28, XXREAL_0:2; :: thesis: verum

end;for m being Nat st k <= m holds

||.(((s1 - s2) . m) - (0. S)).|| < p )

assume A25: 0 < p ; :: thesis: ex k being Nat st

for m being Nat st k <= m holds

||.(((s1 - s2) . m) - (0. S)).|| < p

consider k being Nat such that

A26: p " < k by SEQ_4:3;

take k = k; :: thesis: for m being Nat st k <= m holds

||.(((s1 - s2) . m) - (0. S)).|| < p

let m be Nat; :: thesis: ( k <= m implies ||.(((s1 - s2) . m) - (0. S)).|| < p )

A27: m in NAT by ORDINAL1:def 12;

assume k <= m ; :: thesis: ||.(((s1 - s2) . m) - (0. S)).|| < p

then k + 1 <= m + 1 by XREAL_1:6;

then 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118;

then A28: ||.((s1 . m) - (s2 . m)).|| < 1 / (k + 1) by A11, XXREAL_0:2, A27;

k < k + 1 by NAT_1:13;

then p " < k + 1 by A26, XXREAL_0:2;

then 1 / (k + 1) < 1 / (p ") by A25, XREAL_1:76;

then A29: 1 / (k + 1) < p by XCMPLX_1:216;

||.(((s1 - s2) . m) - (0. S)).|| = ||.(((s1 . m) - (s2 . m)) - (0. S)).|| by NORMSP_1:def 3

.= ||.((s1 . m) - (s2 . m)).|| by RLVECT_1:13 ;

hence ||.(((s1 - s2) . m) - (0. S)).|| < p by A29, A28, XXREAL_0:2; :: thesis: verum

then A31: (s1 - s2) * Ns1 is convergent by LOPBAN_3:7;

then A32: q1 - ((s1 - s2) * Ns1) is convergent by A15, NORMSP_1:20;

rng q1 c= rng s1 by A14, VALUED_0:21;

then A33: rng q1 c= Y by A13, XBOOLE_1:1;

then rng q1 c= dom f by A3, XBOOLE_1:1;

then rng q1 c= (dom f) /\ Y by A33, XBOOLE_1:19;

then A34: rng q1 c= dom (f | Y) by RELAT_1:61;

then A35: (f | Y) /. (lim q1) = lim ((f | Y) /* q1) by A15, A18, NFCONT_1:def 5;

A36: (f | Y) /* q1 is convergent by A15, A18, A34, NFCONT_1:def 5;

lim (s1 - s2) = 0. S by A24, A30, NORMSP_1:def 7;

then lim ((s1 - s2) * Ns1) = 0. S by A30, LOPBAN_3:8;

then A37: lim (q1 - ((s1 - s2) * Ns1)) = (lim q1) - (0. S) by A15, A31, NORMSP_1:26

.= lim q1 by RLVECT_1:13 ;

then A38: (f | Y) /* (q1 - ((s1 - s2) * Ns1)) is convergent by A18, A32, A23, NFCONT_1:def 5;

then A39: ((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) is convergent by A36, NORMSP_1:20;

(f | Y) /. (lim q1) = lim ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) by A18, A32, A37, A23, NFCONT_1:def 5;

then A40: lim (((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) = ((f | Y) /. (lim q1)) - ((f | Y) /. (lim q1)) by A36, A35, A38, NORMSP_1:26

.= 0. T by RLVECT_1:15 ;

now :: thesis: for n being Nat holds contradiction

hence
contradiction
; :: thesis: verumlet n be Nat; :: thesis: contradiction

reconsider r = r as Real ;

consider k being Nat such that

A41: for m being Nat st k <= m holds

||.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . m) - (0. T)).|| < r by A4, A39, A40, NORMSP_1:def 7;

A42: k in NAT by ORDINAL1:def 12;

A43: q1 . k in rng q1 by NFCONT_1:6;

A44: (q1 - ((s1 - s2) * Ns1)) . k in rng (q1 - ((s1 - s2) * Ns1)) by NFCONT_1:6;

||.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k) - (0. T)).|| = ||.((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k).|| by RLVECT_1:13

.= ||.((((f | Y) /* q1) . k) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)).|| by NORMSP_1:def 3

.= ||.(((f | Y) /. (q1 . k)) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)).|| by A34, FUNCT_2:109, A42

.= ||.(((f | Y) /. (q1 . k)) - ((f | Y) /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A23, FUNCT_2:109, A42

.= ||.((f /. (q1 . k)) - ((f | Y) /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A34, A43, PARTFUN2:15

.= ||.((f /. (q1 . k)) - (f /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A23, A44, PARTFUN2:15

.= ||.((f /. (s1 . (Ns1 . k))) - (f /. ((s2 * Ns1) . k))).|| by A17, A21, FUNCT_2:15, A42

.= ||.((f /. (s1 . (Ns1 . k))) - (f /. (s2 . (Ns1 . k)))).|| by FUNCT_2:15, A42 ;

hence contradiction by A11, A41; :: thesis: verum

end;reconsider r = r as Real ;

consider k being Nat such that

A41: for m being Nat st k <= m holds

||.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . m) - (0. T)).|| < r by A4, A39, A40, NORMSP_1:def 7;

A42: k in NAT by ORDINAL1:def 12;

A43: q1 . k in rng q1 by NFCONT_1:6;

A44: (q1 - ((s1 - s2) * Ns1)) . k in rng (q1 - ((s1 - s2) * Ns1)) by NFCONT_1:6;

||.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k) - (0. T)).|| = ||.((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k).|| by RLVECT_1:13

.= ||.((((f | Y) /* q1) . k) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)).|| by NORMSP_1:def 3

.= ||.(((f | Y) /. (q1 . k)) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)).|| by A34, FUNCT_2:109, A42

.= ||.(((f | Y) /. (q1 . k)) - ((f | Y) /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A23, FUNCT_2:109, A42

.= ||.((f /. (q1 . k)) - ((f | Y) /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A34, A43, PARTFUN2:15

.= ||.((f /. (q1 . k)) - (f /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A23, A44, PARTFUN2:15

.= ||.((f /. (s1 . (Ns1 . k))) - (f /. ((s2 * Ns1) . k))).|| by A17, A21, FUNCT_2:15, A42

.= ||.((f /. (s1 . (Ns1 . k))) - (f /. (s2 . (Ns1 . k)))).|| by FUNCT_2:15, A42 ;

hence contradiction by A11, A41; :: thesis: verum