:: Property of Complex Sequence and Continuity of Complex Function
:: by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama
::
:: Received December 7, 1999
:: Copyright (c) 1999-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, SUBSET_1, COMSEQ_1, PARTFUN1, REAL_1, ORDINAL2, NAT_1,
SEQ_1, FCONT_1, RELAT_1, TARSKI, SEQ_2, FUNCT_2, ARYTM_1, FUNCT_1,
ARYTM_3, VALUED_1, COMPLEX1, XBOOLE_0, ORDINAL4, VALUED_0, CARD_1,
XXREAL_0, XREAL_0, RCOMP_1, CFCONT_1, XCMPLX_0, ZFMISC_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, FUNCT_1, ORDINAL1, NUMBERS,
XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, PARTFUN1, FUNCT_2, SEQ_1,
RELSET_1, VALUED_0, VALUED_1, CFUNCT_1, COMSEQ_1, COMSEQ_2, COMSEQ_3,
XXREAL_0, RECDEF_1;
constructors ZFMISC_1, PARTFUN1, XXREAL_0, REAL_1, NAT_1, COMSEQ_2, CFUNCT_1,
COMSEQ_3, RECDEF_1, SEQM_3, VALUED_1, RELSET_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS,
XREAL_0, NAT_1, MEMBERED, VALUED_0, VALUED_1, COMSEQ_2, XCMPLX_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, COMSEQ_2;
equalities VALUED_1;
expansions TARSKI, COMSEQ_2;
theorems TARSKI, NAT_1, FUNCT_1, COMPLEX1, SEQ_1, SEQM_3, SEQ_4, COMSEQ_1,
COMSEQ_2, COMSEQ_3, PARTFUN1, CFUNCT_1, RELAT_1, FUNCT_2, PARTFUN2,
XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, VALUED_1,
VALUED_0, XCMPLX_0;
schemes NAT_1, RECDEF_1, FUNCT_2;
begin
reserve n,n1,m,m1,k for Nat;
reserve x,X,X1 for set;
reserve g,g1,g2,t,x0,x1,x2 for Complex;
reserve s1,s2,q1,seq,seq1,seq2,seq3 for Complex_Sequence;
reserve Y for Subset of COMPLEX;
reserve f,f1,f2,h,h1,h2 for PartFunc of COMPLEX,COMPLEX;
reserve p,r,s for Real;
reserve Ns,Nseq for increasing sequence of NAT;
::
:: COMPLEX SEQUENCE
::
definition
let f,x0;
pred f is_continuous_in x0 means
x0 in dom f & for s1 st rng s1 c=
dom f & s1 is convergent & lim s1 = x0 holds f/*s1 is convergent & f/.x0 = lim
(f/*s1);
end;
theorem Th1:
seq1=seq2-seq3 iff for n holds seq1.n=seq2.n-seq3.n
proof
thus seq1=seq2-seq3 implies for n holds seq1.n=seq2.n-seq3.n
proof
assume
A1: seq1=seq2-seq3;
now
let n;
A2: n in NAT by ORDINAL1:def 12;
seq1.n=seq2.n+(-seq3).n by A1,VALUED_1:1,A2;
then seq1.n=seq2.n+(-seq3.n) by VALUED_1:8;
hence seq1.n=seq2.n-seq3.n;
end;
hence thesis;
end;
assume
A3: for n holds seq1.n=seq2.n-seq3.n;
now
let n be Element of NAT;
thus seq1.n = seq2.n-seq3.n by A3
.= seq2.n+-seq3.n
.= seq2.n+(-seq3).n by VALUED_1:8
.= (seq2+(-seq3)).n by VALUED_1:1;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th2:
(seq1 + seq2)*Ns = (seq1*Ns) + (seq2*Ns) & (seq1 - seq2)*Ns = (
seq1*Ns) - (seq2*Ns) & (seq1 (#) seq2)*Ns = (seq1*Ns) (#) (seq2*Ns)
proof
now
let n be Element of NAT;
thus ((seq1 + seq2)*Ns).n = (seq1 + seq2).(Ns.n) by FUNCT_2:15
.= seq1.(Ns.n) + seq2.(Ns.n) by VALUED_1:1
.= (seq1*Ns).n + seq2.(Ns.n) by FUNCT_2:15
.= (seq1*Ns).n + (seq2*Ns).n by FUNCT_2:15
.= (seq1*Ns + seq2*Ns).n by VALUED_1:1;
end;
hence (seq1 + seq2)*Ns = (seq1*Ns) + (seq2*Ns) by FUNCT_2:63;
now
let n be Element of NAT;
thus ((seq1 - seq2)*Ns).n = (seq1 - seq2).(Ns.n) by FUNCT_2:15
.= seq1.(Ns.n) - seq2.(Ns.n) by Th1
.= (seq1*Ns).n - seq2.(Ns.n) by FUNCT_2:15
.= (seq1*Ns).n - (seq2*Ns).n by FUNCT_2:15
.= (seq1*Ns - seq2*Ns).n by Th1;
end;
hence (seq1 - seq2)*Ns = (seq1*Ns) - (seq2*Ns) by FUNCT_2:63;
now
let n be Element of NAT;
thus ((seq1 (#) seq2)*Ns).n = (seq1 (#) seq2).(Ns.n) by FUNCT_2:15
.= seq1.(Ns.n) * seq2.(Ns.n) by VALUED_1:5
.= (seq1*Ns).n * seq2.(Ns.n) by FUNCT_2:15
.= (seq1*Ns).n * (seq2*Ns).n by FUNCT_2:15
.= ((seq1*Ns)(#)(seq2*Ns)).n by VALUED_1:5;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th3:
(g(#)seq)*Ns = g(#)(seq*Ns)
proof
now
let n be Element of NAT;
thus ((g(#)seq)*Ns).n = (g(#)seq).(Ns.n) by FUNCT_2:15
.= g*(seq.(Ns.n)) by VALUED_1:6
.= g*((seq*Ns).n) by FUNCT_2:15
.= (g(#)(seq*Ns)).n by VALUED_1:6;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(-seq)*Ns = -(seq*Ns) & (|.seq.|)*Ns = |.(seq*Ns).|
proof
thus (-seq)*Ns = ((-1r)(#)seq)*Ns by COMSEQ_1:11
.= (-1r)(#)(seq*Ns) by Th3
.= -(seq*Ns) by COMSEQ_1:11;
now
let n be Element of NAT;
thus ((|.seq.|)*Ns).n = (|.seq.|).(Ns.n) by FUNCT_2:15
.= |.seq.(Ns.n).| by VALUED_1:18
.= |.(seq*Ns).n.| by FUNCT_2:15
.= (|.seq*Ns.|).n by VALUED_1:18;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th5:
(seq*Ns)" = (seq")*Ns
proof
now
let n be Element of NAT;
thus ((seq*Ns)").n = ((seq*Ns).n)" by VALUED_1:10
.= (seq.(Ns.n))" by FUNCT_2:15
.= (seq").(Ns.n) by VALUED_1:10
.= ((seq")*Ns).n by FUNCT_2:15;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(seq1/"seq)*Ns = (seq1*Ns)/"(seq*Ns)
proof
thus (seq1/"seq)*Ns = (seq1*Ns)(#)((seq")*Ns) by Th2
.= (seq1*Ns)/"(seq*Ns) by Th5;
end;
theorem Th7:
rng seq c= dom h1 /\ dom h2 implies (h1+h2)/*seq=h1/*seq+h2/*seq
& (h1-h2)/*seq=h1/*seq-h2/*seq & (h1(#)h2)/*seq=(h1/*seq)(#)(h2/*seq)
proof
A1: dom h1 /\ dom h2 c= dom h1 by XBOOLE_1:17;
A2: dom h1 /\ dom h2 c= dom h2 by XBOOLE_1:17;
assume
A3: rng seq c= dom h1 /\ dom h2;
then
A4: rng seq c= dom (h1 + h2) by VALUED_1:def 1;
now
let n be Element of NAT;
A5: seq.n in rng seq by VALUED_0:28;
thus ((h1+h2)/*seq).n = (h1+h2)/.(seq.n) by A4,FUNCT_2:109
.= h1/.(seq.n) + h2/.(seq.n) by A4,A5,CFUNCT_1:1
.= (h1/*seq).n + h2/.(seq.n) by A3,A1,FUNCT_2:109,XBOOLE_1:1
.= (h1/*seq).n + (h2/*seq).n by A3,A2,FUNCT_2:109,XBOOLE_1:1
.= ((h1/*seq)+(h2/*seq)).n by VALUED_1:1;
end;
hence (h1+h2)/*seq=(h1/*seq)+(h2/*seq) by FUNCT_2:63;
A6: rng seq c= dom (h1 - h2) by A3,CFUNCT_1:2;
now
let n;
A7: n in NAT by ORDINAL1:def 12;
A8: seq.n in rng seq by VALUED_0:28;
thus ((h1-h2)/*seq).n = (h1-h2)/.(seq.n) by A6,FUNCT_2:109,A7
.= h1/.(seq.n) - h2/.(seq.n) by A6,A8,CFUNCT_1:2
.= (h1/*seq).n - h2/.(seq.n) by A3,A1,FUNCT_2:109,XBOOLE_1:1,A7
.= (h1/*seq).n - (h2/*seq).n by A3,A2,FUNCT_2:109,XBOOLE_1:1,A7;
end;
hence (h1-h2)/*seq=h1/*seq-h2/*seq by Th1;
A9: rng seq c= dom (h1 (#) h2) by A3,VALUED_1:def 4;
now
let n be Element of NAT;
A10: seq.n in rng seq by VALUED_0:28;
thus ((h1(#)h2)/*seq).n = (h1(#)h2)/.(seq.n) by A9,FUNCT_2:109
.= (h1/.(seq.n)) * (h2/.(seq.n)) by A9,A10,CFUNCT_1:3
.= ((h1/*seq).n) * (h2/.(seq.n)) by A3,A1,FUNCT_2:109,XBOOLE_1:1
.= ((h1/*seq).n) * ((h2/*seq).n) by A3,A2,FUNCT_2:109,XBOOLE_1:1
.= ((h1/*seq)(#)(h2/*seq)).n by VALUED_1:5;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th8:
rng seq c= dom h implies (g(#)h)/*seq = g(#)(h/*seq)
proof
assume
A1: rng seq c= dom h;
then
A2: rng seq c= dom (g(#)h) by VALUED_1:def 5;
now
let n be Element of NAT;
A3: seq.n in rng seq by VALUED_0:28;
thus ((g(#)h)/*seq).n = (g(#)h)/.(seq.n) by A2,FUNCT_2:109
.= g * (h/.(seq.n)) by A2,A3,CFUNCT_1:4
.= g *((h/*seq).n) by A1,FUNCT_2:109
.= (g(#)(h/*seq)).n by VALUED_1:6;
end;
hence thesis by FUNCT_2:63;
end;
theorem
rng seq c= dom h implies -(h/*seq) = (-h)/*seq
by Th8;
theorem Th10:
rng seq c= dom (h^) implies h/*seq is non-zero
proof
assume
A1: rng seq c= dom (h^);
then
A2: dom h \ h"{0c} c= dom h & rng seq c= dom h \ h"{0c} by CFUNCT_1:def 2
,XBOOLE_1:36;
now
given n being Element of NAT such that
A3: (h/*seq).n=0c;
seq.n in rng seq by VALUED_0:28;
then seq.n in dom (h^) by A1;
then seq.n in dom h \ h"{0c} by CFUNCT_1:def 2;
then seq.n in dom h & not seq.n in h"{0c} by XBOOLE_0:def 5;
then
A4: not h/.(seq.n) in {0c} by PARTFUN2:26;
h/.(seq.n) =0c by A2,A3,FUNCT_2:109,XBOOLE_1:1;
hence contradiction by A4,TARSKI:def 1;
end;
hence thesis by COMSEQ_1:4;
end;
theorem Th11:
rng seq c= dom (h^) implies (h^)/*seq =(h/*seq)"
proof
assume
A1: rng seq c= dom (h^);
then
A2: dom h \ h"{0c} c= dom h & rng seq c= dom h \ h"{0c} by CFUNCT_1:def 2
,XBOOLE_1:36;
now
let n be Element of NAT;
A3: seq.n in rng seq by VALUED_0:28;
thus ((h^)/*seq).n = (h^)/.(seq.n) by A1,FUNCT_2:109
.= (h/.(seq.n))" by A1,A3,CFUNCT_1:def 2
.= ((h/*seq).n)" by A2,FUNCT_2:109,XBOOLE_1:1
.= ((h/*seq)").n by VALUED_1:10;
end;
hence thesis by FUNCT_2:63;
end;
theorem
rng seq c= dom h implies Re ( (h/*seq)*Ns ) = Re (h/*(seq*Ns))
proof
assume
A1: rng seq c= dom h;
now
let n be Element of NAT;
(seq * Ns) is subsequence of seq by VALUED_0:def 17;
then
A2: rng (seq*Ns) c= rng seq by VALUED_0:21;
thus (Re ( (h/*seq)*Ns )).n = Re( ((h/*seq)*Ns).n ) by COMSEQ_3:def 5
.= Re( (h/*seq).(Ns.n) ) by FUNCT_2:15
.= Re( h/.(seq.(Ns.n)) ) by A1,FUNCT_2:109
.=Re( h/.((seq*Ns).n) ) by FUNCT_2:15
.=Re( (h/*(seq*Ns)).n ) by A1,A2,FUNCT_2:109,XBOOLE_1:1
.=(Re (h/*(seq*Ns)) ).n by COMSEQ_3:def 5;
end;
hence thesis by FUNCT_2:63;
end;
theorem
rng seq c= dom h implies Im ( (h/*seq)*Ns ) = Im (h/*(seq*Ns))
proof
assume
A1: rng seq c= dom h;
now
let n be Element of NAT;
(seq * Ns) is subsequence of seq by VALUED_0:def 17;
then
A2: rng (seq*Ns) c= rng seq by VALUED_0:21;
thus (Im ( (h/*seq)*Ns )).n = Im( ((h/*seq)*Ns).n ) by COMSEQ_3:def 6
.= Im( (h/*seq).(Ns.n) ) by FUNCT_2:15
.= Im( h/.(seq.(Ns.n)) ) by A1,FUNCT_2:109
.=Im( h/.((seq*Ns).n) ) by FUNCT_2:15
.=Im( (h/*(seq*Ns)).n ) by A1,A2,FUNCT_2:109,XBOOLE_1:1
.=(Im (h/*(seq*Ns)) ).n by COMSEQ_3:def 6;
end;
hence thesis by FUNCT_2:63;
end;
theorem
h1 is total & h2 is total implies (h1+h2)/*seq = h1/*seq + h2/*seq & (
h1-h2)/*seq = h1/*seq - h2/*seq & (h1(#)h2)/*seq = (h1/*seq) (#) (h2/*seq)
proof
assume h1 is total & h2 is total;
then dom (h1+h2) = COMPLEX by PARTFUN1:def 2;
then dom h1 /\ dom h2 = COMPLEX by VALUED_1:def 1;
then
A1: rng seq c= dom h1 /\ dom h2;
hence (h1+h2)/*seq = h1/*seq + h2/*seq by Th7;
thus (h1-h2)/*seq = h1/*seq - h2/*seq by A1,Th7;
thus thesis by A1,Th7;
end;
theorem
h is total implies (g(#)h)/*seq = g(#)(h/*seq)
proof
assume h is total;
then dom h = COMPLEX by PARTFUN1:def 2;
then rng seq c= dom h;
hence thesis by Th8;
end;
theorem
rng seq c= dom (h|X) & h"{0}={} implies ((h^)|X)/*seq = ((h|X)/*seq)"
proof
assume that
A1: rng seq c= dom (h|X) and
A2: h"{0}={};
now
let x be object;
assume x in rng seq;
then x in dom (h|X) by A1;
then
A3: x in dom h /\ X by RELAT_1:61;
then x in dom h \ h"{0c} by A2,XBOOLE_0:def 4;
then
A4: x in dom (h^) by CFUNCT_1:def 2;
x in X by A3,XBOOLE_0:def 4;
then x in dom (h^) /\ X by A4,XBOOLE_0:def 4;
hence x in dom ((h^)|X) by RELAT_1:61;
end;
then
A5: rng seq c= dom ((h^)|X);
now
let n be Element of NAT;
A6: seq.n in rng seq by VALUED_0:28;
then seq.n in dom (h|X) by A1;
then
A7: seq.n in dom h /\ X by RELAT_1:61;
then seq.n in dom h \ h"{0c} by A2,XBOOLE_0:def 4;
then
A8: seq.n in dom (h^) by CFUNCT_1:def 2;
seq.n in X by A7,XBOOLE_0:def 4;
then seq.n in dom (h^) /\ X by A8,XBOOLE_0:def 4;
then
A9: seq.n in dom((h^)|X) by RELAT_1:61;
thus (((h^)|X)/*seq).n = ((h^)|X)/.(seq.n) by A5,FUNCT_2:109
.= (h^)/.(seq.n) by A9,PARTFUN2:15
.= (h/.(seq.n))" by A8,CFUNCT_1:def 2
.= ((h|X)/.(seq.n))" by A1,A6,PARTFUN2:15
.= (((h|X)/*seq).n)" by A1,FUNCT_2:109
.= (((h|X)/*seq)").n by VALUED_1:10;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th17:
seq1 is subsequence of seq & seq is convergent implies seq1 is convergent
proof
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent;
consider g being Complex such that
A3: for p st 0<p ex n st for m st n<=m holds |.(seq.m)-g.|<p by A2;
take t=g;
let p;
assume 0<p;
then consider n1 such that
A4: for m st n1<=m holds |.(seq.m)-g.|<p by A3;
take n=n1;
let m such that
A5: n<=m;
consider Nseq such that
A6: seq1=seq*Nseq by A1,VALUED_0:def 17;
m<=Nseq.m by SEQM_3:14;
then
A7: n<=Nseq.m by A5,XXREAL_0:2;
m in NAT by ORDINAL1:def 12;
then seq1.m=seq.(Nseq.m) by A6,FUNCT_2:15;
hence |.(seq1.m)-t.|<p by A4,A7;
end;
theorem Th18:
seq1 is subsequence of seq & seq is convergent implies lim seq1= lim seq
proof
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent;
consider Nseq such that
A3: seq1=seq*Nseq by A1,VALUED_0:def 17;
A4: now
let p;
assume 0<p;
then consider n1 such that
A5: for m st n1<=m holds |.(seq.m)-(lim seq).|<p by A2,COMSEQ_2:def 6;
take n=n1;
let m such that
A6: n<=m;
m<=Nseq.m by SEQM_3:14;
then
A7: n<=Nseq.m by A6,XXREAL_0:2;
A8: m in NAT by ORDINAL1:def 12;
seq1.m=seq.(Nseq.m) by A3,FUNCT_2:15,A8;
hence |.(seq1.m)-(lim seq).|<p by A5,A7;
end;
seq1 is convergent by A1,A2,Th17;
hence thesis by A4,COMSEQ_2:def 6;
end;
theorem Th19:
seq is convergent & (ex k st for n st k<=n holds seq1.n=seq.n)
implies seq1 is convergent
proof
assume that
A1: seq is convergent and
A2: ex k st for n st k<=n holds seq1.n=seq.n;
consider g1 being Complex such that
A3: for p st 0<p ex n st for m st n<=m holds |.(seq.m)-g1.|<p by A1;
consider k such that
A4: for n st k<=n holds seq1.n=seq.n by A2;
take g=g1;
let p;
assume 0<p;
then consider n1 such that
A5: for m st n1<=m holds |.(seq.m)-g1.|<p by A3;
A6: now
assume
A7: n1<=k;
take n=k;
let m;
assume
A8: n<=m;
then n1<=m by A7,XXREAL_0:2;
then |.(seq.m)-g1.|<p by A5;
hence |.(seq1.m)-g.|<p by A4,A8;
end;
now
assume
A9: k<=n1;
take n=n1;
let m;
assume
A10: n<=m;
then seq1.m=seq.m by A4,A9,XXREAL_0:2;
hence |.(seq1.m)-g.|<p by A5,A10;
end;
hence ex n st for m st n<=m holds |.seq1.m-g.|<p by A6;
end;
theorem
seq is convergent & (ex k st for n st k<=n holds seq1.n=seq.n) implies
lim seq=lim seq1
proof
assume that
A1: seq is convergent and
A2: ex k st for n st k<=n holds seq1.n=seq.n;
consider k such that
A3: for n st k<=n holds seq1.n=seq.n by A2;
A4: now
let p;
assume 0<p;
then consider n1 such that
A5: for m st n1<=m holds |.(seq.m)-(lim seq).|<p by A1,COMSEQ_2:def 6;
A6: now
assume
A7: n1<=k;
take n=k;
let m;
assume
A8: n<=m;
then n1<=m by A7,XXREAL_0:2;
then |.(seq.m)-(lim seq).|<p by A5;
hence |.(seq1.m)-(lim seq).|<p by A3,A8;
end;
now
assume
A9: k<=n1;
take n=n1;
let m;
assume
A10: n<=m;
then seq1.m=seq.m by A3,A9,XXREAL_0:2;
hence |.(seq1.m)-(lim seq).|<p by A5,A10;
end;
hence ex n st for m st n<=m holds |.seq1.m-(lim seq).|<p by A6;
end;
seq1 is convergent by A1,A2,Th19;
hence thesis by A4,COMSEQ_2:def 6;
end;
theorem
seq is convergent implies (seq ^\k) is convergent & lim (seq ^\k)=lim
seq by Th17,Th18;
theorem Th22:
seq is convergent & (ex k st seq=seq1 ^\k) implies seq1 is convergent
proof
assume that
A1: seq is convergent and
A2: ex k st seq=seq1 ^\k;
consider k such that
A3: seq=seq1 ^\k by A2;
consider g1 being Complex such that
A4: for p st 0<p ex n st for m st n<=m holds |.seq.m-g1.|<p by A1;
take g=g1;
let p;
assume 0<p;
then consider n1 such that
A5: for m st n1<=m holds |.seq.m-g1.|<p by A4;
take n=n1+k;
let m;
assume
A6: n<=m;
then consider l being Nat such that
A7: m=n1+k+l by NAT_1:10;
reconsider l as Element of NAT by ORDINAL1:def 12;
m-k=n1+l+k+-k by A7;
then consider m1 such that
A8: m1=m-k;
now
assume not n1<=m1;
then m1+k<n1+k by XREAL_1:6;
hence contradiction by A6,A8;
end;
then
A9: |.seq.m1-g1.|<p by A5;
m1+k=m by A8;
hence |.seq1.m-g.|<p by A3,A9,NAT_1:def 3;
end;
theorem
seq is convergent & (ex k st seq=seq1 ^\k) implies lim seq1 =lim seq
proof
assume that
A1: seq is convergent and
A2: ex k st seq=seq1 ^\k;
consider k such that
A3: seq=seq1 ^\k by A2;
A4: now
let p;
assume 0<p;
then consider n1 such that
A5: for m st n1<=m holds |.seq.m-(lim seq).|<p by A1,COMSEQ_2:def 6;
take n=n1+k;
let m;
assume
A6: n<=m;
then consider l being Nat such that
A7: m=n1+k+l by NAT_1:10;
reconsider l as Element of NAT by ORDINAL1:def 12;
m-k=n1+l+k+-k by A7;
then consider m1 such that
A8: m1=m-k;
now
assume not n1<=m1;
then m1+k<n1+k by XREAL_1:6;
hence contradiction by A6,A8;
end;
then
A9: |.seq.m1-(lim seq).|<p by A5;
m1+k=m by A8;
hence |.seq1.m-(lim seq).|<p by A3,A9,NAT_1:def 3;
end;
seq1 is convergent by A1,A2,Th22;
hence thesis by A4,COMSEQ_2:def 6;
end;
theorem Th24:
seq is convergent & lim seq<>0 implies ex k st (seq ^\k) is non-zero
proof
assume that
A1: seq is convergent and
A2: lim seq<>0;
consider n1 such that
A3: for m st n1<=m holds |.(lim seq).|/2<|.(seq.m).| by A1,A2,COMSEQ_2:33;
take k=n1;
now
let n be Element of NAT;
0+k<=n+k by XREAL_1:7;
then |.(lim seq).|/2<|.(seq.(n+k)).| by A3;
then
A4: |.(lim seq).|/2<|.((seq ^\k).n).| by NAT_1:def 3;
0<|.(lim seq).| by A2,COMPLEX1:47;
then 0/2<|.(lim seq).|/2 by XREAL_1:74;
then 0 <|.((seq ^\k).n).| by A4;
hence (seq ^\k).n<>0c by COMPLEX1:47;
end;
hence thesis by COMSEQ_1:4;
end;
theorem
seq is convergent & lim seq<>0 implies ex seq1 st seq1 is subsequence
of seq & seq1 is non-zero
proof
assume seq is convergent & lim seq <>0;
then consider k such that
A1: seq ^\k is non-zero by Th24;
take seq ^\k;
thus thesis by A1;
end;
theorem Th26:
seq is constant implies seq is convergent
proof
assume seq is constant;
then consider t being Element of COMPLEX such that
A1: for n being Nat holds seq.n=t by VALUED_0:def 18;
take g=t;
let p such that
A2: 0<p;
take n=0;
let m such that
n<=m;
|.(seq.m)-g.|=|.t-g.| by A1
.=0 by COMPLEX1:44;
hence |.(seq.m)-g.|<p by A2;
end;
theorem Th27:
(seq is constant & g in rng seq or seq is constant & ex n st seq
.n=g ) implies lim seq=g
proof
A1: now
assume that
A2: seq is constant and
A3: g in rng seq;
consider g1 being Element of COMPLEX such that
A4: rng seq={g1} by A2,FUNCT_2:111;
consider g2 being Element of COMPLEX such that
A5: for n being Nat holds seq.n=g2 by A2,VALUED_0:def 18;
A6: g=g1 by A3,A4,TARSKI:def 1;
A7: now
let p such that
A8: 0<p;
reconsider n=0 as Nat;
take n;
let m such that
n<=m;
m in NAT by ORDINAL1:def 12;
then m in dom seq by COMSEQ_1:2;
then seq.m in rng seq by FUNCT_1:def 3;
then g2 in rng seq by A5;
then g2=g by A4,A6,TARSKI:def 1;
then seq.m=g by A5;
hence |.(seq.m)-g.|<p by A8,COMPLEX1:44;
end;
seq is convergent by A2,Th26;
hence thesis by A7,COMSEQ_2:def 6;
end;
A9: now
assume that
seq is constant and
A10: ex n st seq.n=g;
consider n such that
A11: seq.n=g by A10;
n in NAT by ORDINAL1:def 12;
then n in dom seq by COMSEQ_1:2;
hence thesis by A1,A11,FUNCT_1:def 3;
end;
assume seq is constant & g in rng seq or seq is constant &
ex n being Nat st seq.n=g;
hence thesis by A1,A9;
end;
theorem
seq is constant implies for n holds lim seq=seq.n by Th27;
theorem
seq is convergent & lim seq<>0 implies for seq1 st seq1 is subsequence
of seq & seq1 is non-zero holds lim (seq1")=(lim seq)"
proof
assume that
A1: seq is convergent and
A2: lim seq<>0;
let seq1 such that
A3: seq1 is subsequence of seq and
A4: seq1 is non-zero;
lim seq1=lim seq by A1,A3,Th18;
hence thesis by A1,A2,A3,A4,Th17,COMSEQ_2:35;
end;
theorem
seq is constant & seq1 is convergent implies lim (seq+seq1) =(seq.0) +
lim seq1 & lim (seq-seq1) =(seq.0) - lim seq1 & lim (seq1-seq) =(lim seq1) -seq
.0 & lim (seq(#)seq1) =(seq.0) * (lim seq1)
proof
assume that
A1: seq is constant and
A2: seq1 is convergent;
A3: seq is convergent by A1,Th26;
hence lim (seq+seq1) =(lim seq)+(lim seq1) by A2,COMSEQ_2:14
.=(seq.0)+(lim seq1) by A1,Th27;
thus lim (seq-seq1) =(lim seq)-(lim seq1) by A2,A3,COMSEQ_2:26
.=(seq.0)-(lim seq1) by A1,Th27;
thus lim (seq1-seq) =(lim seq1)-(lim seq) by A2,A3,COMSEQ_2:26
.=(lim seq1)-(seq.0) by A1,Th27;
thus lim (seq(#)seq1) =(lim seq)*(lim seq1) by A2,A3,COMSEQ_2:30
.=(seq.0)*(lim seq1) by A1,Th27;
end;
scheme
CompSeqChoice { P[object,object] }: ex s1 st for n holds P[n,s1.n]
provided
A1: for n ex g st P[n,g]
proof
A2: for t being Element of NAT
ex ff being Element of COMPLEX st P[t,ff]
proof let t be Element of NAT;
consider g such that
A3: P[t,g] by A1;
reconsider g as Element of COMPLEX by XCMPLX_0:def 2;
take g;
thus P[t,g] by A3;
end;
consider f being sequence of COMPLEX such that
A4: for t being Element of NAT holds P[t,f.t] from FUNCT_2:sch 3(A2);
reconsider s=f as Complex_Sequence;
take s;
let n;
n in NAT by ORDINAL1:def 12;
hence thesis by A4;
end;
begin
theorem
f is_continuous_in x0 iff x0 in dom f & for s1 st rng s1 c= dom f & s1
is convergent & lim s1=x0 & (for n holds s1.n<>x0) holds f/*s1 is convergent &
f/.x0=lim(f/*s1)
proof
thus f is_continuous_in x0 implies x0 in dom f & for s1 st rng s1 c= dom f &
s1 is convergent & lim s1=x0 & (for n holds s1.n<>x0) holds f/*s1 is convergent
& f/.x0=lim(f/*s1);
assume that
A1: x0 in dom f and
A2: for s1 st rng s1 c=dom f & s1 is convergent & lim s1=x0 & (for n
holds s1.n<>x0) holds f/*s1 is convergent & f/.x0=lim(f/*s1);
thus x0 in dom f by A1;
let s2 such that
A3: rng s2 c=dom f and
A4: s2 is convergent & lim s2=x0;
now
per cases;
suppose
ex n st for m st n<=m holds s2.m=x0;
then consider N be Nat such that
A5: for m st N<=m holds s2.m=x0;
A6: for n holds (s2^\N).n=x0
proof
let n;
s2.(n+N)=x0 by A5,NAT_1:12;
hence thesis by NAT_1:def 3;
end;
A7: f/*(s2^\N)=(f/*s2)^\N by A3,VALUED_0:27;
A8: rng (s2^\N) c= rng s2 by VALUED_0:21;
A9: now
let p such that
A10: p>0;
reconsider n=0 as Nat;
take n;
let m such that
n<=m;
m in NAT by ORDINAL1:def 12;
then |.(f/*(s2^\N)).m-f/.x0.|=|.f/.((s2^\N).m)-f/.x0.|
by A3,A8,FUNCT_2:109
,XBOOLE_1:1
.=|.f/.x0-f/.x0.| by A6
.=0 by COMPLEX1:44;
hence |.(f/*(s2^\N)).m-f/.x0.|<p by A10;
end;
then
A11: f/*(s2^\N) is convergent;
then f/.x0=lim((f/*s2)^\N) by A9,A7,COMSEQ_2:def 6;
hence thesis by A11,A7,Th18,Th22;
end;
suppose
A12: for n ex m st n<=m & s2.m<>x0;
defpred P2[set,set] means for n,m st $1=n & $2=m holds n<m & s2.m<>x0 &
for k st n<k & s2.k<>x0 holds m<=k;
defpred R[set,set,set] means P2[$2,$3];
defpred P[set] means s2.$1<>x0;
ex m1 be Nat st 0<=m1 & s2.m1<>x0 by A12;
then
A13: ex m be Nat st P[m];
consider M be Nat such that
A14: P[M] & for n be Nat st P[n] holds M<=n from NAT_1:sch 5(A13);
reconsider M9 = M as Element of NAT by ORDINAL1:def 12;
A15: now
let n;
consider m such that
A16: n+1<=m & s2.m<>x0 by A12;
take m;
thus n<m & s2.m<>x0 by A16,NAT_1:13;
end;
A17: for n being Nat
for x be Element of NAT ex y be Element of NAT st R[n,x,y]
proof
let n be Nat;
let x be Element of NAT;
defpred P[Nat] means x<$1 & s2.$1<>x0;
ex m st P[m] by A15;
then
A18: ex m be Nat st P[m];
consider l be Nat such that
A19: P[l] & for k be Nat st P[k] holds l<=k from NAT_1:sch 5(A18);
take l;
l in NAT by ORDINAL1:def 12;
hence thesis by A19;
end;
consider F be sequence of NAT such that
A20: F.0=M9 & for n be Nat holds R[n,F.n,F.(n+1)] from
RECDEF_1:sch 2(A17);
A21: for n holds F.n is real;
dom F=NAT by FUNCT_2:def 1;
then reconsider F as Real_Sequence by A21,SEQ_1:2;
for n holds F.n<F.(n+1) by A20;
then reconsider F as increasing sequence of NAT by SEQM_3:def 6;
A22: s2*F is subsequence of s2 by VALUED_0:def 17;
then
A23: s2*F is convergent & lim (s2*F)=x0 by A4,Th17,Th18;
A24: for n st s2.n<>x0 ex m st F.m=n
proof
defpred P[set] means s2.$1<>x0 & for m holds F.m<>$1;
assume ex n st P[n];
then
A25: ex n be Nat st P[n];
consider M1 be Nat such that
A26: P[M1] & for n be Nat st P[n] holds M1<=n from NAT_1:sch 5(A25
);
defpred E[Nat] means $1<M1 & s2.$1<>x0 & ex m st F.m=$1;
A27: ex n being Nat st E[n]
proof
take M;
M<=M1 & M <> M1 by A14,A20,A26;
hence M<M1 by XXREAL_0:1;
thus s2.M<>x0 by A14;
take 0;
thus thesis by A20;
end;
A28: for n being Nat st E[n] holds n <= M1;
consider MX be Nat such that
A29: E[MX] & for n being Nat st E[n] holds n<=MX from NAT_1:sch 6(
A28,A27 );
A30: for k st MX<k & k<M1 holds s2.k=x0
proof
given k such that
A31: MX<k and
A32: k<M1 & s2.k<>x0;
now
per cases;
suppose
ex m st F.m=k;
hence contradiction by A29,A31,A32;
end;
suppose
for m holds F.m<>k;
hence contradiction by A26,A32;
end;
end;
hence contradiction;
end;
consider m such that
A33: F.m=MX by A29;
A34: MX<F.(m+1) & s2.(F.(m+1))<>x0 by A20,A33;
A35: F.(m+1)<=M1 by A20,A26,A29,A33;
now
assume F.(m+1)<>M1;
then F.(m+1)<M1 by A35,XXREAL_0:1;
hence contradiction by A30,A34;
end;
hence contradiction by A26;
end;
defpred P[Nat] means (s2*F).$1<>x0;
A36: for k st P[k] holds P[k+1]
proof
let k such that
(s2*F).k<>x0;
P2[F.k,F.(k+1)] by A20;
then s2.(F.(k+1))<>x0;
hence thesis by FUNCT_2:15;
end;
A37: P[0] by A14,A20,FUNCT_2:15;
A38: for n holds P[n] from NAT_1:sch 2(A37,A36);
A39: rng (s2*F) c= rng s2 by A22,VALUED_0:21;
then rng (s2*F) c= dom f by A3;
then
A40: f/*(s2*F) is convergent & f/.x0=lim(f/*(s2*F)) by A2,A38,A23;
A41: now
let p;
assume
A42: 0<p;
then consider n such that
A43: for m st n<=m holds |.(f/*(s2*F)).m-f/.x0.|<p by A40,COMSEQ_2:def 6;
reconsider k=F.n as Nat;
take k;
let m such that
A44: k<=m;
per cases;
suppose
A45: s2.m=x0;
m in NAT by ORDINAL1:def 12;
then |.(f/*s2).m-f/.x0.|=|.f/.x0-f/.x0.| by A3,FUNCT_2:109,A45
.=0 by COMPLEX1:44;
hence |.(f/*s2).m-f/.x0.|<p by A42;
end;
suppose
s2.m<>x0;
then consider l be Nat such that
A46: m=F.l by A24;
A47: l in NAT by ORDINAL1:def 12;
A48: m in NAT by ORDINAL1:def 12;
n<=l by A44,A46,SEQM_3:1;
then |.(f/*(s2*F)).l-f/.x0.|<p by A43;
then |.f/.((s2*F).l)-f/.x0.|<p
by A3,A39,FUNCT_2:109,XBOOLE_1:1,A47;
then |.f/.(s2.m)-f/.x0.|<p by A46,FUNCT_2:15,A47;
hence |.(f/*s2).m-f/.x0.|<p by A3,FUNCT_2:109,A48;
end;
end;
hence f/*s2 is convergent;
hence f/.x0=lim(f/*s2) by A41,COMSEQ_2:def 6;
end;
end;
hence thesis;
end;
theorem Th32:
f is_continuous_in x0 iff x0 in dom f & for r st 0<r ex s st 0<s
& for x1 st x1 in dom f & |.x1-x0.|<s holds |.f/.x1-f/.x0.|<r
proof
thus f is_continuous_in x0 implies x0 in dom f & for r st 0<r ex s st 0<s &
for x1 st x1 in dom f & |.x1-x0.|<s holds |.f/.x1-f/.x0.|<r
proof
assume
A1: f is_continuous_in x0;
hence x0 in dom f;
given r such that
A2: 0<r and
A3: for s holds not 0<s or ex x1 st x1 in dom f & |.x1-x0.|<s & not |.
f /.x1-f/.x0.|<r;
defpred P[Nat,Complex] means $2 in dom f & |.$2-x0.|
< 1/($1+1) & not |.f/.$2-f/.x0.|<r;
A4: for n ex g st P[n,g]
proof
let n;
0<1/(n+1);
then consider g such that
A5: g in dom f & |.g-x0.| < 1/(n+1) & not |.f/.g-f/.x0.|<r by A3;
take g;
thus thesis by A5;
end;
consider s1 such that
A6: for n holds P[n,s1.n] from CompSeqChoice(A4);
A7: rng s1 c= dom f
proof
let x be object;
assume x in rng s1;
then ex n being Element of NAT st x=s1.n by FUNCT_2:113;
hence thesis by A6;
end;
A8: now
let n;
A9: n in NAT by ORDINAL1:def 12;
not |.f/.(s1.n)-f/.x0.|<r by A6;
hence not |.(f/*s1).n-f/.x0.|<r by A7,FUNCT_2:109,A9;
end;
A10: now
let s;
consider n such that
A11: s"<n by SEQ_4:3;
assume 0<s;
then
A12: 0<s";
s"+0 <n+1 by A11,XREAL_1:8;
then 1/(n+1)<1/s" by A12,XREAL_1:76;
then
A13: 1/(n+1)<s by XCMPLX_1:216;
take k=n;
let m;
assume k<=m;
then k+1<=m+1 by XREAL_1:6;
then 1/(m+1)<=1/(k+1) by XREAL_1:118;
then 1/(m+1)<s by A13,XXREAL_0:2;
hence |.s1.m-x0.|<s by A6,XXREAL_0:2;
end;
then
A14: s1 is convergent;
then lim s1=x0 by A10,COMSEQ_2:def 6;
then f/*s1 is convergent & f/.x0=lim(f/*s1) by A1,A7,A14;
then consider n such that
A15: for m st n<=m holds |.(f/*s1).m-f/.x0.|<r by A2,COMSEQ_2:def 6;
|.(f/*s1).n-f/.x0.|<r by A15;
hence contradiction by A8;
end;
assume that
A16: x0 in dom f and
A17: for r st 0<r ex s st 0<s & for x1 st x1 in dom f & |.x1-x0.|<s
holds |.f/.x1-f/.x0.|<r;
now
let s1 such that
A18: rng s1 c= dom f and
A19: s1 is convergent & lim s1 = x0;
A20: now
let p;
assume 0<p;
then consider s such that
A21: 0<s and
A22: for x1 st x1 in dom f & |.x1-x0.|<s holds |.f/.x1-f/.x0.|<p by A17;
consider n such that
A23: for m st n<=m holds |.s1.m-x0.|<s by A19,A21,COMSEQ_2:def 6;
take k=n;
let m;
A24: m in NAT by ORDINAL1:def 12;
assume k<=m;
then s1.m in rng s1 & |.s1.m-x0.|<s by A23,VALUED_0:28;
then |.f/.(s1.m)-f/.x0.|<p by A18,A22;
hence |.(f/*s1).m - f/.x0.|<p by A18,FUNCT_2:109,A24;
end;
then f/*s1 is convergent;
hence f/*s1 is convergent & f/.x0 = lim (f/*s1) by A20,COMSEQ_2:def 6;
end;
hence thesis by A16;
end;
theorem Th33:
f1 is_continuous_in x0 & f2 is_continuous_in x0 implies f1+f2
is_continuous_in x0 & f1-f2 is_continuous_in x0 & f1(#)f2 is_continuous_in x0
proof
assume that
A1: f1 is_continuous_in x0 and
A2: f2 is_continuous_in x0;
A3: x0 in dom f1 & x0 in dom f2 by A1,A2;
now
x0 in dom f1 /\ dom f2 by A3,XBOOLE_0:def 4;
hence
A4: x0 in dom (f1+f2) by VALUED_1:def 1;
let s1;
assume that
A5: rng s1 c= dom(f1+f2) and
A6: s1 is convergent & lim s1=x0;
A7: rng s1 c= dom f1 /\ dom f2 by A5,VALUED_1:def 1;
dom (f1+f2) = dom f1 /\ dom f2 by VALUED_1:def 1;
then dom (f1+f2) c= dom f2 by XBOOLE_1:17;
then
A8: rng s1 c= dom f2 by A5;
then
A9: f2/*s1 is convergent by A2,A6;
dom (f1+f2) = dom f1 /\ dom f2 by VALUED_1:def 1;
then dom (f1+f2) c= dom f1 by XBOOLE_1:17;
then
A10: rng s1 c= dom f1 by A5;
then
A11: f1/*s1 is convergent by A1,A6;
then ((f1/*s1)+(f2/*s1)) is convergent by A9;
hence (f1+f2)/*s1 is convergent by A7,Th7;
A12: f1/.x0 = lim (f1/*s1) by A1,A6,A10;
A13: f2/.x0 = lim (f2/*s1) by A2,A6,A8;
thus (f1+f2)/.x0 = f1/.x0 + f2/.x0 by A4,CFUNCT_1:1
.= lim ((f1/*s1) + (f2/*s1)) by A11,A12,A9,A13,COMSEQ_2:14
.= lim ((f1+f2)/*s1) by A7,Th7;
end;
hence f1+f2 is_continuous_in x0;
now
x0 in dom f1 /\ dom f2 by A3,XBOOLE_0:def 4;
hence
A14: x0 in dom (f1-f2) by CFUNCT_1:2;
let s1;
assume that
A15: rng s1 c= dom(f1-f2) and
A16: s1 is convergent & lim s1=x0;
A17: rng s1 c= dom f1 /\ dom f2 by A15,CFUNCT_1:2;
dom (f1-f2) = dom f1 /\ dom f2 by CFUNCT_1:2;
then dom (f1-f2) c= dom f2 by XBOOLE_1:17;
then
A18: rng s1 c= dom f2 by A15;
then
A19: f2/*s1 is convergent by A2,A16;
dom (f1-f2) = dom f1 /\ dom f2 by CFUNCT_1:2;
then dom (f1-f2) c= dom f1 by XBOOLE_1:17;
then
A20: rng s1 c= dom f1 by A15;
then
A21: f1/*s1 is convergent by A1,A16;
then f1/*s1-f2/*s1 is convergent by A19;
hence (f1-f2)/*s1 is convergent by A17,Th7;
A22: f1/.x0 = lim (f1/*s1) by A1,A16,A20;
A23: f2/.x0 = lim (f2/*s1) by A2,A16,A18;
thus (f1-f2)/.x0 = f1/.x0 - f2/.x0 by A14,CFUNCT_1:2
.= lim (f1/*s1 - f2/*s1) by A21,A22,A19,A23,COMSEQ_2:26
.= lim ((f1-f2)/*s1) by A17,Th7;
end;
hence f1-f2 is_continuous_in x0;
x0 in dom f1 /\ dom f2 by A3,XBOOLE_0:def 4;
hence
A24: x0 in dom (f1(#)f2) by VALUED_1:def 4;
let s1;
assume that
A25: rng s1 c= dom(f1(#)f2) and
A26: s1 is convergent & lim s1=x0;
dom (f1(#)f2) = dom f1 /\ dom f2 by VALUED_1:def 4;
then dom (f1(#)f2) c= dom f2 by XBOOLE_1:17;
then
A27: rng s1 c= dom f2 by A25;
then
A28: f2/*s1 is convergent by A2,A26;
A29: rng s1 c= dom f1 /\ dom f2 by A25,VALUED_1:def 4;
dom (f1(#)f2) = dom f1 /\ dom f2 by VALUED_1:def 4;
then dom (f1(#)f2) c= dom f1 by XBOOLE_1:17;
then
A30: rng s1 c= dom f1 by A25;
then
A31: f1/*s1 is convergent by A1,A26;
then (f1/*s1)(#)(f2/*s1) is convergent by A28;
hence (f1(#)f2)/*s1 is convergent by A29,Th7;
A32: f1/.x0 = lim (f1/*s1) by A1,A26,A30;
A33: f2/.x0 = lim (f2/*s1) by A2,A26,A27;
thus (f1(#)f2)/.x0 = (f1/.x0) * (f2/.x0) by A24,CFUNCT_1:3
.= lim ((f1/*s1)(#)(f2/*s1)) by A31,A32,A28,A33,COMSEQ_2:30
.= lim ((f1(#)f2)/*s1) by A29,Th7;
end;
theorem Th34:
f is_continuous_in x0 implies g(#)f is_continuous_in x0
proof
assume
A1: f is_continuous_in x0;
then x0 in dom f;
hence
A2: x0 in dom (g(#)f) by VALUED_1:def 5;
let s1;
assume that
A3: rng s1 c= dom(g(#)f) and
A4: s1 is convergent & lim s1=x0;
A5: rng s1 c= dom f by A3,VALUED_1:def 5;
then
A6: f/.x0 = lim (f/*s1) by A1,A4;
A7: f/*s1 is convergent by A1,A4,A5;
then g(#)(f/*s1) is convergent;
hence (g(#)f)/*s1 is convergent by A5,Th8;
thus (g(#)f)/.x0 =g*(f/.x0) by A2,CFUNCT_1:4
.= lim (g(#)(f/*s1)) by A7,A6,COMSEQ_2:18
.= lim ((g(#)f)/*s1) by A5,Th8;
end;
theorem
f is_continuous_in x0 implies -f is_continuous_in x0
by Th34;
theorem Th36:
f is_continuous_in x0 & f/.x0<>0 implies f^ is_continuous_in x0
proof
assume that
A1: f is_continuous_in x0 and
A2: f/.x0<>0;
not f/.x0 in {0c} by A2,TARSKI:def 1;
then
A3: not x0 in f"{0c} by PARTFUN2:26;
x0 in dom f by A1;
then x0 in dom f \ f"{0c} by A3,XBOOLE_0:def 5;
hence
A4: x0 in dom (f^) by CFUNCT_1:def 2;
let s1;
assume that
A5: rng s1 c= dom (f^) and
A6: s1 is convergent & lim s1=x0;
dom f \ f"{0c} c= dom f & rng s1 c= dom f \ f"{0c} by A5,CFUNCT_1:def 2
,XBOOLE_1:36;
then rng s1 c= dom f;
then
A7: f/*s1 is convergent & f/.x0 = lim (f/*s1) by A1,A6;
f/*s1 is non-zero by A5,Th10;
then (f/*s1)" is convergent by A2,A7,COMSEQ_2:34;
hence (f^)/*s1 is convergent by A5,Th11;
thus (f^)/.x0 = (f/.x0)" by A4,CFUNCT_1:def 2
.= lim ((f/*s1)") by A2,A5,A7,Th10,COMSEQ_2:35
.= lim ((f^)/*s1) by A5,Th11;
end;
theorem
f1 is_continuous_in x0 & f1/.x0<>0 & f2 is_continuous_in x0 implies f2
/f1 is_continuous_in x0
proof
assume that
A1: f1 is_continuous_in x0 & f1/.x0<>0 and
A2: f2 is_continuous_in x0;
f1^ is_continuous_in x0 by A1,Th36;
then f2(#)(f1^) is_continuous_in x0 by A2,Th33;
hence thesis by CFUNCT_1:39;
end;
definition
let f,X;
pred f is_continuous_on X means
X c= dom f & for x0 st x0 in X holds f|X is_continuous_in x0;
end;
theorem Th38:
for X,f holds f is_continuous_on X iff X c= dom f & for s1 st
rng s1 c= X & s1 is convergent & lim s1 in X holds f/*s1 is convergent & f/.(
lim s1) = lim (f/*s1)
proof
let X,f;
thus f is_continuous_on X implies X c= dom f & for s1 st rng s1 c= X & s1 is
convergent & lim s1 in X holds f/*s1 is convergent & f/.(lim s1) = lim (f/*s1)
proof
assume
A1: f is_continuous_on X;
then
A2: X c= dom f;
now
let s1 such that
A3: rng s1 c= X and
A4: s1 is convergent and
A5: lim s1 in X;
A6: f|X is_continuous_in (lim s1) by A1,A5;
A7: dom (f|X) = dom f /\ X by RELAT_1:61
.= X by A2,XBOOLE_1:28;
now
let n be Element of NAT;
A8: s1.n in rng s1 by VALUED_0:28;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A3,A7,FUNCT_2:109
.= f/.(s1.n) by A3,A7,A8,PARTFUN2:15
.= (f/*s1).n by A2,A3,FUNCT_2:109,XBOOLE_1:1;
end;
then
A9: (f|X)/*s1 = f/*s1 by FUNCT_2:63;
f/.(lim s1) = (f|X)/.(lim s1) by A5,A7,PARTFUN2:15
.= lim (f/*s1) by A3,A4,A7,A6,A9;
hence
f/*s1 is convergent & f/.(lim s1) = lim (f/*s1) by A3,A4,A7,A6,A9;
end;
hence thesis by A1;
end;
assume that
A10: X c= dom f and
A11: for s1 st rng s1 c= X & s1 is convergent & lim s1 in X holds f/*s1
is convergent & f/.(lim s1) = lim (f/*s1);
now
A12: dom (f|X) = dom f /\ X by RELAT_1:61
.= X by A10,XBOOLE_1:28;
let x1 such that
A13: x1 in X;
now
let s1 such that
A14: rng s1 c= dom (f|X) and
A15: s1 is convergent and
A16: lim s1 = x1;
now
let n be Element of NAT;
A17: s1.n in rng s1 by VALUED_0:28;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A14,FUNCT_2:109
.= f/.(s1.n) by A14,A17,PARTFUN2:15
.= (f/*s1).n by A10,A12,A14,FUNCT_2:109,XBOOLE_1:1;
end;
then
A18: (f|X)/*s1 = f/*s1 by FUNCT_2:63;
(f|X)/.(lim s1) = f/.(lim s1) by A13,A12,A16,PARTFUN2:15
.= lim ((f|X)/*s1) by A11,A13,A12,A14,A15,A16,A18;
hence (f|X)/*s1 is convergent & (f|X)/.x1 = lim ((f|X)/*s1) by A11,A13
,A12,A14,A15,A16,A18;
end;
hence f|X is_continuous_in x1 by A13,A12;
end;
hence thesis by A10;
end;
theorem Th39:
f is_continuous_on X iff X c= dom f & for x0,r st x0 in X & 0<r
ex s st 0<s & for x1 st x1 in X & |.x1-x0.| < s holds |.f/.x1 - f/.x0.| < r
proof
thus f is_continuous_on X implies X c= dom f & for x0,r st x0 in X & 0<r ex
s st 0<s & for x1 st x1 in X & |.x1-x0.| < s holds |.f/.x1 - f/.x0.| < r
proof
assume
A1: f is_continuous_on X;
hence X c= dom f;
A2: X c= dom f by A1;
let x0,r;
assume that
A3: x0 in X and
A4: 0<r;
f|X is_continuous_in x0 by A1,A3;
then consider s such that
A5: 0<s and
A6: for x1 st x1 in dom(f|X) & |.x1-x0.|<s holds |.(f|X)/.x1-(f|X)/.x0
.| <r by A4,Th32;
take s;
thus 0<s by A5;
let x1;
assume that
A7: x1 in X and
A8: |.x1-x0.|<s;
A9: dom (f|X) = dom f /\ X by RELAT_1:61
.= X by A2,XBOOLE_1:28;
then |.f/.x1 - f/.x0.| = |.(f|X)/.x1 - f/.x0.| by A7,PARTFUN2:15
.= |.(f|X)/.x1 - (f|X)/.x0.| by A3,A9,PARTFUN2:15;
hence thesis by A6,A9,A7,A8;
end;
assume that
A10: X c= dom f and
A11: for x0,r st x0 in X & 0<r ex s st 0<s & for x1 st x1 in X & |.x1-x0
.| < s holds |.f/.x1 - f/.x0.| < r;
A12: dom (f|X) = dom f /\ X by RELAT_1:61
.= X by A10,XBOOLE_1:28;
now
let x0 such that
A13: x0 in X;
for r st 0<r ex s st 0<s & for x1 st x1 in dom(f|X) & |.x1-x0.|<s
holds |.(f|X)/.x1-(f|X)/.x0.|<r
proof
let r;
assume 0<r;
then consider s such that
A14: 0<s and
A15: for x1 st x1 in X & |.x1-x0.| < s holds |.f/.x1 - f/.x0.| < r by A11,A13;
take s;
thus 0<s by A14;
let x1 such that
A16: x1 in dom(f|X) and
A17: |.x1-x0.|<s;
|.(f|X)/.x1-(f|X)/.x0.| = |.(f|X)/.x1 - f/.x0.| by A12,A13,PARTFUN2:15
.= |.f/.x1 - f/.x0.| by A16,PARTFUN2:15;
hence thesis by A12,A15,A16,A17;
end;
hence f|X is_continuous_in x0 by A12,A13,Th32;
end;
hence thesis by A10;
end;
theorem Th40:
f is_continuous_on X iff f|X is_continuous_on X
proof
thus f is_continuous_on X implies f|X is_continuous_on X
proof
assume
A1: f is_continuous_on X;
then X c= dom f;
then X c= dom f /\ X by XBOOLE_1:28;
hence X c= dom (f|X) by RELAT_1:61;
let g;
assume g in X;
then f|X is_continuous_in g by A1;
hence thesis by RELAT_1:72;
end;
assume
A2: f|X is_continuous_on X;
then X c= dom(f|X);
then dom f /\ X c= dom f & X c= dom f /\ X by RELAT_1:61,XBOOLE_1:17;
hence X c= dom f;
let g;
assume g in X;
then (f|X)|X is_continuous_in g by A2;
hence thesis by RELAT_1:72;
end;
theorem Th41:
f is_continuous_on X & X1 c= X implies f is_continuous_on X1
proof
assume that
A1: f is_continuous_on X and
A2: X1 c= X;
X c= dom f by A1;
hence
A3: X1 c= dom f by A2;
let g;
assume
A4: g in X1;
then
A5: f|X is_continuous_in g by A1,A2;
thus f|X1 is_continuous_in g
proof
dom f /\ X1 c= dom f /\ X by A2,XBOOLE_1:26;
then dom (f|X1) c= dom f /\ X by RELAT_1:61;
then
A6: dom (f|X1) c= dom (f|X) by RELAT_1:61;
g in dom f /\ X1 by A3,A4,XBOOLE_0:def 4;
hence
A7: g in dom (f|X1) by RELAT_1:61;
then
A8: (f|X)/.g = f/.g by A6,PARTFUN2:15
.= (f|X1)/.g by A7,PARTFUN2:15;
let s1 such that
A9: rng s1 c= dom (f|X1) and
A10: s1 is convergent & lim s1 = g;
A11: rng s1 c= dom (f|X) by A9,A6;
A12: now
let n be Element of NAT;
A13: s1.n in rng s1 by VALUED_0:28;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A9,A6,FUNCT_2:109,XBOOLE_1:1
.= f/.(s1.n) by A11,A13,PARTFUN2:15
.= (f|X1)/.(s1.n) by A9,A13,PARTFUN2:15
.= ((f|X1)/*s1).n by A9,FUNCT_2:109;
end;
(f|X)/*s1 is convergent & (f|X)/.g = lim ((f|X)/*s1) by A5,A10,A11;
hence thesis by A8,A12,FUNCT_2:63;
end;
end;
theorem
x0 in dom f implies f is_continuous_on {x0}
proof
assume
A1: x0 in dom f;
thus {x0} c= dom f
by A1,TARSKI:def 1;
let t such that
A2: t in {x0};
thus f|{x0} is_continuous_in t
proof
t in dom f by A1,A2,TARSKI:def 1;
then t in dom f /\ {x0} by A2,XBOOLE_0:def 4;
hence t in dom (f|{x0}) by RELAT_1:61;
let s1;
assume that
A3: rng s1 c= dom(f|{x0}) and
s1 is convergent and
lim s1=t;
A4: dom f /\ {x0} c= {x0} by XBOOLE_1:17;
rng s1 c= dom f /\ {x0} by A3,RELAT_1:61;
then
A5: rng s1 c= {x0} by A4;
A6: now
let n;
s1.n in rng s1 by VALUED_0:28;
hence s1.n = x0 by A5,TARSKI:def 1;
end;
A7: t=x0 by A2,TARSKI:def 1;
A8: now
let r such that
A9: 0<r;
reconsider n=0 as Nat;
take n;
let m such that
n<=m;
A10: m in NAT by ORDINAL1:def 12;
|.((f|{x0})/*s1).m - (f|{x0})/.t.| = |.(f|{x0})/.(s1.m) - (f|{x0})
/.x0.| by A7,A3,FUNCT_2:109,A10
.= |.(f|{x0})/.x0 - (f|{x0})/.x0.| by A6
.= 0 by COMPLEX1:44;
hence |.((f|{x0})/*s1).m - (f|{x0})/.t.| < r by A9;
end;
hence (f|{x0})/*s1 is convergent;
hence thesis by A8,COMSEQ_2:def 6;
end;
end;
theorem Th43:
for X,f1,f2 st f1 is_continuous_on X & f2 is_continuous_on X
holds f1+f2 is_continuous_on X & f1-f2 is_continuous_on X & f1(#) f2
is_continuous_on X
proof
let X,f1,f2;
assume
A1: f1 is_continuous_on X & f2 is_continuous_on X;
then X c= dom f1 & X c= dom f2;
then
A2: X c= dom f1 /\ dom f2 by XBOOLE_1:19;
then
A3: X c= dom (f1+f2) by CFUNCT_1:1;
now
let s1;
assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X;
A7: f1/*s1 is convergent & f2/*s1 is convergent by A1,A4,A5,A6,Th38;
then
A8: (f1/*s1)+(f2/*s1) is convergent;
A9: rng s1 c= dom f1 /\ dom f2 by A2,A4;
A10: lim s1 in dom (f1+f2) by A3,A6;
f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1) by A1,A4,A5,A6
,Th38;
then (f1+f2)/.(lim s1) = lim (f1/*s1) + lim (f2/*s1) by A10,CFUNCT_1:1
.= lim (f1/*s1 + f2/*s1) by A7,COMSEQ_2:14
.= lim ((f1+f2)/*s1) by A9,Th7;
hence
(f1+f2)/*s1 is convergent & (f1+f2)/.(lim s1)=lim((f1+f2)/*s1) by A9,A8,Th7
;
end;
hence f1+f2 is_continuous_on X by A3,Th38;
A11: X c= dom (f1-f2) by A2,CFUNCT_1:2;
now
let s1;
assume that
A12: rng s1 c= X and
A13: s1 is convergent and
A14: lim s1 in X;
A15: f1/*s1 is convergent & f2/*s1 is convergent by A1,A12,A13,A14,Th38;
then
A16: (f1/*s1)-(f2/*s1) is convergent;
A17: rng s1 c= dom f1 /\ dom f2 by A2,A12;
A18: lim s1 in dom (f1-f2) by A11,A14;
f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1) by A1,A12,A13,A14
,Th38;
then (f1-f2)/.(lim s1) = lim (f1/*s1) - lim (f2/*s1) by A18,CFUNCT_1:2
.= lim (f1/*s1 - f2/*s1) by A15,COMSEQ_2:26
.= lim ((f1-f2)/*s1) by A17,Th7;
hence
(f1-f2)/*s1 is convergent & (f1-f2)/.(lim s1)=lim((f1-f2)/*s1) by A17,A16
,Th7;
end;
hence f1-f2 is_continuous_on X by A11,Th38;
A19: X c= dom (f1(#)f2) by A2,CFUNCT_1:3;
now
let s1;
assume that
A20: rng s1 c= X and
A21: s1 is convergent and
A22: lim s1 in X;
A23: f1/*s1 is convergent & f2/*s1 is convergent by A1,A20,A21,A22,Th38;
then
A24: (f1/*s1)(#)(f2/*s1) is convergent;
A25: rng s1 c= dom f1 /\ dom f2 by A2,A20;
A26: lim s1 in dom (f1(#)f2) by A19,A22;
f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1) by A1,A20,A21,A22
,Th38;
then (f1(#)f2)/.(lim s1) = lim (f1/*s1) * lim (f2/*s1) by A26,
CFUNCT_1:3
.= lim ((f1/*s1) (#) (f2/*s1)) by A23,COMSEQ_2:30
.= lim ((f1(#)f2)/*s1) by A25,Th7;
hence (f1(#)f2)/*s1 is convergent & (f1(#)f2)/.(lim s1)=lim((f1(#)f2)/*s1)
by A25,A24,Th7;
end;
hence thesis by A19,Th38;
end;
theorem
for X,X1,f1,f2 st f1 is_continuous_on X & f2 is_continuous_on X1 holds
f1+f2 is_continuous_on X /\ X1 & f1-f2 is_continuous_on X /\ X1 & f1(#)f2
is_continuous_on X /\ X1
proof
let X,X1,f1,f2;
assume f1 is_continuous_on X & f2 is_continuous_on X1;
then f1 is_continuous_on X /\ X1 & f2 is_continuous_on X /\ X1 by Th41,
XBOOLE_1:17;
hence thesis by Th43;
end;
theorem Th45:
for g,X,f st f is_continuous_on X holds g(#)f is_continuous_on X
proof
let g,X,f;
assume
A1: f is_continuous_on X;
then
A2: X c= dom f;
then
A3: X c= dom(g(#)f) by CFUNCT_1:4;
now
let s1;
assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X;
A7: f/*s1 is convergent by A1,A4,A5,A6,Th38;
then
A8: g(#)(f/*s1) is convergent;
A9: lim s1 in dom(g(#)f) by A3,A6;
f/.(lim s1) = lim (f/*s1) by A1,A4,A5,A6,Th38;
then (g(#)f)/.(lim s1) = g * lim (f/*s1) by CFUNCT_1:4,A9
.= lim (g(#)(f/*s1)) by A7,COMSEQ_2:18
.= lim ((g(#)f)/*s1) by A2,A4,Th8,XBOOLE_1:1;
hence
(g(#)f)/*s1 is convergent & (g(#)f)/.(lim s1)=lim((g(#)f)/*s1) by A2,A4,A8
,Th8,XBOOLE_1:1;
end;
hence thesis by A3,Th38;
end;
theorem
f is_continuous_on X implies -f is_continuous_on X
by Th45;
theorem Th47:
f is_continuous_on X & f"{0} = {} implies f^ is_continuous_on X
proof
assume that
A1: f is_continuous_on X and
A2: f"{0} = {};
A3: dom(f^) = dom f \ {} by A2,CFUNCT_1:def 2
.= dom f;
hence
A4: X c= dom (f^) by A1;
let g;
assume
A5: g in X;
then
A6: f|X is_continuous_in g by A1;
g in dom(f^) /\ X by A4,A5,XBOOLE_0:def 4;
then
A7: g in dom((f^)|X) by RELAT_1:61;
now
let s1;
assume that
A8: rng s1 c= dom((f^)|X) and
A9: s1 is convergent & lim s1= g;
rng s1 c= dom(f^) /\ X by A8,RELAT_1:61;
then
A10: rng s1 c= dom(f|X) by A3,RELAT_1:61;
then
A11: (f|X)/*s1 is convergent by A6,A9;
now
let n be Element of NAT;
A12: s1.n in rng s1 by VALUED_0:28;
rng s1 c= dom f /\ X & dom f /\ X c= dom f by A3,A8,RELAT_1:61
,XBOOLE_1:17;
then
A13: rng s1 c= dom f;
A14: now
assume f/.(s1.n)=0c;
then f/.(s1.n) in {0c} by TARSKI:def 1;
hence contradiction by A2,A13,A12,PARTFUN2:26;
end;
((f|X)/*s1).n = (f|X)/.(s1.n) by A10,FUNCT_2:109
.= f/.(s1.n) by A10,A12,PARTFUN2:15;
hence ((f|X)/*s1).n <>0c by A14;
end;
then
A15: (f|X)/*s1 is non-zero by COMSEQ_1:4;
g in dom f /\ X by A3,A4,A5,XBOOLE_0:def 4;
then
A16: g in dom(f|X) by RELAT_1:61;
then
A17: (f|X)/.g = f/.g by PARTFUN2:15;
now
let n be Element of NAT;
A18: s1.n in rng s1 by VALUED_0:28;
then s1.n in dom((f^)|X) by A8;
then s1.n in dom (f^) /\ X by RELAT_1:61;
then
A19: s1.n in dom (f^) by XBOOLE_0:def 4;
thus (((f^)|X)/*s1).n = ((f^)|X)/.(s1.n) by A8,FUNCT_2:109
.= (f^)/.(s1.n) by A8,A18,PARTFUN2:15
.= (f/.(s1.n))" by A19,CFUNCT_1:def 2
.= ((f|X)/.(s1.n))" by A10,A18,PARTFUN2:15
.= (((f|X)/*s1).n)" by A10,FUNCT_2:109
.= (((f|X)/*s1)").n by VALUED_1:10;
end;
then
A20: ((f^)|X)/*s1 = ((f|X)/*s1)" by FUNCT_2:63;
reconsider gg = g as Element of COMPLEX by XCMPLX_0:def 2;
A21: now
assume f/.g = 0c;
then f/.gg in {0c} by TARSKI:def 1;
hence contradiction by A2,A3,A4,A5,PARTFUN2:26;
end;
then lim ((f|X)/*s1) <> 0c by A6,A9,A10,A17;
hence ((f^)|X)/*s1 is convergent by A11,A15,A20,COMSEQ_2:34;
(f|X)/.g = lim ((f|X)/*s1) by A6,A9,A10;
hence lim (((f^)|X)/*s1) = ((f|X)/.g)" by A11,A17,A21,A15,A20,COMSEQ_2:35
.= (f/.g)" by A16,PARTFUN2:15
.= (f^)/.gg by A4,A5,CFUNCT_1:def 2
.= ((f^)|X)/.g by A7,PARTFUN2:15;
end;
hence thesis by A7;
end;
theorem
f is_continuous_on X & (f|X)"{0} = {} implies f^ is_continuous_on X
proof
assume that
A1: f is_continuous_on X and
A2: (f|X)"{0} = {};
f|X is_continuous_on X by A1,Th40;
then (f|X)^ is_continuous_on X by A2,Th47;
then (f^)|X is_continuous_on X by CFUNCT_1:54;
hence thesis by Th40;
end;
theorem
f1 is_continuous_on X & f1"{0} = {} & f2 is_continuous_on X implies f2
/f1 is_continuous_on X
proof
assume that
A1: f1 is_continuous_on X & f1"{0} = {} and
A2: f2 is_continuous_on X;
f1^ is_continuous_on X by A1,Th47;
then f2(#)(f1^) is_continuous_on X by A2,Th43;
hence thesis by CFUNCT_1:39;
end;
theorem
f is total & (for x1,x2 holds f/.(x1+x2) = f/.x1 + f/.x2) & (ex x0 st
f is_continuous_in x0) implies f is_continuous_on COMPLEX
proof
assume that
A1: f is total and
A2: for x1,x2 holds f/.(x1+x2) = f/.x1 + f/.x2 and
A3: ex x0 st f is_continuous_in x0;
A4: dom f = COMPLEX by A1,PARTFUN1:def 2;
consider x0 such that
A5: f is_continuous_in x0 by A3;
A6: f/.x0 + 0c = f/.(x0+0c) .= f/.x0+f/.0c by A2;
A7: now
let x1;
0c = f/.(x1+-x1) by A6
.= f/.x1+f/.(-x1) by A2;
hence -(f/.x1)=f/.(-x1);
end;
A8: now
let x1,x2;
thus f/.(x1-x2)=f/.(x1+-x2) .= f/.x1 + f/.(-x2) by A2
.= f/.x1 +- f/.x2 by A7
.= f/.x1 - f/.x2;
end;
now
let x1,r;
assume that
x1 in COMPLEX and
A9: r>0;
set y=x1-x0;
consider s such that
A10: 0<s and
A11: for x1 st x1 in dom f & |.x1-x0.|<s holds |.f/.x1-f/.x0.|<r by A5,A9,Th32;
take s;
thus s>0 by A10;
let x2 such that
x2 in COMPLEX and
A12: |.x2-x1.|<s;
A13: |.x2-y-x0.|=|.x2-x1.|;
A14: x2 - y in dom f by A4,XCMPLX_0:def 2;
x1-x0+x0=x1;
then |.f/.x2-f/.x1.| = |.f/.x2-(f/.y+f/.x0).| by A2
.= |.f/.x2-f/.y-f/.x0.|
.= |.f/.(x2-y)-f/.x0.| by A8;
hence |.f/.x2-f/.x1.|<r by A11,A12,A13,A14;
end;
hence thesis by A4,Th39;
end;
definition
let X;
attr X is compact means
for s1 st (rng s1) c= X ex s2 st s2 is
subsequence of s1 & s2 is convergent & (lim s2) in X;
end;
theorem Th51:
for f st dom f is compact & f is_continuous_on (dom f) holds (
rng f) is compact
proof
let f;
assume that
A1: dom f is compact and
A2: f is_continuous_on (dom f);
now
let s1 such that
A3: rng s1 c= rng f;
defpred P[object,object] means $2 in dom f & f/.$2=s1.$1;
A4: for n ex g st P[n,g]
proof
let n;
s1.n in rng s1 by VALUED_0:28;
then consider g being Element of COMPLEX such that
A5: g in dom f & s1.n=f.g by A3,PARTFUN1:3;
take g;
thus thesis by A5,PARTFUN1:def 6;
end;
consider q1 such that
A6: for n holds P[n,q1.n] from CompSeqChoice(A4);
now
let x be object;
assume x in rng q1;
then ex n being Element of NAT st x = q1.n by FUNCT_2:113;
hence x in dom f by A6;
end;
then
A7: rng q1 c= dom f;
then consider s2 such that
A8: s2 is subsequence of q1 and
A9: s2 is convergent and
A10: (lim s2) in dom f by A1;
take q2 = f/*s2;
rng s2 c= rng q1 by A8,VALUED_0:21;
then
A11: rng s2 c= dom f by A7;
now
let n be Element of NAT;
f/.(q1.n)=s1.n by A6;
hence (f/*q1).n= s1.n by A7,FUNCT_2:109;
end;
then
A12: f/*q1=s1 by FUNCT_2:63;
f|(dom f) is_continuous_in (lim s2) by A2,A10;
then
A13: f is_continuous_in (lim s2) by RELAT_1:68;
then f/.(lim s2) = lim (f/*s2) by A9,A11;
then f.(lim s2) = lim (f/*s2) by A10,PARTFUN1:def 6;
hence
q2 is subsequence of s1 & q2 is convergent & (lim q2) in rng f by A7,A12,A8
,A9,A13,A11,FUNCT_1:def 3,VALUED_0:22;
end;
hence thesis;
end;
theorem
Y c= dom f & Y is compact & f is_continuous_on Y implies (f.:Y) is compact
proof
assume that
A1: Y c= dom f and
A2: Y is compact and
A3: f is_continuous_on Y;
A4: dom (f|Y) = dom f /\ Y by RELAT_1:61
.= Y by A1,XBOOLE_1:28;
f|Y is_continuous_on Y
proof
thus Y c= dom (f|Y) by A4;
let g;
assume g in Y;
then f|Y is_continuous_in g by A3;
hence thesis by RELAT_1:72;
end;
then rng (f|Y) is compact by A2,A4,Th51;
hence thesis by RELAT_1:115;
end;