:: Uniform Continuity of Functions on Normed Complex Linear Spaces
:: by Noboru Endou
::
:: Received October 6, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, XCMPLX_0, NORMSP_1, CLVECT_1, PARTFUN1,
NFCONT_2, TARSKI, RELAT_1, CARD_1, ARYTM_3, PRE_TOPC, ARYTM_1, STRUCT_0,
COMPLEX1, XBOOLE_0, XXREAL_0, VALUED_1, SUPINF_2, FUNCT_1, CFCONT_1,
NFCONT_1, SUBSET_1, RCOMP_1, NAT_1, VALUED_0, SEQ_2, ORDINAL2, FCONT_1,
FUNCT_2, SEQ_4, CLOPBAN1, ALI2, FUNCOP_1, POWER, RSSPACE3, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
COMPLEX1, XREAL_0, REAL_1, NAT_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, PRE_TOPC, VALUED_0, STRUCT_0, RLVECT_1, FUNCOP_1, VALUED_1,
SEQ_2, SEQ_4, FUNCT_7, VFUNCT_1, POWER, VFUNCT_2, NORMSP_0, NORMSP_1,
CLVECT_1, NFCONT_1, CLOPBAN1, NFCONT_2, NCFCONT1, CSSPACE3;
constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_2, SEQ_4, POWER, FUNCT_7,
CSSPACE3, NFCONT_1, NFCONT_2, CLOPBAN3, VFUNCT_2, NCFCONT1, RELSET_1,
COMSEQ_2;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0,
MEMBERED, STRUCT_0, VALUED_1, FUNCT_2, NUMBERS, VALUED_0, FUNCT_7,
CLVECT_1, XCMPLX_0, NAT_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RLVECT_1;
theorems TARSKI, ABSVALUE, XBOOLE_1, RLVECT_1, XCMPLX_1, SEQ_2, NAT_1,
RELAT_1, VFUNCT_1, FUNCT_2, SEQ_4, NORMSP_1, LOPBAN_3, PARTFUN2,
CLVECT_1, CLOPBAN3, VFUNCT_2, NFCONT_1, CLOPBAN1, COMPLEX1, NCFCONT1,
NFCONT_2, FUNCOP_1, POWER, CSSPACE3, FUNCT_7, SEQ_1, XREAL_1, XXREAL_0,
ORDINAL1, PARTFUN1, VALUED_0, NORMSP_0;
schemes FUNCT_2, NAT_1;
begin :: Uniform Continuity of Functions on Real and Complex Normed Linear Spaces
reserve X,X1 for set,
r,s for Real,
z for Complex,
RNS for RealNormSpace,
CNS, CNS1,CNS2 for ComplexNormSpace;
definition
let X be set;
let CNS1,CNS2 be ComplexNormSpace;
let f be PartFunc of CNS1,CNS2;
pred f is_uniformly_continuous_on X means
X c= dom f & for r st 0 < r
ex s st 0 < s & for x1,x2 be Point of CNS1 st x1 in X & x2 in X & ||.x1 - x2.||
< s holds ||. f/.x1 - f/.x2 .|| < r;
end;
definition
let X be set;
let RNS be RealNormSpace;
let CNS be ComplexNormSpace;
let f be PartFunc of CNS,RNS;
pred f is_uniformly_continuous_on X means
X c= dom f & for r st 0 < r
ex s st 0 < s & for x1,x2 be Point of CNS st x1 in X & x2 in X & ||.x1 - x2.||
< s holds ||. f/.x1 - f/.x2 .|| < r;
end;
definition
let X be set;
let RNS be RealNormSpace;
let CNS be ComplexNormSpace;
let f be PartFunc of RNS,CNS;
pred f is_uniformly_continuous_on X means
X c= dom f & for r st 0 < r
ex s st 0 < s & for x1,x2 be Point of RNS st x1 in X & x2 in X & ||.x1 - x2.||
< s holds ||. f/.x1 - f/.x2 .|| < r;
end;
definition
let X be set;
let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS,COMPLEX;
pred f is_uniformly_continuous_on X means
X c= dom f & for r st 0 < r
ex s st 0 < s & for x1,x2 be Point of CNS st x1 in X & x2 in X & ||.x1 - x2.||
< s holds |.(f/.x1 - f/.x2).| < r;
end;
definition
let X be set;
let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS,REAL;
pred f is_uniformly_continuous_on X means
X c= dom f & for r st 0 < r
ex s st 0 < s & for x1,x2 be Point of CNS st x1 in X & x2 in X & ||.x1 - x2.||
< s holds |.f/.x1 - f/.x2.| < r;
end;
definition
let X be set;
let RNS be RealNormSpace;
let f be PartFunc of the carrier of RNS,COMPLEX;
pred f is_uniformly_continuous_on X means
X c= dom f & for r st 0 < r
ex s st 0 < s & for x1,x2 be Point of RNS st x1 in X & x2 in X & ||.x1 - x2.||
< s holds |.(f/.x1 - f/.x2).| < r;
end;
theorem Th1:
for f be PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X
& X1 c= X holds f is_uniformly_continuous_on X1
proof
let f be PartFunc of CNS1,CNS2;
assume that
A1: f is_uniformly_continuous_on X and
A2: X1 c= X;
X c= dom f by A1;
hence X1 c= dom f by A2,XBOOLE_1:1;
let r;
assume 0 < r;
then consider s such that
A3: 0 < s and
A4: for x1,x2 be Point of CNS1 st x1 in X & x2 in X & ||.x1-x2.|| < s
holds ||.f/.x1-f/.x2.||<r by A1;
take s;
thus 0 < s by A3;
let x1,x2 be Point of CNS1;
assume x1 in X1 & x2 in X1 & ||.x1-x2.||<s;
hence thesis by A2,A4;
end;
theorem Th2:
for f be PartFunc of CNS,RNS st f is_uniformly_continuous_on X &
X1 c= X holds f is_uniformly_continuous_on X1
proof
let f be PartFunc of CNS,RNS;
assume that
A1: f is_uniformly_continuous_on X and
A2: X1 c= X;
X c= dom f by A1;
hence X1 c= dom f by A2,XBOOLE_1:1;
let r;
assume 0 < r;
then consider s such that
A3: 0 < s and
A4: for x1,x2 be Point of CNS st x1 in X & x2 in X & ||.x1-x2.|| < s
holds ||.f/.x1-f/.x2.||<r by A1;
take s;
thus 0 < s by A3;
let x1,x2 be Point of CNS;
assume x1 in X1 & x2 in X1 & ||.x1-x2.||<s;
hence thesis by A2,A4;
end;
theorem Th3:
for f be PartFunc of RNS,CNS st f is_uniformly_continuous_on X &
X1 c= X holds f is_uniformly_continuous_on X1
proof
let f be PartFunc of RNS,CNS;
assume that
A1: f is_uniformly_continuous_on X and
A2: X1 c= X;
X c= dom f by A1;
hence X1 c= dom f by A2,XBOOLE_1:1;
let r;
assume 0 < r;
then consider s such that
A3: 0 < s and
A4: for x1,x2 be Point of RNS st x1 in X & x2 in X & ||.x1-x2.|| < s
holds ||.f/.x1-f/.x2.||<r by A1;
take s;
thus 0 < s by A3;
let x1,x2 be Point of RNS;
assume x1 in X1 & x2 in X1 & ||.x1-x2.||<s;
hence thesis by A2,A4;
end;
theorem
for f1,f2 be PartFunc of CNS1,CNS2 st f1 is_uniformly_continuous_on X
& f2 is_uniformly_continuous_on X1 holds f1+f2 is_uniformly_continuous_on X/\X1
proof
let f1,f2 be PartFunc of CNS1,CNS2;
assume that
A1: f1 is_uniformly_continuous_on X and
A2: f2 is_uniformly_continuous_on X1;
A3: f2 is_uniformly_continuous_on X /\ X1 by A2,Th1,XBOOLE_1:17;
then
A4: X /\ X1 c= dom f2;
A5: f1 is_uniformly_continuous_on X /\ X1 by A1,Th1,XBOOLE_1:17;
then X /\ X1 c= dom f1;
then X /\ X1 c= dom f1 /\ dom f2 by A4,XBOOLE_1:19;
hence
A6: X /\ X1 c= dom (f1+f2) by VFUNCT_1:def 1;
let r;
assume 0 < r;
then
A7: 0<r/2;
then consider s such that
A8: 0<s and
A9: for x1,x2 be Point of CNS1 st x1 in X /\ X1 & x2 in X /\X1 & ||.x1-
x2.||<s holds ||.f1/.x1-f1/.x2.||<r/2 by A5;
consider g be Real such that
A10: 0<g and
A11: for x1,x2 be Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 & ||.x1
-x2.|| < g holds ||.f2/.x1-f2/.x2.|| < r/2 by A3,A7;
take p=min(s,g);
thus 0<p by A8,A10,XXREAL_0:15;
let x1,x2 be Point of CNS1;
assume that
A12: x1 in X/\X1 and
A13: x2 in X/\X1 and
A14: ||.x1-x2.||<p;
p <= g by XXREAL_0:17;
then ||.x1-x2.||<g by A14,XXREAL_0:2;
then
A15: ||.f2/.x1-f2/.x2.||<r/2 by A11,A12,A13;
p <= s by XXREAL_0:17;
then ||.x1-x2.||<s by A14,XXREAL_0:2;
then ||. f1/.x1 - f1/.x2 .|| < r/2 by A9,A12,A13;
then
A16: ||.f1/.x1-f1/.x2.||+||.f2/.x1-f2/.x2.||<r/2+r/2 by A15,XREAL_1:8;
A17: ||.f1/.x1 - f1/.x2 + (f2/.x1-f2/.x2).|| <= ||.f1/.x1-f1/.x2.|| + ||.f2
/.x1-f2/.x2.|| by CLVECT_1:def 13;
||.(f1+f2)/.x1-(f1+f2)/.x2.|| = ||.f1/.x1 + f2/.x1-(f1+f2)/.x2.|| by A6,A12,
VFUNCT_1:def 1
.= ||.f1/.x1 + f2/.x1 - (f1/.x2+f2/.x2).|| by A6,A13,VFUNCT_1:def 1
.= ||.f1/.x1 + (f2/.x1 - (f1/.x2+f2/.x2)).|| by RLVECT_1:def 3
.= ||.f1/.x1 + (f2/.x1 - f1/.x2-f2/.x2).|| by RLVECT_1:27
.= ||.f1/.x1 + (-f1/.x2 + f2/.x1-f2/.x2).||
.= ||.f1/.x1 + (-f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:def 3
.= ||.f1/.x1 - f1/.x2 + (f2/.x1-f2/.x2).|| by RLVECT_1:def 3;
hence thesis by A16,A17,XXREAL_0:2;
end;
theorem
for f1,f2 be PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X &
f2 is_uniformly_continuous_on X1 holds f1+f2 is_uniformly_continuous_on X/\X1
proof
let f1,f2 be PartFunc of CNS,RNS;
assume that
A1: f1 is_uniformly_continuous_on X and
A2: f2 is_uniformly_continuous_on X1;
A3: f2 is_uniformly_continuous_on X /\ X1 by A2,Th2,XBOOLE_1:17;
then
A4: X /\ X1 c= dom f2;
A5: f1 is_uniformly_continuous_on X /\ X1 by A1,Th2,XBOOLE_1:17;
then X /\ X1 c= dom f1;
then X /\ X1 c= dom f1 /\ dom f2 by A4,XBOOLE_1:19;
hence
A6: X /\ X1 c= dom (f1+f2) by VFUNCT_1:def 1;
let r;
assume 0 < r;
then
A7: 0<r/2;
then consider s such that
A8: 0<s and
A9: for x1,x2 be Point of CNS st x1 in X /\ X1 & x2 in X /\X1 & ||.x1-
x2.||<s holds ||.f1/.x1-f1/.x2.||<r/2 by A5;
consider g be Real such that
A10: 0<g and
A11: for x1,x2 be Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.x1-
x2.|| < g holds ||.f2/.x1-f2/.x2.|| < r/2 by A3,A7;
take p=min(s,g);
thus 0<p by A8,A10,XXREAL_0:15;
let x1,x2 be Point of CNS;
assume that
A12: x1 in X/\X1 and
A13: x2 in X/\X1 and
A14: ||.x1-x2.||<p;
p <= g by XXREAL_0:17;
then ||.x1-x2.||<g by A14,XXREAL_0:2;
then
A15: ||.f2/.x1-f2/.x2.||<r/2 by A11,A12,A13;
p <= s by XXREAL_0:17;
then ||.x1-x2.||<s by A14,XXREAL_0:2;
then ||.f1/.x1-f1/.x2.||<r/2 by A9,A12,A13;
then
A16: ||.f1/.x1-f1/.x2.||+||.f2/.x1-f2/.x2.||<r/2+r/2 by A15,XREAL_1:8;
A17: ||.f1/.x1 - f1/.x2 + (f2/.x1-f2/.x2).|| <= ||.f1/.x1-f1/.x2.|| + ||.f2
/.x1-f2/.x2.|| by NORMSP_1:def 1;
||.(f1+f2)/.x1-(f1+f2)/.x2.|| = ||.f1/.x1 + f2/.x1-(f1+f2)/.x2.|| by A6,A12,
VFUNCT_1:def 1
.= ||.f1/.x1 + f2/.x1 - (f1/.x2+f2/.x2).|| by A6,A13,VFUNCT_1:def 1
.= ||.f1/.x1 + (f2/.x1 - (f1/.x2+f2/.x2)).|| by RLVECT_1:def 3
.= ||.f1/.x1 + (f2/.x1 - f1/.x2-f2/.x2).|| by RLVECT_1:27
.= ||.f1/.x1 + (-f1/.x2 + f2/.x1-f2/.x2).||
.= ||.f1/.x1 + (-f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:def 3
.= ||.f1/.x1 - f1/.x2 + (f2/.x1-f2/.x2).|| by RLVECT_1:def 3;
hence thesis by A16,A17,XXREAL_0:2;
end;
theorem
for f1,f2 be PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X &
f2 is_uniformly_continuous_on X1 holds f1+f2 is_uniformly_continuous_on X/\X1
proof
let f1,f2 be PartFunc of RNS,CNS;
assume that
A1: f1 is_uniformly_continuous_on X and
A2: f2 is_uniformly_continuous_on X1;
A3: f2 is_uniformly_continuous_on X /\ X1 by A2,Th3,XBOOLE_1:17;
then
A4: X /\ X1 c= dom f2;
A5: f1 is_uniformly_continuous_on X /\ X1 by A1,Th3,XBOOLE_1:17;
then X /\ X1 c= dom f1;
then X /\ X1 c= dom f1 /\ dom f2 by A4,XBOOLE_1:19;
hence
A6: X /\ X1 c= dom (f1+f2) by VFUNCT_1:def 1;
let r;
assume 0 < r;
then
A7: 0<r/2;
then consider s such that
A8: 0<s and
A9: for x1,x2 be Point of RNS st x1 in X /\ X1 & x2 in X /\X1 & ||.x1-
x2.||<s holds ||.f1/.x1-f1/.x2.||<r/2 by A5;
consider g be Real such that
A10: 0<g and
A11: for x1,x2 be Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.x1-
x2.|| < g holds ||.f2/.x1-f2/.x2.|| < r/2 by A3,A7;
take p=min(s,g);
thus 0<p by A8,A10,XXREAL_0:15;
let x1,x2 be Point of RNS;
assume that
A12: x1 in X/\X1 and
A13: x2 in X/\X1 and
A14: ||.x1-x2.||<p;
p <= g by XXREAL_0:17;
then ||.x1-x2.||<g by A14,XXREAL_0:2;
then
A15: ||.f2/.x1-f2/.x2.||<r/2 by A11,A12,A13;
p <= s by XXREAL_0:17;
then ||.x1-x2.||<s by A14,XXREAL_0:2;
then ||.f1/.x1-f1/.x2.||<r/2 by A9,A12,A13;
then
A16: ||.f1/.x1-f1/.x2.||+||.f2/.x1-f2/.x2.||<r/2+r/2 by A15,XREAL_1:8;
A17: ||.f1/.x1 - f1/.x2 + (f2/.x1-f2/.x2).|| <= ||.f1/.x1-f1/.x2.|| + ||.f2
/.x1-f2/.x2.|| by CLVECT_1:def 13;
||.(f1+f2)/.x1-(f1+f2)/.x2.|| = ||.f1/.x1 + f2/.x1-(f1+f2)/.x2.|| by A6,A12,
VFUNCT_1:def 1
.= ||.f1/.x1 + f2/.x1 - (f1/.x2+f2/.x2).|| by A6,A13,VFUNCT_1:def 1
.= ||.f1/.x1 + (f2/.x1 - (f1/.x2+f2/.x2)).|| by RLVECT_1:def 3
.= ||.f1/.x1 + (f2/.x1 - f1/.x2-f2/.x2).|| by RLVECT_1:27
.= ||.f1/.x1 + (-f1/.x2 + f2/.x1-f2/.x2).||
.= ||.f1/.x1 + (-f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:def 3
.= ||.f1/.x1 - f1/.x2 + (f2/.x1-f2/.x2).|| by RLVECT_1:def 3;
hence thesis by A16,A17,XXREAL_0:2;
end;
theorem
for f1,f2 be PartFunc of CNS1,CNS2 st f1 is_uniformly_continuous_on X
& f2 is_uniformly_continuous_on X1 holds f1-f2 is_uniformly_continuous_on X/\X1
proof
let f1,f2 be PartFunc of CNS1,CNS2;
assume that
A1: f1 is_uniformly_continuous_on X and
A2: f2 is_uniformly_continuous_on X1;
A3: f2 is_uniformly_continuous_on X /\ X1 by A2,Th1,XBOOLE_1:17;
then
A4: X /\ X1 c= dom f2;
A5: f1 is_uniformly_continuous_on X /\ X1 by A1,Th1,XBOOLE_1:17;
then X /\ X1 c= dom f1;
then X /\ X1 c= dom f1 /\ dom f2 by A4,XBOOLE_1:19;
hence
A6: X /\ X1 c= dom (f1-f2) by VFUNCT_1:def 2;
let r;
assume 0<r;
then
A7: 0<r/2;
then consider s such that
A8: 0<s and
A9: for x1,x2 be Point of CNS1 st x1 in X /\ X1 & x2 in X /\X1 & ||.x1-
x2.||<s holds ||.f1/.x1-f1/.x2.||<r/2 by A5;
consider g be Real such that
A10: 0<g and
A11: for x1,x2 be Point of CNS1 st x1 in X /\ X1 & x2 in X /\ X1 & ||.x1
-x2.||<g holds ||.f2/.x1-f2/.x2.||<r/2 by A3,A7;
take p=min(s,g);
thus 0<p by A8,A10,XXREAL_0:15;
let x1,x2 be Point of CNS1;
assume that
A12: x1 in X/\X1 and
A13: x2 in X/\X1 and
A14: ||.x1-x2.||<p;
p <= g by XXREAL_0:17;
then ||.x1-x2.||<g by A14,XXREAL_0:2;
then
A15: ||.f2/.x1-f2/.x2.||<r/2 by A11,A12,A13;
p <= s by XXREAL_0:17;
then ||.x1-x2.||<s by A14,XXREAL_0:2;
then ||.f1/.x1-f1/.x2.||<r/2 by A9,A12,A13;
then
A16: ||.f1/.x1-f1/.x2.||+||.f2/.x1-f2/.x2.||<r/2+r/2 by A15,XREAL_1:8;
A17: ||.f1/.x1 - f1/.x2 - (f2/.x1-f2/.x2).|| <= ||.f1/.x1-f1/.x2.|| + ||.f2
/.x1-f2/.x2.|| by CLVECT_1:104;
||.(f1-f2)/.x1-(f1-f2)/.x2.|| = ||.f1/.x1 - f2/.x1-(f1-f2)/.x2.|| by A6,A12,
VFUNCT_1:def 2
.= ||.f1/.x1 - f2/.x1 - (f1/.x2-f2/.x2).|| by A6,A13,VFUNCT_1:def 2
.= ||.f1/.x1 - (f2/.x1 + (f1/.x2-f2/.x2)).|| by RLVECT_1:27
.= ||.f1/.x1 - (f1/.x2 + f2/.x1-f2/.x2).|| by RLVECT_1:def 3
.= ||.f1/.x1 - (f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:def 3
.= ||.f1/.x1 - f1/.x2 - (f2/.x1-f2/.x2).|| by RLVECT_1:27;
hence thesis by A16,A17,XXREAL_0:2;
end;
theorem
for f1,f2 be PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X &
f2 is_uniformly_continuous_on X1 holds f1-f2 is_uniformly_continuous_on X/\X1
proof
let f1,f2 be PartFunc of CNS,RNS;
assume that
A1: f1 is_uniformly_continuous_on X and
A2: f2 is_uniformly_continuous_on X1;
A3: f2 is_uniformly_continuous_on X /\ X1 by A2,Th2,XBOOLE_1:17;
then
A4: X /\ X1 c= dom f2;
A5: f1 is_uniformly_continuous_on X /\ X1 by A1,Th2,XBOOLE_1:17;
then X /\ X1 c= dom f1;
then X /\ X1 c= dom f1 /\ dom f2 by A4,XBOOLE_1:19;
hence
A6: X /\ X1 c= dom (f1-f2) by VFUNCT_1:def 2;
let r;
assume 0<r;
then
A7: 0<r/2;
then consider s such that
A8: 0<s and
A9: for x1,x2 be Point of CNS st x1 in X /\ X1 & x2 in X /\X1 & ||.x1-
x2.||<s holds ||.f1/.x1-f1/.x2.||<r/2 by A5;
consider g be Real such that
A10: 0<g and
A11: for x1,x2 be Point of CNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.x1-
x2.||<g holds ||.f2/.x1-f2/.x2.||<r/2 by A3,A7;
take p=min(s,g);
thus 0<p by A8,A10,XXREAL_0:15;
let x1,x2 be Point of CNS;
assume that
A12: x1 in X/\X1 and
A13: x2 in X/\X1 and
A14: ||.x1-x2.||<p;
p <= g by XXREAL_0:17;
then ||.x1-x2.||<g by A14,XXREAL_0:2;
then
A15: ||.f2/.x1-f2/.x2.||<r/2 by A11,A12,A13;
p <= s by XXREAL_0:17;
then ||.x1-x2.||<s by A14,XXREAL_0:2;
then ||.f1/.x1-f1/.x2.||<r/2 by A9,A12,A13;
then
A16: ||.f1/.x1-f1/.x2.||+||.f2/.x1-f2/.x2.||<r/2+r/2 by A15,XREAL_1:8;
A17: ||.f1/.x1 - f1/.x2 - (f2/.x1-f2/.x2).|| <= ||.f1/.x1-f1/.x2.|| + ||.f2
/.x1-f2/.x2.|| by NORMSP_1:3;
||.(f1-f2)/.x1-(f1-f2)/.x2.|| = ||.f1/.x1 - f2/.x1-(f1-f2)/.x2.|| by A6,A12,
VFUNCT_1:def 2
.= ||.f1/.x1 - f2/.x1 - (f1/.x2-f2/.x2).|| by A6,A13,VFUNCT_1:def 2
.= ||.f1/.x1 - (f2/.x1 + (f1/.x2-f2/.x2)).|| by RLVECT_1:27
.= ||.f1/.x1 - (f1/.x2 + f2/.x1-f2/.x2).|| by RLVECT_1:def 3
.= ||.f1/.x1 - (f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:def 3
.= ||.f1/.x1 - f1/.x2 - (f2/.x1-f2/.x2).|| by RLVECT_1:27;
hence thesis by A16,A17,XXREAL_0:2;
end;
theorem
for f1,f2 be PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X &
f2 is_uniformly_continuous_on X1 holds f1-f2 is_uniformly_continuous_on X/\X1
proof
let f1,f2 be PartFunc of RNS,CNS;
assume that
A1: f1 is_uniformly_continuous_on X and
A2: f2 is_uniformly_continuous_on X1;
A3: f2 is_uniformly_continuous_on X /\ X1 by A2,Th3,XBOOLE_1:17;
then
A4: X /\ X1 c= dom f2;
A5: f1 is_uniformly_continuous_on X /\ X1 by A1,Th3,XBOOLE_1:17;
then X /\ X1 c= dom f1;
then X /\ X1 c= dom f1 /\ dom f2 by A4,XBOOLE_1:19;
hence
A6: X /\ X1 c= dom (f1-f2) by VFUNCT_1:def 2;
let r;
assume 0<r;
then
A7: 0<r/2;
then consider s such that
A8: 0<s and
A9: for x1,x2 be Point of RNS st x1 in X /\ X1 & x2 in X /\X1 & ||.x1-
x2.||<s holds ||.f1/.x1-f1/.x2.||<r/2 by A5;
consider g be Real such that
A10: 0<g and
A11: for x1,x2 be Point of RNS st x1 in X /\ X1 & x2 in X /\ X1 & ||.x1-
x2.||<g holds ||.f2/.x1-f2/.x2.||<r/2 by A3,A7;
take p=min(s,g);
thus 0<p by A8,A10,XXREAL_0:15;
let x1,x2 be Point of RNS;
assume that
A12: x1 in X/\X1 and
A13: x2 in X/\X1 and
A14: ||.x1-x2.||<p;
p <= g by XXREAL_0:17;
then ||.x1-x2.||<g by A14,XXREAL_0:2;
then
A15: ||.f2/.x1-f2/.x2.||<r/2 by A11,A12,A13;
p <= s by XXREAL_0:17;
then ||.x1-x2.||<s by A14,XXREAL_0:2;
then ||.f1/.x1-f1/.x2.||<r/2 by A9,A12,A13;
then
A16: ||.f1/.x1-f1/.x2.||+||.f2/.x1-f2/.x2.||<r/2+r/2 by A15,XREAL_1:8;
A17: ||.f1/.x1 - f1/.x2 - (f2/.x1-f2/.x2).|| <= ||.f1/.x1-f1/.x2.|| + ||.f2
/.x1-f2/.x2.|| by CLVECT_1:104;
||.(f1-f2)/.x1-(f1-f2)/.x2.|| = ||.f1/.x1 - f2/.x1-(f1-f2)/.x2.|| by A6,A12,
VFUNCT_1:def 2
.= ||.f1/.x1 - f2/.x1 - (f1/.x2-f2/.x2).|| by A6,A13,VFUNCT_1:def 2
.= ||.f1/.x1 - (f2/.x1 + (f1/.x2-f2/.x2)).|| by RLVECT_1:27
.= ||.f1/.x1 - (f1/.x2 + f2/.x1-f2/.x2).|| by RLVECT_1:def 3
.= ||.f1/.x1 - (f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:def 3
.= ||.f1/.x1 - f1/.x2 - (f2/.x1-f2/.x2).|| by RLVECT_1:27;
hence thesis by A16,A17,XXREAL_0:2;
end;
theorem Th10:
for f be PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X
holds z(#)f is_uniformly_continuous_on X
proof
let f be PartFunc of CNS1,CNS2;
assume
A1: f is_uniformly_continuous_on X;
then X c= dom f;
hence
A2: X c= dom (z(#)f) by VFUNCT_2:def 2;
now
per cases;
suppose
A3: z=0;
let r;
assume
A4: 0<r;
then consider s such that
A5: 0<s and
for x1,x2 be Point of CNS1 st x1 in X & x2 in X & ||.x1-x2.||<s
holds ||.f/.x1-f/.x2.||<r by A1;
take s;
thus 0<s by A5;
let x1,x2 be Point of CNS1;
assume that
A6: x1 in X and
A7: x2 in X and
||.x1-x2.||<s;
||.(z(#)f)/.x1-(z(#)f)/.x2.|| = ||.z*(f/.x1)-(z(#)f)/.x2.|| by A2,A6,
VFUNCT_2:def 2
.= ||.0.CNS2 -(z(#)f)/.x2.|| by A3,CLVECT_1:1
.= ||.0.CNS2 - z*(f/.x2).|| by A2,A7,VFUNCT_2:def 2
.= ||.0.CNS2 - 0.CNS2.|| by A3,CLVECT_1:1
.= ||.0.CNS2 .|| by RLVECT_1:13
.= 0 by NORMSP_0:def 6;
hence ||.(z(#)f)/.x1-(z(#)f)/.x2.|| <r by A4;
end;
suppose
A8: z<>0;
let r;
A9: 0<|.z.| by A8,COMPLEX1:47;
assume 0<r;
then 0 < r/|.z.| by A9;
then consider s such that
A10: 0<s and
A11: for x1,x2 be Point of CNS1 st x1 in X & x2 in X & ||.x1-x2.||<s
holds ||.f/.x1-f/.x2.||<r/|.z.| by A1;
take s;
thus 0<s by A10;
let x1,x2 be Point of CNS1;
assume that
A12: x1 in X and
A13: x2 in X and
A14: ||.x1-x2.||<s;
A15: ||.(z(#)f)/.x1-(z(#)f)/.x2.|| = ||.z*(f/.x1)-(z(#)f)/.x2.|| by A2,A12,
VFUNCT_2:def 2
.= ||.z*(f/.x1) - z*(f/.x2).|| by A2,A13,VFUNCT_2:def 2
.= ||.z*(f/.x1 - f/.x2).|| by CLVECT_1:9
.= |.z.|*||.f/.x1 - f/.x2.|| by CLVECT_1:def 13;
|.z.|*||.f/.x1-f/.x2.||<r/|.z.|*|.z.| by A9,A11,A12,A13,A14,XREAL_1:68;
hence ||.(z(#)f)/.x1-(z(#)f)/.x2.|| <r by A9,A15,XCMPLX_1:87;
end;
end;
hence thesis;
end;
theorem Th11:
for f be PartFunc of CNS,RNS st f is_uniformly_continuous_on X
holds r(#)f is_uniformly_continuous_on X
proof
let f be PartFunc of CNS,RNS;
assume
A1: f is_uniformly_continuous_on X;
then X c= dom f;
hence
A2: X c= dom (r(#)f) by VFUNCT_1:def 4;
now
per cases;
suppose
A3: r=0;
let p be Real;
assume
A4: 0<p;
then consider s such that
A5: 0<s and
for x1,x2 be Point of CNS st x1 in X & x2 in X & ||.x1-x2.||<s holds
||.f/.x1-f/.x2.||<p by A1;
take s;
thus 0<s by A5;
let x1,x2 be Point of CNS;
assume that
A6: x1 in X and
A7: x2 in X and
||.x1-x2.||<s;
||.(r(#)f)/.x1-(r(#)f)/.x2.|| = ||.r*(f/.x1)-(r(#)f)/.x2.|| by A2,A6,
VFUNCT_1:def 4
.= ||.0.RNS -(r(#)f)/.x2.|| by A3,RLVECT_1:10
.= ||.0.RNS - r*(f/.x2).|| by A2,A7,VFUNCT_1:def 4
.= ||.0.RNS - 0.RNS.|| by A3,RLVECT_1:10
.= ||.0.RNS .|| by RLVECT_1:13
.= 0 by NORMSP_0:def 6;
hence ||.(r(#)f)/.x1-(r(#)f)/.x2.|| <p by A4;
end;
suppose
A8: r<>0;
let p be Real;
A9: 0<|.r.| by A8,COMPLEX1:47;
assume 0<p;
then 0 < p/|.r.| by A9;
then consider s such that
A10: 0<s and
A11: for x1,x2 be Point of CNS st x1 in X & x2 in X & ||.x1-x2.||<s
holds ||.f/.x1-f/.x2.||<p/|.r.| by A1;
take s;
thus 0<s by A10;
let x1,x2 be Point of CNS;
assume that
A12: x1 in X and
A13: x2 in X and
A14: ||.x1-x2.||<s;
A15: ||.(r(#)f)/.x1-(r(#)f)/.x2.|| = ||.r*(f/.x1)-(r(#)f)/.x2.|| by A2,A12,
VFUNCT_1:def 4
.= ||.r*(f/.x1) - r*(f/.x2).|| by A2,A13,VFUNCT_1:def 4
.= ||.r*(f/.x1 - f/.x2).|| by RLVECT_1:34
.= |.r.|*||.f/.x1 - f/.x2.|| by NORMSP_1:def 1;
|.r.|*||.f/.x1-f/.x2.||<p/|.r.|*|.r.| by A9,A11,A12,A13,A14,XREAL_1:68;
hence ||.(r(#)f)/.x1-(r(#)f)/.x2.|| < p by A9,A15,XCMPLX_1:87;
end;
end;
hence thesis;
end;
theorem Th12:
for f be PartFunc of RNS,CNS st f is_uniformly_continuous_on X
holds z(#)f is_uniformly_continuous_on X
proof
let f be PartFunc of RNS,CNS;
assume
A1: f is_uniformly_continuous_on X;
then X c= dom f;
hence
A2: X c= dom (z(#)f) by VFUNCT_2:def 2;
now
per cases;
suppose
A3: z=0;
let r;
assume
A4: 0<r;
then consider s such that
A5: 0<s and
for x1,x2 be Point of RNS st x1 in X & x2 in X & ||.x1-x2.||<s holds
||.f/.x1-f/.x2.||<r by A1;
take s;
thus 0<s by A5;
let x1,x2 be Point of RNS;
assume that
A6: x1 in X and
A7: x2 in X and
||.x1-x2.||<s;
||.(z(#)f)/.x1-(z(#)f)/.x2.|| = ||.z*(f/.x1)-(z(#)f)/.x2.|| by A2,A6,
VFUNCT_2:def 2
.= ||.0.CNS -(z(#)f)/.x2.|| by A3,CLVECT_1:1
.= ||.0.CNS - z*(f/.x2).|| by A2,A7,VFUNCT_2:def 2
.= ||.0.CNS - 0.CNS.|| by A3,CLVECT_1:1
.= ||.0.CNS .|| by RLVECT_1:13
.= 0 by NORMSP_0:def 6;
hence ||.(z(#)f)/.x1-(z(#)f)/.x2.|| <r by A4;
end;
suppose
A8: z<>0;
let r;
A9: 0<|.z.| by A8,COMPLEX1:47;
assume 0<r;
then 0 < r/|.z.| by A9;
then consider s such that
A10: 0<s and
A11: for x1,x2 be Point of RNS st x1 in X & x2 in X & ||.x1-x2.||<s
holds ||.f/.x1-f/.x2.||<r/|.z.| by A1;
take s;
thus 0<s by A10;
let x1,x2 be Point of RNS;
assume that
A12: x1 in X and
A13: x2 in X and
A14: ||.x1-x2.||<s;
A15: ||.(z(#)f)/.x1-(z(#)f)/.x2.|| = ||.z*(f/.x1)-(z(#)f)/.x2.|| by A2,A12,
VFUNCT_2:def 2
.= ||.z*(f/.x1) - z*(f/.x2).|| by A2,A13,VFUNCT_2:def 2
.= ||.z*(f/.x1 - f/.x2).|| by CLVECT_1:9
.= |.z.|*||.f/.x1 - f/.x2.|| by CLVECT_1:def 13;
|.z.|*||.f/.x1-f/.x2.||<r/|.z.|*|.z.| by A9,A11,A12,A13,A14,XREAL_1:68;
hence ||.(z(#)f)/.x1-(z(#)f)/.x2.|| <r by A9,A15,XCMPLX_1:87;
end;
end;
hence thesis;
end;
theorem
for f be PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
-f is_uniformly_continuous_on X
proof
let f be PartFunc of CNS1,CNS2;
A1: -f = (-1r)(#)f by VFUNCT_2:23;
assume f is_uniformly_continuous_on X;
hence thesis by A1,Th10;
end;
theorem
for f be PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds -
f is_uniformly_continuous_on X
proof
let f be PartFunc of CNS,RNS;
A1: -f = (-1)(#)f by VFUNCT_1:23;
assume f is_uniformly_continuous_on X;
hence thesis by A1,Th11;
end;
theorem
for f be PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds -
f is_uniformly_continuous_on X
proof
let f be PartFunc of RNS,CNS;
A1: -f = (-1r)(#)f by VFUNCT_2:23;
assume f is_uniformly_continuous_on X;
hence thesis by A1,Th12;
end;
theorem
for f be PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
proof
let f be PartFunc of CNS1,CNS2;
assume
A1: f is_uniformly_continuous_on X;
then X c= dom f;
hence
A2: X c= dom (||.f.||) by NORMSP_0:def 3;
let r;
assume 0<r;
then consider s such that
A3: 0<s and
A4: for x1,x2 be Point of CNS1 st x1 in X & x2 in X & ||.x1-x2.||<s
holds ||.f/.x1-f/.x2.||<r by A1;
take s;
thus 0<s by A3;
let x1,x2 be Point of CNS1;
assume that
A5: x1 in X and
A6: x2 in X and
A7: ||.x1-x2.||<s;
|.(||.f.||)/.x1-(||.f.||)/.x2.| =|.(||.f.||).x1-(||.f.||)/.x2.| by A2,A5,
PARTFUN1:def 6
.=|.(||.f.||).x1-(||.f.||).x2.| by A2,A6,PARTFUN1:def 6
.= |.||.f/.x1.||-(||.f.||).x2.| by A2,A5,NORMSP_0:def 3
.= |.||.f/.x1.|| - ||.f/.x2.||.| by A2,A6,NORMSP_0:def 3;
then
A8: |.(||.f.||)/.x1-(||.f.||)/.x2.| <= ||.f/.x1-f/.x2.|| by CLVECT_1:110;
||.f/.x1-f/.x2.||<r by A4,A5,A6,A7;
hence thesis by A8,XXREAL_0:2;
end;
theorem
for f be PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
proof
let f be PartFunc of CNS,RNS;
assume
A1: f is_uniformly_continuous_on X;
then X c= dom f;
hence
A2: X c= dom (||.f.||) by NORMSP_0:def 3;
let r;
assume 0<r;
then consider s such that
A3: 0<s and
A4: for x1,x2 be Point of CNS st x1 in X & x2 in X & ||.x1-x2.||<s holds
||.f/.x1-f/.x2.||<r by A1;
take s;
thus 0<s by A3;
let x1,x2 be Point of CNS;
assume that
A5: x1 in X and
A6: x2 in X and
A7: ||.x1-x2.||<s;
|.(||.f.||)/.x1-(||.f.||)/.x2.| =|.(||.f.||).x1-(||.f.||)/.x2.| by A2,A5,
PARTFUN1:def 6
.=|.(||.f.||).x1-(||.f.||).x2.| by A2,A6,PARTFUN1:def 6
.= |.||.f/.x1.||-(||.f.||).x2.| by A2,A5,NORMSP_0:def 3
.= |.||.f/.x1.|| - ||.f/.x2.||.| by A2,A6,NORMSP_0:def 3;
then
A8: |.(||.f.||)/.x1-(||.f.||)/.x2.| <= ||.f/.x1-f/.x2.|| by NORMSP_1:9;
||.f/.x1-f/.x2.||<r by A4,A5,A6,A7;
hence thesis by A8,XXREAL_0:2;
end;
theorem
for f be PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
proof
let f be PartFunc of RNS,CNS;
assume
A1: f is_uniformly_continuous_on X;
then X c= dom f;
then
A2: X c= dom (||.f.||) by NORMSP_0:def 3;
for r be Real st 0 < r ex s be Real st 0 < s &
for x1,x2 be Point of RNS
st x1 in X & x2 in X & ||.x1-x2.|| < s holds |.(||.f.||)/.x1 - (||.f.||)/.x2
.| < r
proof
let r be Real;
assume 0 < r;
then consider s be Real such that
A3: 0 < s and
A4: for x1,x2 be Point of RNS st x1 in X & x2 in X & ||.x1-x2.|| < s
holds ||. f/.x1 - f/.x2 .|| < r by A1;
reconsider s as Real;
take s;
thus 0<s by A3;
let x1,x2 be Point of RNS;
assume that
A5: x1 in X and
A6: x2 in X and
A7: ||.x1-x2.||<s;
|.(||.f.||)/.x1-(||.f.||)/.x2.| =|.(||.f.||).x1-(||.f.||)/.x2.| by A2,A5,
PARTFUN1:def 6
.=|.(||.f.||).x1-(||.f.||).x2.| by A2,A6,PARTFUN1:def 6
.= |.||.f/.x1.||-(||.f.||).x2.| by A2,A5,NORMSP_0:def 3
.= |.||.f/.x1.|| - ||.f/.x2.||.| by A2,A6,NORMSP_0:def 3;
then
A8: |.(||.f.||)/.x1-(||.f.||)/.x2.| <= ||.f/.x1-f/.x2.|| by CLVECT_1:110;
||.f/.x1-f/.x2.||<r by A4,A5,A6,A7;
hence thesis by A8,XXREAL_0:2;
end;
hence thesis by A2,NFCONT_2:def 2;
end;
theorem Th19:
for f be PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X
holds f is_continuous_on X
proof
let f be PartFunc of CNS1,CNS2;
assume
A1: f is_uniformly_continuous_on X;
A2: now
let x0 be Point of CNS1;
let r be Real;
assume that
A3: x0 in X and
A4: 0<r;
consider s be Real such that
A5: 0<s and
A6: for x1,x2 be Point of CNS1 st x1 in X & x2 in X & ||.x1 -x2.|| < s
holds ||.f/.x1 - f/.x2.||< r by A1,A4;
take s;
thus 0<s by A5;
let x1 be Point of CNS1;
assume x1 in X & ||.x1-x0.|| < s;
hence ||.f/.x1 - f/.x0.|| < r by A3,A6;
end;
X c= dom f by A1;
hence thesis by A2,NCFCONT1:44;
end;
theorem Th20:
for f be PartFunc of CNS,RNS st f is_uniformly_continuous_on X
holds f is_continuous_on X
proof
let f be PartFunc of CNS,RNS;
assume
A1: f is_uniformly_continuous_on X;
A2: now
let x0 be Point of CNS;
let r be Real;
assume that
A3: x0 in X and
A4: 0<r;
consider s be Real such that
A5: 0<s and
A6: for x1,x2 be Point of CNS st x1 in X & x2 in X & ||.x1 -x2.|| < s
holds ||.f/.x1 - f/.x2.||< r by A1,A4;
take s;
thus 0<s by A5;
let x1 be Point of CNS;
assume x1 in X & ||.x1-x0.|| < s;
hence ||.f/.x1 - f/.x0.|| < r by A3,A6;
end;
X c= dom f by A1;
hence thesis by A2,NCFCONT1:45;
end;
theorem Th21:
for f be PartFunc of RNS,CNS st f is_uniformly_continuous_on X
holds f is_continuous_on X
proof
let f be PartFunc of RNS,CNS;
assume
A1: f is_uniformly_continuous_on X;
A2: now
let x0 be Point of RNS;
let r be Real;
assume that
A3: x0 in X and
A4: 0<r;
consider s be Real such that
A5: 0<s and
A6: for x1,x2 be Point of RNS st x1 in X & x2 in X & ||.x1 -x2.|| < s
holds ||.f/.x1 - f/.x2.||< r by A1,A4;
take s;
thus 0<s by A5;
let x1 be Point of RNS;
assume x1 in X & ||.x1-x0.|| < s;
hence ||.f/.x1 - f/.x0.|| < r by A3,A6;
end;
X c= dom f by A1;
hence thesis by A2,NCFCONT1:46;
end;
theorem
for f be PartFunc of the carrier of CNS, COMPLEX st f
is_uniformly_continuous_on X holds f is_continuous_on X
proof
let f be PartFunc of the carrier of CNS, COMPLEX;
assume
A1: f is_uniformly_continuous_on X;
A2: now
let x0 be Point of CNS;
let r be Real;
assume that
A3: x0 in X and
A4: 0<r;
consider s be Real such that
A5: 0<s and
A6: for x1,x2 be Point of CNS st x1 in X & x2 in X & ||.x1 -x2.|| < s
holds |.(f/.x1 - f/.x2).|< r by A1,A4;
take s;
thus 0<s by A5;
let x1 be Point of CNS;
assume x1 in X & ||.x1-x0.|| < s;
hence |.(f/.x1 - f/.x0).| < r by A3,A6;
end;
X c= dom f by A1;
hence thesis by A2,NCFCONT1:47;
end;
theorem Th23:
for f be PartFunc of the carrier of CNS, REAL st f
is_uniformly_continuous_on X holds f is_continuous_on X
proof
let f be PartFunc of the carrier of CNS, REAL;
assume
A1: f is_uniformly_continuous_on X;
A2: now
let x0 be Point of CNS;
let r be Real;
assume that
A3: x0 in X and
A4: 0<r;
consider s be Real such that
A5: 0<s and
A6: for x1,x2 be Point of CNS st x1 in X & x2 in X & ||.x1 -x2.|| < s
holds |.f/.x1 - f/.x2.|< r by A1,A4;
take s;
thus 0<s by A5;
let x1 be Point of CNS;
assume x1 in X & ||.x1-x0.|| < s;
hence |.f/.x1 - f/.x0.| < r by A3,A6;
end;
X c= dom f by A1;
hence thesis by A2,NCFCONT1:48;
end;
theorem
for f be PartFunc of the carrier of RNS, COMPLEX st f
is_uniformly_continuous_on X holds f is_continuous_on X
proof
let f be PartFunc of the carrier of RNS, COMPLEX;
assume
A1: f is_uniformly_continuous_on X;
A2: now
let x0 be Point of RNS;
let r be Real;
assume that
A3: x0 in X and
A4: 0<r;
consider s be Real such that
A5: 0<s and
A6: for x1,x2 be Point of RNS st x1 in X & x2 in X & ||.x1 -x2.|| < s
holds |.(f/.x1 - f/.x2).|< r by A1,A4;
take s;
thus 0<s by A5;
let x1 be Point of RNS;
assume x1 in X & ||.x1-x0.|| < s;
hence |.(f/.x1 - f/.x0).| < r by A3,A6;
end;
X c= dom f by A1;
hence thesis by A2,NCFCONT1:49;
end;
theorem Th25:
for f be PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds f
is_uniformly_continuous_on X
proof
let f be PartFunc of CNS1,CNS2;
assume
A1: f is_Lipschitzian_on X;
hence X c= dom f by NCFCONT1:def 17;
consider r be Real such that
A2: 0<r and
A3: for x1,x2 be Point of CNS1 st x1 in X & x2 in X holds ||.f/.x1-f/.x2
.||<=r*||.x1-x2.|| by A1,NCFCONT1:def 17;
let p be Real such that
A4: 0<p;
take s=p/r;
thus 0<s by A2,A4;
let x1,x2 be Point of CNS1;
assume x1 in X & x2 in X & ||.x1 -x2.|| < s;
then r*||.x1 -x2.|| < s*r & ||.f/.x1-f/.x2.||<=r*||.x1-x2.|| by A2,A3,
XREAL_1:68;
then ||.f/.x1-f/.x2.||<p/r*r by XXREAL_0:2;
hence thesis by A2,XCMPLX_1:87;
end;
theorem Th26:
for f be PartFunc of CNS,RNS st f is_Lipschitzian_on X holds f
is_uniformly_continuous_on X
proof
let f be PartFunc of CNS,RNS;
assume
A1: f is_Lipschitzian_on X;
hence X c= dom f by NCFCONT1:def 18;
consider r be Real such that
A2: 0<r and
A3: for x1,x2 be Point of CNS st x1 in X & x2 in X holds ||.f/.x1-f/.x2
.||<=r*||.x1-x2.|| by A1,NCFCONT1:def 18;
let p be Real such that
A4: 0<p;
take s=p/r;
thus 0<s by A2,A4;
let x1,x2 be Point of CNS;
assume x1 in X & x2 in X & ||.x1 -x2.|| < s;
then r*||.x1 -x2.|| < s*r & ||.f/.x1-f/.x2.||<=r*||.x1-x2.|| by A2,A3,
XREAL_1:68;
then ||.f/.x1-f/.x2.||<p/r*r by XXREAL_0:2;
hence thesis by A2,XCMPLX_1:87;
end;
theorem Th27:
for f be PartFunc of RNS,CNS st f is_Lipschitzian_on X holds f
is_uniformly_continuous_on X
proof
let f be PartFunc of RNS,CNS;
assume
A1: f is_Lipschitzian_on X;
hence X c= dom f by NCFCONT1:def 19;
consider r be Real such that
A2: 0<r and
A3: for x1,x2 be Point of RNS st x1 in X & x2 in X holds ||.f/.x1-f/.x2
.||<=r*||.x1-x2.|| by A1,NCFCONT1:def 19;
let p be Real such that
A4: 0<p;
take s=p/r;
thus 0<s by A2,A4;
let x1,x2 be Point of RNS;
assume x1 in X & x2 in X & ||.x1 -x2.|| < s;
then r*||.x1 -x2.|| < s*r & ||.f/.x1-f/.x2.||<=r*||.x1-x2.|| by A2,A3,
XREAL_1:68;
then ||.f/.x1-f/.x2.||<p/r*r by XXREAL_0:2;
hence thesis by A2,XCMPLX_1:87;
end;
theorem
for f be PartFunc of CNS1,CNS2, Y be Subset of CNS1 st Y is compact &
f is_continuous_on Y holds f is_uniformly_continuous_on Y
proof
let f be PartFunc of CNS1,CNS2;
let Y be Subset of CNS1;
assume that
A1: Y is compact and
A2: f is_continuous_on Y;
A3: Y c= dom f by A2,NCFCONT1:def 11;
assume not thesis;
then consider r such that
A4: 0<r and
A5: for s st 0<s ex x1,x2 be Point of CNS1 st x1 in Y & x2 in Y & ||.x1
-x2.|| < s & not ||.f/.x1 - f/.x2.||< r by A3;
defpred P[Element of NAT,Point of CNS1] means $2 in Y & ex x2 be Point of
CNS1 st x2 in Y & ||.$2-x2.||<1/($1+1) & not ||.f/.($2)-f/.x2.|| < r;
A6: now
let n be Element of NAT;
consider x1 be Point of CNS1 such that
A7: ex x2 be Point of CNS1 st x1 in Y & x2 in Y & ||.x1 -x2.|| < 1/(n
+1) & not ||.f/.x1 - f/.x2.||< r by A5;
take x1;
thus P[n,x1] by A7;
end;
consider s1 be sequence of CNS1 such that
A8: for n be Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A6);
defpred P1[Nat, Point of CNS1] means $2 in Y & ||.s1.$1-$2.|| < 1
/($1+1) & not ||.f/.(s1.$1)-f/.$2.|| < r;
A9: for n be Element of NAT ex x2 be Point of CNS1 st P1[n,x2] by A8;
consider s2 be sequence of CNS1 such that
A10: for n be Element of NAT holds P1[n,s2.n] from FUNCT_2:sch 3(A9);
A11: for n be Nat holds P1[n,s2.n]
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A10;
end;
now
let x be Point of CNS1;
assume x in rng s1;
then consider n be Nat such that
A12: x=s1.n by NCFCONT1:7;
n in NAT by ORDINAL1:def 12;
hence x in Y by A8,A12;
end;
then for x be object st x in rng s1 holds x in Y;
then
A13: rng s1 c= Y by TARSKI:def 3;
then consider q1 be sequence of CNS1 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 be 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 11;
now
let x be object;
assume x in rng s2;
then consider n be Nat such that
A19: x=s2.n by NCFCONT1:7;
thus x in Y by A11,A19;
end;
then
A20: rng s2 c= Y by TARSKI:def 3;
now
let n be Element of NAT;
thus q2.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.CNS1 + s2.(Ns1.n) by RLVECT_1:15
.= s2.(Ns1.n) by RLVECT_1:4
.= (s2*Ns1).n by FUNCT_2:15;
end;
then
A21: q2 = s2*Ns1 by FUNCT_2:63;
then rng q2 c= rng s2 by VALUED_0:21;
then
A22: rng q2 c= Y by A20,XBOOLE_1:1;
then rng q2 c= dom f by A3,XBOOLE_1:1;
then rng q2 c= dom f /\ Y by A22,XBOOLE_1:19;
then
A23: rng q2 c= dom (f|Y) by RELAT_1:61;
A24: now
let p be Real such that
A25: 0<p;
consider k be Nat such that
A26: p" < k by SEQ_4:3;
take k;
let m be Nat;
assume k <= m;
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.CNS1.|| = ||.s1.m - s2.m - 0.CNS1.|| by NORMSP_1:def 3
.= ||.s1.m - s2.m .|| by RLVECT_1:13;
hence ||.(s1-s2).m - 0.CNS1.|| < p by A28,A27,XXREAL_0:2;
end;
then
A29: s1-s2 is convergent by CLVECT_1:def 15;
then
A30: (s1-s2)*Ns1 is convergent by CLOPBAN3:7;
then
A31: q2 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 5;
A35: (f|Y)/*q1 is convergent by A15,A18,A33,NCFCONT1:def 5;
lim (s1-s2) = 0.CNS1 by A24,A29,CLVECT_1:def 16;
then lim ((s1-s2)*Ns1) = 0.CNS1 by A29,CLOPBAN3:8;
then
A36: lim q2 = lim q1 - 0.CNS1 by A15,A30,CLVECT_1:120
.= lim q1 by RLVECT_1:13;
then
A37: (f|Y)/*q2 is convergent by A18,A31,A23,NCFCONT1:def 5;
then
A38: (f|Y)/*q1 - (f|Y)/*q2 is convergent by A35,CLVECT_1:114;
(f|Y)/.(lim q1) = lim ((f|Y)/*q2) by A18,A31,A36,A23,NCFCONT1:def 5;
then
A39: lim ((f|Y)/*q1 - (f|Y)/*q2) = (f|Y)/.(lim q1) - (f|Y)/.(lim q1) by A35,A34
,A37,CLVECT_1:120
.= 0.CNS2 by RLVECT_1:15;
now
let n be Element of NAT;
consider k be Nat such that
A40: for m be Nat st k<=m holds ||.((f|Y)/*q1 - (f|Y)/*q2).
m-0.CNS2 .||<r by A4,A38,A39,CLVECT_1:def 16;
A41: k in NAT by ORDINAL1:def 12;
A42: q1.k in rng q1 by NCFCONT1:7;
A43: q2.k in rng q2 by NCFCONT1:7;
||.((f|Y)/*q1 - (f|Y)/*q2).k - 0.CNS2 .|| = ||.((f|Y)/*q1 - (f|Y)/*q2
).k .|| by RLVECT_1:13
.= ||.((f|Y)/*q1).k - ((f|Y)/*q2).k.|| by NORMSP_1:def 3
.= ||.(f|Y)/.(q1.k) - ((f|Y)/*q2).k.|| by A33,FUNCT_2:109,A41
.= ||.(f|Y)/.(q1.k) - (f|Y)/.(q2.k) .|| by A23,FUNCT_2:109,A41
.= ||.f/.(q1.k) - (f|Y)/.(q2.k).|| by A33,A42,PARTFUN2:15
.= ||.f/.(q1.k) - f/.(q2.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;
end;
hence contradiction;
end;
theorem
for f be PartFunc of CNS,RNS, Y be Subset of CNS st Y is compact & f
is_continuous_on Y holds f is_uniformly_continuous_on Y
proof
let f be PartFunc of CNS,RNS;
let Y be Subset of CNS;
assume that
A1: Y is compact and
A2: f is_continuous_on Y;
A3: Y c= dom f by A2,NCFCONT1:def 12;
assume not thesis;
then consider r such that
A4: 0<r and
A5: for s st 0<s ex x1,x2 be Point of CNS st x1 in Y & x2 in Y & ||.x1 -
x2.|| < s & not ||.f/.x1 - f/.x2.||< r by A3;
defpred P[Element of NAT,Point of CNS] means $2 in Y & ex x2 be Point of CNS
st x2 in Y & ||.$2-x2.||<1/($1+1) & not ||.f/.($2)-f/.x2.|| < r;
A6: now
let n be Element of NAT;
consider x1 be Point of CNS such that
A7: ex x2 be 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;
thus P[n,x1] by A7;
end;
consider s1 be sequence of CNS such that
A8: for n be Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A6);
defpred P1[Nat, Point of CNS] means $2 in Y & ||.s1.$1-$2.|| < 1/
($1+1) & not ||.f/.(s1.$1)-f/.$2.|| < r;
A9: for n be Element of NAT ex x2 be Point of CNS st P1[n,x2] by A8;
consider s2 be sequence of CNS such that
A10: for n be Element of NAT holds P1[n,s2.n] from FUNCT_2:sch 3(A9);
A11: for n be Nat holds P1[n,s2.n]
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A10;
end;
now
let x be Point of CNS;
assume x in rng s1;
then consider n be Nat such that
A12: x=s1.n by NCFCONT1:7;
n in NAT by ORDINAL1:def 12;
hence x in Y by A8,A12;
end;
then for x be object st x in rng s1 holds x in Y;
then
A13: rng s1 c= Y by TARSKI:def 3;
then consider q1 be 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 be 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
let x be object;
assume x in rng s2;
then consider n be Nat such that
A19: x=s2.n by NCFCONT1:7;
thus x in Y by A11,A19;
end;
then
A20: rng s2 c= Y by TARSKI:def 3;
now
let n be Element of NAT;
thus q2.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;
end;
then
A21: q2 = s2*Ns1 by FUNCT_2:63;
then rng q2 c= rng s2 by VALUED_0:21;
then
A22: rng q2 c= Y by A20,XBOOLE_1:1;
then rng q2 c= dom f by A3,XBOOLE_1:1;
then rng q2 c= dom f /\ Y by A22,XBOOLE_1:19;
then
A23: rng q2 c= dom (f|Y) by RELAT_1:61;
A24: now
let p be Real such that
A25: 0<p;
consider k be Nat such that
A26: p" < k by SEQ_4:3;
take k;
let m be Nat;
assume k <= m;
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;
end;
then
A29: s1-s2 is convergent by CLVECT_1:def 15;
then
A30: (s1-s2)*Ns1 is convergent by CLOPBAN3:7;
then
A31: q2 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 q2 = lim q1 - 0.CNS by A15,A30,CLVECT_1:120
.= lim q1 by RLVECT_1:13;
then
A37: (f|Y)/*q2 is convergent by A18,A31,A23,NCFCONT1:def 6;
then
A38: (f|Y)/*q1 - (f|Y)/*q2 is convergent by A35,NORMSP_1:20;
(f|Y)/.(lim q1) = lim ((f|Y)/*q2) by A18,A31,A36,A23,NCFCONT1:def 6;
then
A39: lim ((f|Y)/*q1 - (f|Y)/*q2) = (f|Y)/.(lim q1) - (f|Y)/.(lim q1) by A35,A34
,A37,NORMSP_1:26
.= 0.RNS by RLVECT_1:15;
now
let n be Element of NAT;
consider k be Nat such that
A40: for m be Nat st k<=m holds ||.((f|Y)/*q1 - (f|Y)/*q2).
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: q2.k in rng q2 by NCFCONT1:7;
||.((f|Y)/*q1 - (f|Y)/*q2).k - 0.RNS .|| = ||.((f|Y)/*q1 - (f|Y)/*q2)
.k .|| by RLVECT_1:13
.= ||.((f|Y)/*q1).k - ((f|Y)/*q2).k.|| by NORMSP_1:def 3
.= ||.(f|Y)/.(q1.k) - ((f|Y)/*q2).k.|| by A33,FUNCT_2:109,A41
.= ||.(f|Y)/.(q1.k) - (f|Y)/.(q2.k) .|| by A23,FUNCT_2:109,A41
.= ||.f/.(q1.k) - (f|Y)/.(q2.k).|| by A33,A42,PARTFUN2:15
.= ||.f/.(q1.k) - f/.(q2.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;
end;
hence contradiction;
end;
theorem
for f be PartFunc of RNS,CNS, Y be Subset of RNS st Y is compact & f
is_continuous_on Y holds f is_uniformly_continuous_on Y
proof
let f be PartFunc of RNS,CNS;
let Y be Subset of RNS;
assume that
A1: Y is compact and
A2: f is_continuous_on Y;
A3: Y c= dom f by A2,NCFCONT1:def 13;
assume not thesis;
then consider r such that
A4: 0<r and
A5: for s st 0<s ex x1,x2 be Point of RNS st x1 in Y & x2 in Y & ||.x1 -
x2.|| < s & not ||.f/.x1 - f/.x2.||< r by A3;
defpred P[Element of NAT,Point of RNS] means $2 in Y & ex x2 be Point of RNS
st x2 in Y & ||.$2-x2.||<1/($1+1) & not ||.f/.($2)-f/.x2.|| < r;
A6: now
let n be Element of NAT;
consider x1 be Point of RNS such that
A7: ex x2 be Point of RNS st x1 in Y & x2 in Y & ||.x1 -x2.|| < 1/(n+
1) & not ||.f/.x1 - f/.x2.||< r by A5;
take x1;
thus P[n,x1] by A7;
end;
consider s1 be sequence of RNS such that
A8: for n be Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A6);
defpred P1[Nat, Point of RNS] means $2 in Y & ||.s1.$1-$2.|| < 1/
($1+1) & not ||.f/.(s1.$1)-f/.$2.|| < r;
A9: for n be Element of NAT ex x2 be Point of RNS st P1[n,x2] by A8;
consider s2 be sequence of RNS such that
A10: for n be Element of NAT holds P1[n,s2.n] from FUNCT_2:sch 3(A9);
A11: for n be Nat holds P1[n,s2.n]
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A10;
end;
now
let x be Point of RNS;
assume x in rng s1;
then consider n be Nat such that
A12: x=s1.n by NFCONT_1:6;
n in NAT by ORDINAL1:def 12;
hence x in Y by A8,A12;
end;
then for x be object st x in rng s1 holds x in Y;
then
A13: rng s1 c= Y by TARSKI:def 3;
then consider q1 be 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 be 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 13;
now
let x be object;
assume x in rng s2;
then consider n be Nat such that
A19: x=s2.n by NFCONT_1:6;
thus x in Y by A11,A19;
end;
then
A20: rng s2 c= Y by TARSKI:def 3;
now
let n be Element of NAT;
thus q2.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.RNS + s2.(Ns1.n) by RLVECT_1:15
.= s2.(Ns1.n) by RLVECT_1:4
.= (s2*Ns1).n by FUNCT_2:15;
end;
then
A21: q2 = s2*Ns1 by FUNCT_2:63;
then rng q2 c= rng s2 by VALUED_0:21;
then
A22: rng q2 c= Y by A20,XBOOLE_1:1;
then rng q2 c= dom f by A3,XBOOLE_1:1;
then rng q2 c= dom f /\ Y by A22,XBOOLE_1:19;
then
A23: rng q2 c= dom (f|Y) by RELAT_1:61;
A24: now
let p be Real such that
A25: 0<p;
consider k be Nat such that
A26: p" < k by SEQ_4:3;
take k;
let m be Nat;
assume k <= m;
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.RNS.|| = ||.s1.m - s2.m - 0.RNS.|| by NORMSP_1:def 3
.= ||.s1.m - s2.m .|| by RLVECT_1:13;
hence ||.(s1-s2).m - 0.RNS.|| < p by A28,A27,XXREAL_0:2;
end;
then
A29: s1-s2 is convergent by NORMSP_1:def 6;
then
A30: (s1-s2)*Ns1 is convergent by LOPBAN_3:7;
then
A31: q2 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 q2 = lim q1 - 0.RNS by A15,A30,NORMSP_1:26
.= lim q1 by RLVECT_1:13;
then
A37: (f|Y)/*q2 is convergent by A18,A31,A23,NCFCONT1:def 7;
then
A38: (f|Y)/*q1 - (f|Y)/*q2 is convergent by A35,CLVECT_1:114;
(f|Y)/.(lim q1) = lim ((f|Y)/*q2) by A18,A31,A36,A23,NCFCONT1:def 7;
then
A39: lim ((f|Y)/*q1 - (f|Y)/*q2) = (f|Y)/.(lim q1) - (f|Y)/.(lim q1) by A35,A34
,A37,CLVECT_1:120
.= 0.CNS by RLVECT_1:15;
now
let n be Element of NAT;
consider k be Nat such that
A40: for m be Nat st k<=m holds ||.((f|Y)/*q1 - (f|Y)/*q2).
m-0.CNS .||<r by A4,A38,A39,CLVECT_1:def 16;
A41: q1.k in rng q1 by NFCONT_1:6;
A42: q2.k in rng q2 by NFCONT_1:6;
A43: k in NAT by ORDINAL1:def 12;
||.((f|Y)/*q1 - (f|Y)/*q2).k - 0.CNS .|| = ||.((f|Y)/*q1 - (f|Y)/*q2)
.k .|| by RLVECT_1:13
.= ||.((f|Y)/*q1).k - ((f|Y)/*q2).k.|| by NORMSP_1:def 3
.= ||.(f|Y)/.(q1.k) - ((f|Y)/*q2).k.|| by A33,FUNCT_2:109,A43
.= ||.(f|Y)/.(q1.k) - (f|Y)/.(q2.k) .|| by A23,FUNCT_2:109,A43
.= ||.f/.(q1.k) - (f|Y)/.(q2.k).|| by A33,A41,PARTFUN2:15
.= ||.f/.(q1.k) - f/.(q2.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;
end;
hence contradiction;
end;
theorem
for f be PartFunc of CNS1,CNS2, Y be Subset of CNS1 st Y c= dom f & Y
is compact & f is_uniformly_continuous_on Y holds f.:Y is compact by Th19,
NCFCONT1:83;
theorem
for f be PartFunc of CNS,RNS, Y be Subset of CNS st Y c= dom f & Y is
compact & f is_uniformly_continuous_on Y holds f.:Y is compact by Th20,
NCFCONT1:84;
theorem
for f be PartFunc of RNS,CNS, Y be Subset of RNS st Y c= dom f & Y is
compact & f is_uniformly_continuous_on Y holds f.:Y is compact by Th21,
NCFCONT1:85;
theorem
for f be PartFunc of the carrier of CNS,REAL, Y be Subset of CNS st Y
<> {} & Y c= dom f & Y is compact & f is_uniformly_continuous_on Y ex x1,x2 be
Point of CNS st x1 in Y & x2 in Y & f/.x1 = upper_bound (f.:Y) & f/.x2 =
lower_bound (f.:Y) by Th23,NCFCONT1:96;
theorem
for f be PartFunc of CNS1,CNS2 st X c= dom f & f|X is constant holds f
is_uniformly_continuous_on X by Th25,NCFCONT1:112;
theorem
for f be PartFunc of CNS,RNS st X c= dom f & f|X is constant holds f
is_uniformly_continuous_on X by Th26,NCFCONT1:113;
theorem
for f be PartFunc of RNS,CNS st X c= dom f & f|X is constant holds f
is_uniformly_continuous_on X by Th27,NCFCONT1:114;
begin :: Contraction Mapping Principle on Normed Complex Linear Spaces
definition
let M be non empty CNORMSTR;
let f be Function of M,M;
attr f is contraction means
:Def7:
ex L being Real st 0 < L & L < 1 & for x,y being Point of M holds
||.f.x - f.y.|| <=L*||.x - y.||;
end;
registration
let M be ComplexBanachSpace;
cluster contraction for Function of M,M;
existence
proof
set x = the Point of M;
reconsider f = (the carrier of M) --> x as Function of the carrier of M,
the carrier of M;
reconsider jd = 1/2 as Real;
take f, jd;
thus 0<jd & jd<1;
let z,y be Point of M;
f.z=x & f.y=x by FUNCOP_1:7;
then
A1: ||.f.z-f.y.|| = 0 by CLVECT_1:107;
||.z-y.||>=0 by CLVECT_1:105;
hence thesis by A1;
end;
end;
definition
let M be ComplexBanachSpace;
mode Contraction of M is contraction Function of M,M;
end;
theorem
for X be ComplexNormSpace, x,y be Point of X holds ||.x-y.|| > 0 iff x <> y
proof
let X be ComplexNormSpace;
let x, y be Point of X;
0 < ||.x-y.|| implies x-y <> 0.X by NORMSP_0:def 6;
hence 0 < ||.x-y.|| implies x <> y by RLVECT_1:15;
now
assume x <> y;
then 0 <> ||.x-y.|| by CLVECT_1:112;
hence 0 < ||.x-y.|| by CLVECT_1:105;
end;
hence thesis;
end;
theorem
for X be ComplexNormSpace, x, y be Point of X holds ||.x-y.|| = ||.y-x .||
proof
let X be ComplexNormSpace;
let x, y be Point of X;
thus ||.x-y.|| = ||.-(x-y).|| by CLVECT_1:103
.= ||.y-x.|| by RLVECT_1:33;
end;
Lm1: for X be ComplexNormSpace, x,y,z be Point of X,
e be Real holds ( ||.x-z
.|| <e/2 & ||.z-y.|| <e/2 implies ||.x-y.|| <e )
proof
let X be ComplexNormSpace;
let x,y,z be Point of X;
let e be Real;
assume ||.x-z.|| < e/2 & ||.z-y.|| < e/2;
then ||.x-z.|| + ||.z-y.|| < e/2 + e/2 by XREAL_1:8;
then ||.x-y.|| + (||.x-z.|| + ||.z-y.||) < (||.x-z.|| + ||.z-y.||) + e by
CLVECT_1:111,XREAL_1:8;
then ||.x-y.|| + (||.x-z.|| + ||.z-y.||) +- (||.x-z.|| + ||.z-y.||) < e + (
||.x-z.|| + ||.z-y.||) +- (||.x-z.|| + ||.z-y.||) by XREAL_1:8;
hence thesis;
end;
Lm2: for X be ComplexNormSpace, x,y,z be Point of X,
e be Real holds ||.x-z.||
<e/2 & ||.y-z.|| < e/2 implies ||.x-y.|| <e
proof
let X be ComplexNormSpace;
let x,y,z be Point of X;
let e be Real;
assume that
A1: ||.x-z.|| < e/2 and
A2: ||.y-z.|| < e/2;
||.-(y-z).|| < e/2 by A2,CLVECT_1:103;
then ||.z-y.|| < e/2 by RLVECT_1:33;
hence thesis by A1,Lm1;
end;
Lm3: for X be ComplexNormSpace, x be Point of X
st for e be Real st e>0 holds ||.x.|| <e
holds x=0.X
proof
let X be ComplexNormSpace;
let x be Point of X such that
A1: for e be Real st e > 0 holds ||.x.|| <e;
now
assume x<>0.X;
then 0 <> ||.x.|| by NORMSP_0:def 5;
then 0 < ||.x.|| by CLVECT_1:105;
hence contradiction by A1;
end;
hence thesis;
end;
Lm4: for X be ComplexNormSpace, x,y be Point of X
st for e be Real st e>0 holds ||.x-y.|| <e
holds x=y
proof
let X be ComplexNormSpace;
let x,y be Point of X;
assume for e be Real st e > 0 holds ||.x-y.|| <e;
then x-y = 0.X by Lm3;
hence thesis by RLVECT_1:21;
end;
theorem Th40:
for X be ComplexBanachSpace, f be Function of X,X st f is
Contraction of X ex xp be Point of X st f.xp=xp & for x be Point of X st f.x=x
holds xp=x
proof
let X be ComplexBanachSpace;
set x0 = the Element of X;
let f be Function of X,X;
assume f is Contraction of X;
then consider K be Real such that
A1: 0 < K and
A2: K < 1 and
A3: for x,y be Point of X holds ||.f.x - f.y.|| <= K*||.x - y.|| by Def7;
deffunc G(set,set)=f.$2;
consider g be Function such that
A4: dom g = NAT & g.0 = x0 & for n being Nat holds g.(n+1) = G(n,g.n)
from NAT_1:sch 11;
defpred P[Nat] means g.$1 in the carrier of X;
A5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A6: P[k];
g.(k+1)= f.(g.k) by A4;
hence thesis by A6,FUNCT_2:5;
end;
A7: P[0] by A4;
for n be Nat holds P[n] from NAT_1:sch 2(A7,A5);
then for n be object st n in NAT holds g.n in the carrier of X;
then reconsider g as sequence of X by A4,FUNCT_2:3;
A8: now
let n be Element of NAT;
||. (g^\1).n - f. (lim g) .|| = ||. g.(n+1) - f. (lim g) .|| by NAT_1:def 3
.= ||. f.(g.n)- f. (lim g) .|| by A4;
hence ||. (g^\1).n - f. (lim g) .|| <= K* ||. g.n - lim g .|| by A3;
end;
A9: for n be Nat holds ||.g.(n+1) - g.n .|| <= ||. g.1-g.0 .||*(K to_power n )
proof
defpred P[Nat] means ||.g.($1+1) - g.($1) .|| <= ||. g.1-g.0
.||* (K to_power $1 );
A10: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then
A11: K* ||. g.(k+1) - g.k .|| <= K*( ||. g.1-g.0 .||* (K to_power k ) )
by A1,XREAL_1:64;
||.f.(g.(k+1)) - f.(g.k) .|| <= K* ||. g.(k+1) - g.k .|| by A3;
then
||.f.(g.(k+1)) - f.(g.k) .|| <=||. g.1-g.0 .||*(K* (K to_power k ))
by A11,XXREAL_0:2;
then
A12: ||.f.(g.(k+1)) - f.(g.k) .|| <=||. g.1-g.0 .||*((K to_power 1)* (K
to_power k )) by POWER:25;
g.((k+1)+1) =f.(g.(k+1)) & g.(k+1) =f.(g.k) by A4;
hence thesis by A1,A12,POWER:27;
end;
||.g.(0+1) - g.0 .|| = ||. g.1-g.0 .|| * 1
.= ||. g.1-g.0 .|| * (K to_power 0 ) by POWER:24;
then
A13: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A13,A10);
hence thesis;
end;
A14: for k,n be Element of NAT holds ||.g.(n+k) - g.n .|| <= ||. g.1-g.0 .||
* ((K to_power n - K to_power (n+k)) /(1-K))
proof
defpred P[Nat] means
for n be Element of NAT holds ||.g.(n+$1)
- g.n .|| <= ||. g.1-g.0 .||*( (K to_power n-K to_power (n+$1)) /(1-K));
A15: now
let k be Nat such that
A16: P[k];
now
let n be Element of NAT;
1- K <> 0 by A2;
then
A17: ||. g.1-g.0 .||*((K to_power n - K to_power (n+k)) /(1-K)) + ||.
g.1-g.0 .||*(K to_power (n+k)) = ||. g.1-g.0 .||*((K to_power n - K to_power (n
+k))/(1-K)) + ||. g.1-g.0 .||*(K to_power (n+k))*(1-K)/(1-K) by XCMPLX_1:89
.= ||. g.1-g.0 .||*((K to_power n - K to_power (n+k))/(1-K)) + ||.
g.1-g.0 .||*((K to_power (n+k))*(1-K))/(1-K)
.= ||. g.1-g.0 .||*((K to_power n - K to_power (n+k))/(1-K)) + ||.
g.1-g.0 .||*((K to_power (n+k)*(1-K))/(1-K)) by XCMPLX_1:74
.= ||. g.1-g.0 .||*(((K to_power n - K to_power (n+k))/(1-K)) + ((
K to_power (n+k)*(1-K))/(1-K)))
.= ||. g.1-g.0 .||*((K to_power n - K to_power (n+k) + (1*K
to_power (n+k) - K*K to_power (n+k)) ) / (1-K)) by XCMPLX_1:62
.= ||. g.1-g.0 .||*((K to_power n- K*K to_power (n+k)) / (1-K))
.= ||. g.1-g.0 .||*((K to_power n- (K to_power 1) *K to_power (n+k
)) / (1-K)) by POWER:25
.= ||. g.1-g.0 .||*((K to_power n - K to_power (n+k+1))/(1-K)) by A1,
POWER:27;
||.g.(n+k) - g.n .|| <= ||. g.1-g.0 .||* ((K to_power n - K
to_power (n+k)) / (1-K)) & ||.g.((n+k)+1) - g.(n+k) .|| <= ||. g.1-g.0 .||* (K
to_power (n+k)) by A9,A16;
then
||.g.(n+(k+1)) - g.n .|| <= ||.g.(n+(k+1)) - g.(n+k) .|| + ||.g.(
n+k) - g.n .|| & ||.g.(n+(k+1)) - g.(n+k) .|| + ||.g.(n+k) - g.n .|| <= ||. g.1
-g.0 .|| * (K to_power (n+k)) + ||. g.1-g.0 .|| * ((K to_power n - K to_power (
n+k)) /(1-K )) by CLVECT_1:111,XREAL_1:7;
hence ||.g.(n+(k+1)) - g.n .|| <= ||. g.1-g.0 .||*((K to_power n - K
to_power (n+(k+1)))/(1-K)) by A17,XXREAL_0:2;
end;
hence P[k+1];
end;
now
let n be Element of NAT;
||.g.(n+0) - g.n .|| = ||.0.X.|| by RLVECT_1:15
.= 0 by CLVECT_1:102;
hence ||.g.(n+0) - g.n .|| <= ||. g.1-g.0 .||* ((K to_power n-K to_power
(n+0)) /(1-K));
end;
then
A18: P[0];
for k be Nat holds P[k] from NAT_1:sch 2(A18,A15);
hence thesis;
end;
A19: for k,n be Element of NAT holds ||.g.(n+k) - g.n .|| <= ||. g.1-g.0 .||
* (K to_power n/(1-K))
proof
let k be Element of NAT;
now
let n be Element of NAT;
A20: 0 <= ||. g.1-g.0 .|| by CLVECT_1:105;
K to_power (n+k) > 0 by A1,POWER:34;
then
A21: K to_power n - K to_power (n+k) <= K to_power n - 0 by XREAL_1:13;
1-K > 1-1 by A2,XREAL_1:15;
then
(K to_power n - K to_power (n+k)) /(1-K) <= (( K to_power n ) /(1-K
)) by A21,XREAL_1:72;
then
A22: ||. g.1-g.0 .|| * ((K to_power n - K to_power (n+k)) /(1-K)) <= ||.
g.1-g.0 .|| * ((K to_power n) /(1-K)) by A20,XREAL_1:64;
||.g.(n+k) - g.n .|| <= ||. g.1-g.0 .||*( (K to_power n - K
to_power (n+k)) /(1-K)) by A14;
hence
||.g.(n+k) - g.n .|| <= ||. g.1-g.0 .||* ((K to_power n) /(1-K)) by A22,
XXREAL_0:2;
end;
hence thesis;
end;
now
let e be Real such that
A23: e >0;
e/2 > 0 by A23;
then consider n be Nat such that
A24: |. ||. g.1-g.0 .||/(1-K)* (K to_power n) .| < e/2 by A1,A2,NFCONT_2:16;
reconsider nn=n+1 as Nat;
take nn;
||. g.1-g.0 .||/(1-K)* (K to_power n) <= |. ||. g.1-g.0 .||/(1-K)*
(K to_power n) .| by ABSVALUE:4;
then ||. g.1-g.0 .||/(1-K)* (K to_power n) < e/2 by A24,XXREAL_0:2;
then
A25: ||. g.1-g.0 .|| *( (K to_power n)/(1-K)) < e/2 by XCMPLX_1:75;
now
let m,l be Nat such that
A26: nn <= m and
A27: nn <= l;
n < m by A26,NAT_1:13;
then consider k1 being Nat such that
A28: n+k1 =m by NAT_1:10;
n < l by A27,NAT_1:13;
then consider k2 being Nat such that
A29: n+k2 =l by NAT_1:10;
reconsider k2 as Nat;
A30: n in NAT by ORDINAL1:def 12;
A31: k2 in NAT by ORDINAL1:def 12;
||.g.(n+k2) - g.n .|| <= ||. g.1-g.0 .||*( (K to_power n) /(1-K) )
by A19,A30,A31;
then
A32: ||.g.l - g.n .|| < e/2 by A25,A29,XXREAL_0:2;
reconsider k1 as Element of NAT by ORDINAL1:def 12;
||.g.(n+k1) - g.n .|| <= ||. g.1-g.0 .||*( (K to_power n) /(1-K))
by A19,A30;
then ||.g.m - g.n .|| < e/2 by A25,A28,XXREAL_0:2;
hence ||.g.l - g.m .|| < e by A32,Lm2;
end;
hence
for n, m be Nat st n >= nn & m >= nn holds ||.g.n - g.m.|| < e;
end;
then g is Cauchy_sequence_by_Norm by CSSPACE3:8;
then
A33: g is convergent by CLOPBAN1:def 13;
then
A34: K(#)||. g - lim g .|| is convergent by CLVECT_1:118,SEQ_2:7;
A35: lim (K(#)(||.g - lim g.||)) =K*lim ||.(g - lim g).|| by A33,CLVECT_1:118
,SEQ_2:8
.=K*0 by A33,CLVECT_1:118
.=0;
A36: for e be Real
st e >0 ex n be Nat st for m be Nat
st n<=m holds ||. (g^\1).m - f. (lim g) .|| <e
proof
let e be Real;
assume e >0;
then consider n be Nat such that
A37: for m be Nat st n<=m holds |. (K(#)||. g - lim g .||
).m-0 .| < e by A34,A35,SEQ_2:def 7;
take n;
now
let m be Nat;
A38: m in NAT by ORDINAL1:def 12;
assume n<=m;
then |. (K(#)||. g - lim g .||).m-0 .|<e by A37;
then |. K*||. g - lim g .||.m.| < e by SEQ_1:9;
then |. K*||. (g - lim g).m .||.| < e by NORMSP_0:def 4;
then
A39: |. K*||. g.m - lim g .||.| < e by NORMSP_1:def 4;
K*||. g.m - lim g .|| <=|. K*||. g.m - lim g .||.| by ABSVALUE:4;
then
A40: K*||. g.m - lim g .|| < e by A39,XXREAL_0:2;
||. (g^\1).m - f. (lim g) .|| <= K* ||. g.m - lim g .|| by A8,A38;
hence ||. (g^\1).m - f. (lim g) .|| < e by A40,XXREAL_0:2;
end;
hence thesis;
end;
take xp=lim g;
A41: g^\1 is convergent & lim (g^\1) = lim g by A33,CLOPBAN3:9;
then
A42: lim g = f.(lim g) by A36,CLVECT_1:def 16;
now
let x be Point of X such that
A43: f.x=x;
A44: for k be Element of NAT holds ||.x-xp.|| <= ||.x-xp.||*(K to_power k)
proof
defpred P[Nat] means ||.x-xp .|| <= ||.x-xp.||*(K to_power $1);
A45: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then
A46: K* ||. x-xp .|| <= K*( ||.x-xp.||*(K to_power k) ) by A1,XREAL_1:64;
||.f.x - f.xp .|| <= K* ||. x-xp .|| by A3;
then ||.f.x - f.xp .|| <= ||. x-xp .||*(K* (K to_power k )) by A46,
XXREAL_0:2;
then ||.f.x - f.xp .|| <= ||. x-xp .||*((K to_power 1)* (K to_power k
)) by POWER:25;
hence thesis by A1,A42,A43,POWER:27;
end;
||.x-xp .|| = ||. x-xp .|| * 1
.= ||. x-xp .|| * (K to_power 0 ) by POWER:24;
then
A47: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A47,A45);
hence thesis;
end;
for e be Real st 0 <e holds ||.x-xp.|| < e
proof
let e be Real;
assume 0 < e;
then consider n be Nat such that
A48: |. ||.x-xp.||*(K to_power n) .| < e by A1,A2,NFCONT_2:16;
A49: n in NAT by ORDINAL1:def 12;
||.x-xp.||*(K to_power n) <=|. ||.x-xp.||*(K to_power n) .| by
ABSVALUE:4;
then
A50: ||.x-xp.||*(K to_power n) <e by A48,XXREAL_0:2;
||.x-xp.|| <= ||.x-xp.||*(K to_power n) by A44,A49;
hence thesis by A50,XXREAL_0:2;
end;
hence x=xp by Lm4;
end;
hence thesis by A41,A36,CLVECT_1:def 16;
end;
theorem
for X be ComplexBanachSpace for f be Function of X,X st ex n0 be
Element of NAT st iter(f,n0) is Contraction of X holds ex xp be Point of X st f
.xp=xp & for x be Point of X st f.x=x holds xp=x
proof
let X be ComplexBanachSpace;
let f be Function of X, X;
given n0 be Element of NAT such that
A1: iter(f,n0) is Contraction of X;
consider xp be Point of X such that
A2: (iter(f,n0)).xp=xp and
A3: for x be Point of X st iter(f,n0).x=x holds xp=x by A1,Th40;
A4: now
let x be Point of X such that
A5: f.x=x;
for n be Element of NAT holds (iter(f,n)).x=x
proof
defpred P[Nat] means (iter(f,$1)).x=x;
A6: now
let n be Nat such that
A7: P[n];
A8: iter(f,n) is Function of X,X by FUNCT_7:83;
(iter(f,n+1)).x =(f*iter(f,n)).x by FUNCT_7:71
.=x by A5,A7,A8,FUNCT_2:15;
hence P[n+1];
end;
(iter(f,0)).x=(id the carrier of X).x by FUNCT_7:84
.=x;
then
A9: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A9,A6);
hence thesis;
end;
then (iter(f,n0)).x=x;
hence xp=x by A3;
end;
A10: iter(f,n0) is Function of X,X by FUNCT_7:83;
(iter(f,n0)).(f.xp) =(iter(f,n0)*f).xp by FUNCT_2:15
.=(iter(f,n0+1)).xp by FUNCT_7:69
.=(f*iter(f,n0)).xp by FUNCT_7:71
.=f.xp by A2,A10,FUNCT_2:15;
then f.xp=xp by A3;
hence thesis by A4;
end;