The Mizar abstract of CFCONT

Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users
The abstract of the Mizar article:: Property of Complex Sequence and Continuity of Complex Function
by
Takashi Mitsuishi,
Katsumi Wasaki, and
Yasunari Shidama
Received December 7, 1999
MML identifier: CFCONT_1
[ Mizar article, MML identifier index ]
environ

 vocabulary COMPLEX1, COMSEQ_1, PARTFUN1, ORDINAL2, SEQM_3, SEQ_1, RELAT_1,
      FUNCT_1, CFUNCT_1, FCONT_1, SEQ_2, FINSEQ_4, ARYTM_1, ANPROJ_1, BOOLE,
      FINSEQ_1, ARYTM_3, COMPTS_1, ARYTM;
 notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, NUMBERS, XREAL_0,
      REAL_1, NAT_1, PARTFUN1, FUNCT_2, SEQ_1, RELSET_1, SEQM_3, COMPLEX1,
      FINSEQ_4, CFUNCT_1, COMSEQ_1, COMSEQ_2, COMSEQ_3;
 constructors REAL_1, NAT_1, FINSEQ_4, SEQ_1, COMSEQ_1, COMSEQ_2, COMSEQ_3,
      PARTFUN1, CFUNCT_1, COMPLEX1, MEMBERED;
 clusters FUNCT_1, RELSET_1, SEQM_3, COMSEQ_1, NAT_1, COMPLEX1, MEMBERED,
      NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

 reserve n,n1,m,m1,l,k for Nat;
 reserve x,y,X,X1 for set;
 reserve g,g1,g2,t,x0,x1,x2 for Element of 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 Seq_of_Nat;
 reserve Rseq1 for Real_Sequence;

::
:: COMPLEX SEQUENCE
::

definition let h,seq;
assume  rng seq c= dom h;
func h*seq -> Complex_Sequence equals
:: CFCONT_1:def 1
(h qua Function)*seq;
end;

definition let f,x0;
 pred f is_continuous_in x0 means
:: CFCONT_1:def 2
 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;

canceled;

theorem :: CFCONT_1:2
seq1=seq2-seq3 iff for n holds seq1.n=seq2.n-seq3.n;

theorem :: CFCONT_1:3
rng (seq^\n) c= rng seq;

theorem :: CFCONT_1:4
rng seq c= dom f implies seq.n in dom f;

theorem :: CFCONT_1:5
x in rng seq iff ex n st x = seq.n;

theorem :: CFCONT_1:6
  seq.n in rng seq;

theorem :: CFCONT_1:7
seq1 is_subsequence_of seq implies rng seq1 c= rng seq;

theorem :: CFCONT_1:8
  seq1 is_subsequence_of seq & seq is non-zero implies seq1 is non-zero;

