:: Property of Complex Sequence and Continuity of Complex Function
:: by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama
::
:: Received December 7, 1999
:: Copyright (c) 1999-2021 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 " {0} = {} 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 Th17, Th18;

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{ P₁[ object , object ] } :

ex s1 being Complex_Sequence st
for n being Nat holds P₁[n,s1 . n]

provided

A1: for n being Nat ex g being Complex st P₁[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 " {0} = {} 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) " {0} = {} 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 " {0} = {} & 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;