let RNS be RealNormSpace; for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS
for Y being Subset of RNS st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
let CNS be ComplexNormSpace; for f being PartFunc of RNS,CNS
for Y being Subset of RNS st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
let f be PartFunc of RNS,CNS; for Y being Subset of RNS st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y
let Y be Subset of RNS; ( 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
; f is_uniformly_continuous_on Y
A3:
Y c= dom f
by A2, NCFCONT1:def 13;
assume
not f is_uniformly_continuous_on Y
; 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 RNS 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 RNS] means ( $2 in Y & ex x2 being Point of RNS st
( x2 in Y & ||.($2 - x2).|| < 1 / ($1 + 1) & not ||.((f /. $2) - (f /. x2)).|| < r ) );
consider s1 being sequence of RNS 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 RNS] 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 RNS st S2[n,x2]
by A8;
consider s2 being sequence of RNS 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]
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 RNS 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 V43() 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 13;
then A20:
rng s2 c= Y
by TARSKI:def 3;
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;
then A29:
s1 - s2 is convergent
by NORMSP_1:def 6;
then A30:
(s1 - s2) * Ns1 is convergent
by LOPBAN_3:7;
then A31:
q1 - ((s1 - s2) * Ns1) is convergent
by A15, NORMSP_1:20;
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 7;
A35:
(f | Y) /* q1 is convergent
by A15, A18, A33, NCFCONT1:def 7;
lim (s1 - s2) = 0. RNS
by A24, A29, NORMSP_1:def 7;
then
lim ((s1 - s2) * Ns1) = 0. RNS
by A29, LOPBAN_3:8;
then A36: lim (q1 - ((s1 - s2) * Ns1)) =
(lim q1) - (0. RNS)
by A15, A30, NORMSP_1:26
.=
lim q1
by RLVECT_1:13
;
then A37:
(f | Y) /* (q1 - ((s1 - s2) * Ns1)) is convergent
by A18, A31, A23, NCFCONT1:def 7;
then A38:
((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) is convergent
by A35, CLVECT_1:114;
(f | Y) /. (lim q1) = lim ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))
by A18, A31, A36, A23, NCFCONT1:def 7;
then A39: lim (((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) =
((f | Y) /. (lim q1)) - ((f | Y) /. (lim q1))
by A35, A34, A37, CLVECT_1:120
.=
0. CNS
by RLVECT_1:15
;
now for n being Element of NAT holds contradictionlet n be
Element of
NAT ;
contradictionconsider 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. CNS)).|| < r
by A4, A38, A39, CLVECT_1:def 16;
A41:
q1 . k in rng q1
by NFCONT_1:6;
A42:
(q1 - ((s1 - s2) * Ns1)) . k in rng (q1 - ((s1 - s2) * Ns1))
by NFCONT_1:6;
A43:
k in NAT
by ORDINAL1:def 12;
||.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k) - (0. CNS)).|| =
||.((((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, A43
.=
||.(((f | Y) /. (q1 . k)) - ((f | Y) /. ((q1 - ((s1 - s2) * Ns1)) . k))).||
by A23, FUNCT_2:109, A43
.=
||.((f /. (q1 . k)) - ((f | Y) /. ((q1 - ((s1 - s2) * Ns1)) . k))).||
by A33, A41, PARTFUN2:15
.=
||.((f /. (q1 . k)) - (f /. ((q1 - ((s1 - s2) * Ns1)) . k))).||
by A23, A42, PARTFUN2:15
.=
||.((f /. (s1 . (Ns1 . k))) - (f /. ((s2 * Ns1) . k))).||
by A17, A21, FUNCT_2:15, A43
.=
||.((f /. (s1 . (Ns1 . k))) - (f /. (s2 . (Ns1 . k)))).||
by FUNCT_2:15, A43
;
hence
contradiction
by A11, A40;
verum end;
hence
contradiction
; verum