let X be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of X
for Z being Subset of REAL st Z c= dom f & Z is compact & f | Z is continuous holds
f | Z is uniformly_continuous
let f be PartFunc of REAL, the carrier of X; :: thesis: for Z being Subset of REAL st Z c= dom f & Z is compact & f | Z is continuous holds
f | Z is uniformly_continuous
let Z be Subset of REAL; :: thesis: ( Z c= dom f & Z is compact & f | Z is continuous implies f | Z is uniformly_continuous )
assume that
A1: Z c= dom f and
A2: Z is compact and
A3: f | Z is continuous ; :: thesis: f | Z is uniformly_continuous
assume not f | Z is uniformly_continuous ; :: 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 Real st
( x1 in dom (f | Z) & x2 in dom (f | Z) & |.(x1 - x2).| < s & not ||.((f /. x1) - (f /. x2)).|| < r ) by Th1;
defpred S1[ Element of NAT , Real] means ( $2 in Z & ex x2 being Element of REAL st
( x2 in Z & |.($2 - x2).| < 1 / ($1 + 1) & not ||.((f /. $2) - (f /. x2)).|| < r ) );
A6: now :: thesis: for n being Element of NAT ex x1 being Element of REAL st S1[n,x1]
let n be Element of NAT ; :: thesis: ex x1 being Element of REAL st S1[n,x1]
consider x1 being Real such that
A7: ex x2 being Real st
( x1 in dom (f | Z) & x2 in dom (f | Z) & |.(x1 - x2).| < 1 / (n + 1) & not ||.((f /. x1) - (f /. x2)).|| < r ) by A5;
reconsider x1 = x1 as Element of REAL by XREAL_0:def 1;
take x1 = x1; :: thesis: S1[n,x1]
dom (f | Z) = Z by A1, RELAT_1:62;
hence S1[n,x1] by A7; :: thesis: verum
end;
consider s1 being Real_Sequence such that
A8: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch 3(A6);
A9: now :: thesis: for x being object st x in rng s1 holds
x in Z
let x be object ; :: thesis: ( x in rng s1 implies x in Z )
assume x in rng s1 ; :: thesis: x in Z
then ex n being Element of NAT st x = s1 . n by FUNCT_2:113;
hence x in Z by A8; :: thesis: verum
end;
then rng s1 c= Z ;
then consider q1 being Real_Sequence such that
A10: ( q1 is subsequence of s1 & q1 is convergent & lim q1 in Z ) by A2;
A11: f | Z is_continuous_in lim q1 by A3, A1, A10, RELAT_1:57;
rng q1 c= rng s1 by A10, VALUED_0:21;
then ( rng q1 c= Z & rng q1 c= dom f ) by A1, A9;
then rng q1 c= (dom f) /\ Z by XBOOLE_1:19;
then A12: rng q1 c= dom (f | Z) by RELAT_1:61;
then A13: ( (f | Z) /. (lim q1) = lim ((f | Z) /* q1) & (f | Z) /* q1 is convergent ) by A10, A11;
defpred S2[ Element of NAT , Real] means ( $2 in Z & |.((s1 . $1) - $2).| < 1 / ($1 + 1) & not ||.((f /. (s1 . $1)) - (f /. $2)).|| < r );
A14: for n being Element of NAT ex x2 being Element of REAL st S2[n,x2] by A8;
consider s2 being Real_Sequence such that
A15: for n being Element of NAT holds S2[n,s2 . n] from FUNCT_2:sch 3(A14);
A16: now :: thesis: for x being object st x in rng s2 holds
x in Z
let x be object ; :: thesis: ( x in rng s2 implies x in Z )
assume x in rng s2 ; :: thesis: x in Z
then ex n being Element of NAT st x = s2 . n by FUNCT_2:113;
hence x in Z by A15; :: thesis: verum
end;
consider Ns1 being increasing sequence of NAT such that
A17: q1 = s1 * Ns1 by A10, VALUED_0:def 17;
set q2 = q1 - ((s1 - s2) * Ns1);
now :: thesis: for n being Element of NAT holds (q1 - ((s1 - s2) * Ns1)) . n = (s2 * Ns1) . n
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, RFUNCT_2:1
.= (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 RFUNCT_2:1
.= (s2 * Ns1) . n by FUNCT_2:15 ; :: thesis: verum
end;
then A18: ( q1 - ((s1 - s2) * Ns1) = s2 * Ns1 & q1 - ((s1 - s2) * Ns1) is subsequence of s2 ) by FUNCT_2:63;
then rng (q1 - ((s1 - s2) * Ns1)) c= rng s2 by VALUED_0:21;
then ( rng (q1 - ((s1 - s2) * Ns1)) c= Z & rng (q1 - ((s1 - s2) * Ns1)) c= dom f ) by A1, A16;
then rng (q1 - ((s1 - s2) * Ns1)) c= (dom f) /\ Z by XBOOLE_1:19;
then A19: rng (q1 - ((s1 - s2) * Ns1)) c= dom (f | Z) by RELAT_1:61;
A20: 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).| < 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).| < p )
assume A21: 0 < p ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
|.(((s1 - s2) . m) - 0).| < p
consider k being Nat such that
A22: p " < k by SEQ_4:3;
take k = k; :: thesis: for m being Nat st k <= m holds
|.(((s1 - s2) . m) - 0).| < p
let m be Nat; :: thesis: ( k <= m implies |.(((s1 - s2) . m) - 0).| < p )
A23: m in NAT by ORDINAL1:def 12;
assume k <= m ; :: thesis: |.(((s1 - s2) . m) - 0).| < p
then k + 1 <= m + 1 by XREAL_1:6;
then 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118;
then A24: |.((s1 . m) - (s2 . m)).| < 1 / (k + 1) by A15, XXREAL_0:2, A23;
k < k + 1 by NAT_1:13;
then p " < k + 1 by A22, XXREAL_0:2;
then A25: 1 / (k + 1) < 1 / (p ") by A21, XREAL_1:76;
|.(((s1 - s2) . m) - 0).| = |.((s1 . m) - (s2 . m)).| by RFUNCT_2:1;
hence |.(((s1 - s2) . m) - 0).| < p by A25, A24, XXREAL_0:2; :: thesis: verum
end;
then A26: s1 - s2 is convergent by SEQ_2:def 6;
A27: (s1 - s2) * Ns1 is convergent by A20, SEQ_2:def 6, SEQ_4:16;
then A28: q1 - ((s1 - s2) * Ns1) is convergent by A10, SEQ_2:11;
lim (s1 - s2) = 0 by A20, A26, SEQ_2:def 7;
then lim ((s1 - s2) * Ns1) = 0 by A20, SEQ_2:def 6, SEQ_4:17;
then lim (q1 - ((s1 - s2) * Ns1)) = (lim q1) - 0 by A10, A27, SEQ_2:12;
then A29: ( (f | Z) /* (q1 - ((s1 - s2) * Ns1)) is convergent & (f | Z) /. (lim q1) = lim ((f | Z) /* (q1 - ((s1 - s2) * Ns1))) ) by A11, A28, A19;
then A30: ((f | Z) /* q1) - ((f | Z) /* (q1 - ((s1 - s2) * Ns1))) is convergent by A13, NORMSP_1:20;
lim (((f | Z) /* q1) - ((f | Z) /* (q1 - ((s1 - s2) * Ns1)))) = ((f | Z) /. (lim q1)) - ((f | Z) /. (lim q1)) by A13, A29, NORMSP_1:26;
then A31: lim (((f | Z) /* q1) - ((f | Z) /* (q1 - ((s1 - s2) * Ns1)))) = 0. X by RLVECT_1:15;
now :: thesis: for n being Nat holds contradiction
let n be Nat; :: thesis: contradiction
consider k being Nat such that
A32: for m being Nat st k <= m holds
||.(((((f | Z) /* q1) - ((f | Z) /* (q1 - ((s1 - s2) * Ns1)))) . m) - (0. X)).|| < r by A4, A30, A31, NORMSP_1:def 7;
A33: ( q1 . k in dom (f | Z) & (q1 - ((s1 - s2) * Ns1)) . k in dom (f | Z) ) by A12, A19, VALUED_0:28;
A34: k in NAT by ORDINAL1:def 12;
A35: ||.(((((f | Z) /* q1) - ((f | Z) /* (q1 - ((s1 - s2) * Ns1)))) . k) - (0. X)).|| = ||.((((f | Z) /* q1) . k) - (((f | Z) /* (q1 - ((s1 - s2) * Ns1))) . k)).|| by NORMSP_1:def 3;
( ((f | Z) /* q1) . k = (f | Z) /. (q1 . k) & ((f | Z) /* (q1 - ((s1 - s2) * Ns1))) . k = (f | Z) /. ((q1 - ((s1 - s2) * Ns1)) . k) ) by A12, A19, FUNCT_2:109, A34;
then ( ((f | Z) /* q1) . k = f /. (q1 . k) & ((f | Z) /* (q1 - ((s1 - s2) * Ns1))) . k = f /. ((q1 - ((s1 - s2) * Ns1)) . k) ) by A33, PARTFUN1:80;
then ||.((((f | Z) /* q1) . k) - (((f | Z) /* (q1 - ((s1 - s2) * Ns1))) . k)).|| = ||.((f /. (s1 . (Ns1 . k))) - (f /. ((s2 * Ns1) . k))).|| by A17, A18, FUNCT_2:15, ORDINAL1:def 12
.= ||.((f /. (s1 . (Ns1 . k))) - (f /. (s2 . (Ns1 . k)))).|| by FUNCT_2:15, ORDINAL1:def 12 ;
hence contradiction by A15, A32, A35; :: thesis: verum
end;
hence contradiction ; :: thesis: verum