let RNS be RealNormSpace; :: thesis: for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS
for Y being Subset of CNS st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
let CNS be ComplexNormSpace; :: thesis: for f being PartFunc of CNS,RNS
for Y being Subset of CNS st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
let f be PartFunc of CNS,RNS; :: thesis: for Y being Subset of CNS st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
let Y be Subset of CNS; :: 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, NCFCONT1:def 12;
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 CNS st
( x1 in Y & x2 in Y & ||.(x1 - x2).|| < s & not ||.((f /. x1) - (f /. x2)).|| < r ) by A3;
defpred S1[ Element of NAT , Point of CNS] means ( $2 in Y & ex x2 being Point of CNS st
( x2 in Y & ||.($2 - x2).|| < 1 / ($1 + 1) & not ||.((f /. $2) - (f /. x2)).|| < r ) );
A6: now :: thesis: for n being Element of NAT ex x1 being Point of CNS st S1[n,x1]
let n be Element of NAT ; :: thesis: ex x1 being Point of CNS st S1[n,x1]
consider x1 being Point of CNS such that
A7: ex x2 being Point of CNS st
( x1 in Y & x2 in Y & ||.(x1 - x2).|| < 1 / (n + 1) & not ||.((f /. x1) - (f /. x2)).|| < r ) by A5;
take x1 = x1; :: thesis: S1[n,x1]
thus S1[n,x1] by A7; :: thesis: verum
end;
consider s1 being sequence of CNS such that
A8: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch 3(A6);
 defpred S2[ Nat, Point of CNS] means ( $2 in Y & ||.((s1 . $1) - $2).|| < 1 / ($1 + 1) & not ||.((f /. (s1 . $1)) - (f /. $2)).|| < r );
A9: for n being Element of NAT ex x2 being Point of CNS st S2[n,x2] by A8;
consider s2 being sequence of CNS such that
A10: for n being Element of NAT holds S2[n,s2 . n] from FUNCT_2:sch 3(A9);
 A11: for n being Nat holds S2[n,s2 . n]
proof
let n be Nat; :: thesis: S2[n,s2 . n]
n in NAT by ORDINAL1:def 12;
hence S2[n,s2 . n] by A10; :: thesis: verum
end;
now :: thesis: for x being Point of CNS st x in rng s1 holds
x in Y
let x be Point of CNS; :: 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 NCFCONT1:7;
n in NAT by ORDINAL1:def 12;
hence x in Y by A8, A12; :: thesis: verum
end;
then for x being object st x in rng s1 holds
x in Y ;
then A13: rng s1 c= Y by TARSKI:def 3;
then consider q1 being sequence of CNS such that
A14: q1 is subsequence of s1 and
A15: q1 is convergent and
A16: lim q1 in Y by A1, NCFCONT1: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, NCFCONT1:def 12;
now :: thesis: for x being object st x in rng s2 holds
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 NCFCONT1:7;
thus x in Y by A11, A19; :: thesis: verum
end;
then A20: rng s2 c= Y by TARSKI:def 3;
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, 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. CNS) + (s2 . (Ns1 . n)) by RLVECT_1:15
.= s2 . (Ns1 . n) by RLVECT_1:4
.= (s2 * Ns1) . n by FUNCT_2:15 ; :: thesis: verum
end;
then A21: q1 - ((s1 - s2) * Ns1) = s2 * Ns1 by FUNCT_2:63;
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. CNS)).|| < 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. CNS)).|| < p )
assume A25: 0 < p ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
||.(((s1 - s2) . m) - (0. CNS)).|| < 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. CNS)).|| < p
let m be Nat; :: thesis: ( k <= m implies ||.(((s1 - s2) . m) - (0. CNS)).|| < p )
assume k <= m ; :: thesis: ||.(((s1 - s2) . m) - (0. CNS)).|| < p
then k + 1 <= m + 1 by XREAL_1:6;
then 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118;
then A27: ||.((s1 . m) - (s2 . m)).|| < 1 / (k + 1) by A11, XXREAL_0:2;
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 A28: 1 / (k + 1) < p by XCMPLX_1:216;
||.(((s1 - s2) . m) - (0. CNS)).|| = ||.(((s1 . m) - (s2 . m)) - (0. CNS)).|| by NORMSP_1:def 3
.= ||.((s1 . m) - (s2 . m)).|| by RLVECT_1:13 ;
hence ||.(((s1 - s2) . m) - (0. CNS)).|| < p by A28, A27, XXREAL_0:2; :: thesis: verum
end;
then A29: s1 - s2 is convergent by CLVECT_1:def 15;
then A30: (s1 - s2) * Ns1 is convergent by CLOPBAN3:7;
then A31: q1 - ((s1 - s2) * Ns1) is convergent by A15, CLVECT_1:114;
rng q1 c= rng s1 by A14, VALUED_0:21;
then A32: 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 A32, XBOOLE_1:19;
then A33: rng q1 c= dom (f | Y) by RELAT_1:61;
then A34: (f | Y) /. (lim q1) = lim ((f | Y) /* q1) by A15, A18, NCFCONT1:def 6;
A35: (f | Y) /* q1 is convergent by A15, A18, A33, NCFCONT1:def 6;
lim (s1 - s2) = 0. CNS by A24, A29, CLVECT_1:def 16;
then lim ((s1 - s2) * Ns1) = 0. CNS by A29, CLOPBAN3:8;
then A36: lim (q1 - ((s1 - s2) * Ns1)) = (lim q1) - (0. CNS) by A15, A30, CLVECT_1:120
.= lim q1 by RLVECT_1:13 ;
then A37: (f | Y) /* (q1 - ((s1 - s2) * Ns1)) is convergent by A18, A31, A23, NCFCONT1:def 6;
then A38: ((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) is convergent by A35, NORMSP_1:20;
(f | Y) /. (lim q1) = lim ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) by A18, A31, A36, A23, NCFCONT1:def 6;
then A39: lim (((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) = ((f | Y) /. (lim q1)) - ((f | Y) /. (lim q1)) by A35, A34, A37, NORMSP_1:26
.= 0. RNS by RLVECT_1:15 ;
now :: thesis: for n being Element of NAT holds contradiction
let n be Element of NAT ; :: thesis: contradiction
consider k being Nat such that
A40: for m being Nat st k <= m holds
||.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . m) - (0. RNS)).|| < r by A4, A38, A39, NORMSP_1:def 7;
A41: k in NAT by ORDINAL1:def 12;
A42: q1 . k in rng q1 by NCFCONT1:7;
A43: (q1 - ((s1 - s2) * Ns1)) . k in rng (q1 - ((s1 - s2) * Ns1)) by NCFCONT1:7;
||.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k) - (0. RNS)).|| = ||.((((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 A33, FUNCT_2:109, A41
.= ||.(((f | Y) /. (q1 . k)) - ((f | Y) /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A23, FUNCT_2:109, A41
.= ||.((f /. (q1 . k)) - ((f | Y) /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A33, A42, PARTFUN2:15
.= ||.((f /. (q1 . k)) - (f /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A23, A43, PARTFUN2:15
.= ||.((f /. (s1 . (Ns1 . k))) - (f /. ((s2 * Ns1) . k))).|| by A17, A21, FUNCT_2:15, A41
.= ||.((f /. (s1 . (Ns1 . k))) - (f /. (s2 . (Ns1 . k)))).|| by FUNCT_2:15, A41 ;
hence contradiction by A11, A40; :: thesis: verum
end;
hence contradiction ; :: thesis: verum