:: Property of Complex Sequence and Continuity of Complex Function
:: by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama
::
:: Copyright (c) 1999-2018 Association of Mizar Users

::
:: COMPLEX SEQUENCE
::
definition
let f be PartFunc of COMPLEX,COMPLEX;
let x0 be Complex;
pred f is_continuous_in x0 means :: CFCONT_1:def 1
( x0 in dom f & ( for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) );
end;

:: deftheorem defines is_continuous_in CFCONT_1:def 1 :
for f being PartFunc of COMPLEX,COMPLEX
for x0 being Complex holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) );

theorem Th1: :: CFCONT_1:1
for seq1, seq2, seq3 being Complex_Sequence holds
( seq1 = seq2 - seq3 iff for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) )
proof end;

theorem Th2: :: CFCONT_1:2
for seq1, seq2 being Complex_Sequence
for Ns being V42() sequence of NAT holds
( (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) & (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) )
proof end;

theorem Th3: :: CFCONT_1:3
for g being Complex
for seq being Complex_Sequence
for Ns being V42() sequence of NAT holds (g (#) seq) * Ns = g (#) (seq * Ns)
proof end;

theorem :: CFCONT_1:4
for seq being Complex_Sequence
for Ns being V42() sequence of NAT holds
( (- seq) * Ns = - (seq * Ns) & |.seq.| * Ns = |.(seq * Ns).| )
proof end;

theorem Th5: :: CFCONT_1:5
for seq being Complex_Sequence
for Ns being V42() sequence of NAT holds (seq * Ns) " = (seq ") * Ns
proof end;

theorem :: CFCONT_1:6
for seq, seq1 being Complex_Sequence
for Ns being V42() sequence of NAT holds (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns)
proof end;

theorem Th7: :: CFCONT_1:7
for seq being Complex_Sequence
for h1, h2 being PartFunc of COMPLEX,COMPLEX st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
proof end;

theorem Th8: :: CFCONT_1:8
for g being Complex
for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom h holds
(g (#) h) /* seq = g (#) (h /* seq)
proof end;

theorem :: CFCONT_1:9
for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom h holds
- (h /* seq) = (- h) /* seq by Th8;

theorem Th10: :: CFCONT_1:10
for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h ^) holds
h /* seq is non-zero
proof end;

theorem Th11: :: CFCONT_1:11
for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h ^) holds
(h ^) /* seq = (h /* seq) "
proof end;

theorem :: CFCONT_1:12
for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX
for Ns being V42() sequence of NAT st rng seq c= dom h holds
Re ((h /* seq) * Ns) = Re (h /* (seq * Ns))
proof end;

theorem :: CFCONT_1:13
for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX
for Ns being V42() sequence of NAT st rng seq c= dom h holds
Im ((h /* seq) * Ns) = Im (h /* (seq * Ns))
proof end;

theorem :: CFCONT_1:14
for seq being Complex_Sequence
for h1, h2 being PartFunc of COMPLEX,COMPLEX st h1 is total & h2 is total holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
proof end;

theorem :: CFCONT_1:15
for g being Complex
for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX st h is total holds
(g (#) h) /* seq = g (#) (h /* seq)
proof end;

theorem :: CFCONT_1:16
for X being set
for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h | X) & h " = {} holds
((h ^) | X) /* seq = ((h | X) /* seq) "
proof end;

theorem Th17: :: CFCONT_1:17
for seq, seq1 being Complex_Sequence st seq1 is subsequence of seq & seq is convergent holds
seq1 is convergent
proof end;

theorem Th18: :: CFCONT_1:18
for seq, seq1 being Complex_Sequence st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq
proof end;

theorem Th19: :: CFCONT_1:19
for seq, seq1 being Complex_Sequence st seq is convergent & ex k being Nat st
for n being Nat st k <= n holds
seq1 . n = seq . n holds
seq1 is convergent
proof end;

theorem :: CFCONT_1:20
for seq, seq1 being Complex_Sequence st seq is convergent & ex k being Nat st
for n being Nat st k <= n holds
seq1 . n = seq . n holds
lim seq = lim seq1
proof end;

theorem :: CFCONT_1:21
for k being Nat
for seq being Complex_Sequence st seq is convergent holds
( seq ^\ k is convergent & lim (seq ^\ k) = lim seq ) by ;

theorem Th22: :: CFCONT_1:22
for seq, seq1 being Complex_Sequence st seq is convergent & ex k being Nat st seq = seq1 ^\ k holds
seq1 is convergent
proof end;

theorem :: CFCONT_1:23
for seq, seq1 being Complex_Sequence st seq is convergent & ex k being Nat st seq = seq1 ^\ k holds
lim seq1 = lim seq
proof end;

theorem Th24: :: CFCONT_1:24
for seq being Complex_Sequence st seq is convergent & lim seq <> 0 holds
ex k being Nat st seq ^\ k is non-zero
proof end;

theorem :: CFCONT_1:25
for seq being Complex_Sequence st seq is convergent & lim seq <> 0 holds
ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is non-zero )
proof end;

theorem Th26: :: CFCONT_1:26
for seq being Complex_Sequence st seq is constant holds
seq is convergent
proof end;

theorem Th27: :: CFCONT_1:27
for g being Complex
for seq being Complex_Sequence st ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Nat st seq . n = g ) ) holds
lim seq = g
proof end;

theorem :: CFCONT_1:28
for seq being Complex_Sequence st seq is constant holds
for n being Nat holds lim seq = seq . n by Th27;

theorem :: CFCONT_1:29
for seq being Complex_Sequence st seq is convergent & lim seq <> 0 holds
for seq1 being Complex_Sequence st seq1 is subsequence of seq & seq1 is non-zero holds
lim (seq1 ") = (lim seq) "
proof end;

theorem :: CFCONT_1:30
for seq, seq1 being Complex_Sequence st seq is constant & seq1 is convergent holds
( 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 end;

scheme :: CFCONT_1:sch 1
CompSeqChoice{ P1[ object , object ] } :
ex s1 being Complex_Sequence st
for n being Nat holds P1[n,s1 . n]
provided
A1: for n being Nat ex g being Complex st P1[n,g]
proof end;

theorem :: CFCONT_1:31
for x0 being Complex
for f being PartFunc of COMPLEX,COMPLEX holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )
proof end;

theorem Th32: :: CFCONT_1:32
for x0 being Complex
for f being PartFunc of COMPLEX,COMPLEX holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Complex st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
proof end;

theorem Th33: :: CFCONT_1:33
for x0 being Complex
for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 )
proof end;

theorem Th34: :: CFCONT_1:34
for g, x0 being Complex
for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_in x0 holds
g (#) f is_continuous_in x0
proof end;

theorem :: CFCONT_1:35
for x0 being Complex
for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_in x0 holds
- f is_continuous_in x0 by Th34;

theorem Th36: :: CFCONT_1:36
for x0 being Complex
for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_in x0 & f /. x0 <> 0 holds
f ^ is_continuous_in x0
proof end;

theorem :: CFCONT_1:37
for x0 being Complex
for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_in x0 & f1 /. x0 <> 0 & f2 is_continuous_in x0 holds
f2 / f1 is_continuous_in x0
proof end;

definition
let f be PartFunc of COMPLEX,COMPLEX;
let X be set ;
pred f is_continuous_on X means :: CFCONT_1:def 2
( X c= dom f & ( for x0 being Complex st x0 in X holds
f | X is_continuous_in x0 ) );
end;

:: deftheorem defines is_continuous_on CFCONT_1:def 2 :
for f being PartFunc of COMPLEX,COMPLEX
for X being set holds
( f is_continuous_on X iff ( X c= dom f & ( for x0 being Complex st x0 in X holds
f | X is_continuous_in x0 ) ) );

theorem Th38: :: CFCONT_1:38
for X being set
for f being PartFunc of COMPLEX,COMPLEX holds
( f is_continuous_on X iff ( X c= dom f & ( for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) )
proof end;

theorem Th39: :: CFCONT_1:39
for X being set
for f being PartFunc of COMPLEX,COMPLEX holds
( f is_continuous_on X iff ( X c= dom f & ( for x0 being Complex
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Complex st x1 in X & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
proof end;

theorem Th40: :: CFCONT_1:40
for X being set
for f being PartFunc of COMPLEX,COMPLEX holds
( f is_continuous_on X iff f | X is_continuous_on X )
proof end;

theorem Th41: :: CFCONT_1:41
for X, X1 being set
for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X & X1 c= X holds
f is_continuous_on X1
proof end;

theorem :: CFCONT_1:42
for x0 being Complex
for f being PartFunc of COMPLEX,COMPLEX st x0 in dom f holds
f is_continuous_on {x0}
proof end;

theorem Th43: :: CFCONT_1:43
for X being set
for f1, f2 being PartFunc of COMPLEX,COMPLEX 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 end;

theorem :: CFCONT_1:44
for X, X1 being set
for f1, f2 being PartFunc of COMPLEX,COMPLEX 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 end;

theorem Th45: :: CFCONT_1:45
for g being Complex
for X being set
for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X holds
g (#) f is_continuous_on X
proof end;

theorem :: CFCONT_1:46
for X being set
for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X holds
- f is_continuous_on X by Th45;

theorem Th47: :: CFCONT_1:47
for X being set
for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X & f " = {} holds
f ^ is_continuous_on X
proof end;

theorem :: CFCONT_1:48
for X being set
for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X & (f | X) " = {} holds
f ^ is_continuous_on X
proof end;

theorem :: CFCONT_1:49
for X being set
for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_on X & f1 " = {} & f2 is_continuous_on X holds
f2 / f1 is_continuous_on X
proof end;

theorem :: CFCONT_1:50
for f being PartFunc of COMPLEX,COMPLEX st f is total & ( for x1, x2 being Complex holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Complex st f is_continuous_in x0 holds
f is_continuous_on COMPLEX
proof end;

definition
let X be set ;
attr X is compact means :: CFCONT_1:def 3
for s1 being Complex_Sequence st rng s1 c= X holds
ex s2 being Complex_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X );
end;

:: deftheorem defines compact CFCONT_1:def 3 :
for X being set holds
( X is compact iff for s1 being Complex_Sequence st rng s1 c= X holds
ex s2 being Complex_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) );

theorem Th51: :: CFCONT_1:51
for f being PartFunc of COMPLEX,COMPLEX st dom f is compact & f is_continuous_on dom f holds
rng f is compact
proof end;

theorem :: CFCONT_1:52
for Y being Subset of COMPLEX
for f being PartFunc of COMPLEX,COMPLEX st Y c= dom f & Y is compact & f is_continuous_on Y holds
f .: Y is compact
proof end;