theorem :: CFCONT_1:9
(seq1 + seq2)(#)Ns = (seq1(#)Ns) + (seq2(#)Ns) &
(seq1 - seq2)(#)Ns = (seq1(#)Ns) - (seq2(#)Ns) &
(seq1 (#) seq2)(#)Ns = (seq1(#)Ns) (#) (seq2(#)Ns);

theorem :: CFCONT_1:10
(g(#)seq)(#)Ns = g(#)(seq(#)Ns);

theorem :: CFCONT_1:11
  (-seq)(#)Ns = -(seq(#)Ns) & (|.seq.|)*Ns = |.(seq(#)Ns).|;

theorem :: CFCONT_1:12
  (seq(#)Ns)" = (seq")(#)Ns;

theorem :: CFCONT_1:13
  (seq1/"seq)(#)Ns = (seq1(#)Ns)/"(seq(#)Ns);

theorem :: CFCONT_1:14
  (for n holds seq.n in Y) implies rng seq c= Y;

canceled;

theorem :: CFCONT_1:16
rng seq c= dom f implies (f*seq).n = f/.(seq.n);

theorem :: CFCONT_1:17
rng seq c= dom f implies (f*seq)^\n=f*(seq^\n);

theorem :: CFCONT_1:18
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);

theorem :: CFCONT_1:19
rng seq c= dom h implies (g(#)h)*seq = g(#)(h*seq);

theorem :: CFCONT_1:20
  rng seq c= dom h implies -(h*seq) = (-h)*seq;

theorem :: CFCONT_1:21
rng seq c= dom (h^) implies h*seq is non-zero;

theorem :: CFCONT_1:22
rng seq c= dom (h^) implies (h^)*seq =(h*seq)";

theorem :: CFCONT_1:23
rng seq c= dom h implies Re ( (h*seq)(#)Ns ) = Re (h*(seq(#)Ns));

theorem :: CFCONT_1:24
rng seq c= dom h implies Im ( (h*seq)(#)Ns ) = Im (h*(seq(#)Ns));

theorem :: CFCONT_1:25
rng seq c= dom h implies (h*seq)(#)Ns = h * (seq(#)Ns);

theorem :: CFCONT_1:26
rng seq1 c= dom h & seq2 is_subsequence_of seq1 implies
  h*seq2 is_subsequence_of h*seq1;

theorem :: CFCONT_1:27
  h is total implies (h*seq).n = h/.(seq.n);

theorem :: CFCONT_1:28
  h is total implies h*(seq^\n) = (h*seq)^\n;

theorem :: CFCONT_1:29
  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);

theorem :: CFCONT_1:30
  h is total implies (g(#)h)*seq = g(#)(h*seq);

theorem :: CFCONT_1:31
  rng seq c= dom (h|X) implies (h|X)*seq = h*seq;

theorem :: CFCONT_1:32
  rng seq c= dom (h|X) & (rng seq c= dom (h|Y) or X c= Y) implies
 (h|X)*seq = (h|Y)*seq;

theorem :: CFCONT_1:33
  rng seq c= dom (h|X) & h"{0c}={} implies ((h^)|X)*seq = ((h|X)*seq)";

definition let seq;
 redefine canceled;

attr seq is constant means
:: CFCONT_1:def 4
ex g st for n holds seq.n=g;
end;

theorem :: CFCONT_1:34
seq is constant iff ex g st rng seq={g};

theorem :: CFCONT_1:35
seq is constant iff for n holds seq.n=seq.(n+1);

theorem :: CFCONT_1:36
seq is constant iff for n,k holds seq.n=seq.(n+k);

theorem :: CFCONT_1:37
  seq is constant iff for n,m holds seq.n=seq.m;

theorem :: CFCONT_1:38
 seq ^\k is_subsequence_of seq;

theorem :: CFCONT_1:39
seq1 is_subsequence_of seq & seq is convergent implies
seq1 is convergent;

theorem :: CFCONT_1:40
seq1 is_subsequence_of seq & seq is convergent implies
lim seq1=lim seq;

theorem :: CFCONT_1:41
 seq is convergent & (ex k st for n st k<=n holds seq1.n=seq.n)
      implies seq1 is convergent;

theorem :: CFCONT_1:42
   seq is convergent & (ex k st for n st k<=n holds seq1.n=seq.n)
      implies lim seq=lim seq1;

theorem :: CFCONT_1:43
 seq is convergent implies ((seq ^\k) is convergent &
            lim (seq ^\k)=lim seq);

theorem :: CFCONT_1:44
 seq is convergent & (ex k st seq=seq1 ^\k)
       implies seq1 is convergent;

theorem :: CFCONT_1:45
   seq is convergent & (ex k st seq=seq1 ^\k)
       implies lim seq1 =lim seq;

theorem :: CFCONT_1:46
seq is convergent & lim seq<>0c implies ex k st (seq ^\k) is non-zero;

theorem :: CFCONT_1:47
   seq is convergent & lim seq<>0c implies
       ex seq1 st seq1 is_subsequence_of seq & seq1 is non-zero;

theorem :: CFCONT_1:48
seq is constant implies seq is convergent;

theorem :: CFCONT_1:49
(seq is constant & g in rng seq or
      seq is constant & (ex n st seq.n=g)) implies lim seq=g;

theorem :: CFCONT_1:50
  seq is constant implies for n holds lim seq=seq.n;

theorem :: CFCONT_1:51
   seq is convergent & lim seq<>0c implies
       for seq1 st seq1 is_subsequence_of seq & seq1 is non-zero holds
        lim (seq1")=(lim seq)";

theorem :: CFCONT_1:52
   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);

scheme CompSeqChoice { P[set,set] }:
  ex s1 st for n holds P[n,s1.n]
provided
 for n ex g st P[n,g];

begin
::
:: CONTINUITY OF COMPLEX FUNCTIONS
::

theorem :: CFCONT_1:53
  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);

theorem :: CFCONT_1:54
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;

theorem :: CFCONT_1:55
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;


theorem :: CFCONT_1:56
f is_continuous_in x0 implies g(#)f is_continuous_in x0;

theorem :: CFCONT_1:57
  f is_continuous_in x0 implies -f is_continuous_in x0;


theorem :: CFCONT_1:58
f is_continuous_in x0 & f/.x0<>0c implies f^ is_continuous_in x0;

theorem :: CFCONT_1:59
  f1 is_continuous_in x0 & f1/.x0<>0c & f2 is_continuous_in x0 implies
f2/f1 is_continuous_in x0;

definition let f,X;
 pred f is_continuous_on X means
:: CFCONT_1:def 5
 X c= dom f & for x0 st x0 in X holds f|X is_continuous_in x0;
end;

theorem :: CFCONT_1:60
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);

theorem :: CFCONT_1:61
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;

theorem :: CFCONT_1:62
f is_continuous_on X iff f|X is_continuous_on X;

theorem :: CFCONT_1:63
f is_continuous_on X & X1 c= X implies f is_continuous_on X1;

theorem :: CFCONT_1:64
  x0 in dom f implies f is_continuous_on {x0};

theorem :: CFCONT_1:65
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;

theorem :: CFCONT_1:66
  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;

theorem :: CFCONT_1:67
for g,X,f st f is_continuous_on X holds g(#)f is_continuous_on X;

theorem :: CFCONT_1:68
  f is_continuous_on X implies -f is_continuous_on X;

theorem :: CFCONT_1:69
f is_continuous_on X & f"{0c} = {} implies f^ is_continuous_on X;

theorem :: CFCONT_1:70
  f is_continuous_on X & (f|X)"{0c} = {} implies f^ is_continuous_on X;

theorem :: CFCONT_1:71
  f1 is_continuous_on X & f1"{0c} = {} & f2 is_continuous_on X implies
f2/f1 is_continuous_on X;

theorem :: CFCONT_1:72
  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;

definition let X;
attr X is compact means
:: CFCONT_1:def 6
 for s1 st (rng s1) c= X ex s2 st s2 is_subsequence_of s1 &
 s2 is convergent & (lim s2) in X;
end;

theorem :: CFCONT_1:73
for f st dom f is compact & f is_continuous_on (dom f) holds (rng f) is compact
;

theorem :: CFCONT_1:74
  Y c= dom f & Y is compact & f is_continuous_on Y implies
(f.:Y) is compact;
The abstract of the Mizar article:

Property of Complex Sequence and Continuity of Complex Function
