:: by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama

::

:: Received December 7, 1999

:: Copyright (c) 1999-2021 Association of Mizar Users

definition

let f be PartFunc of COMPLEX,COMPLEX;

let x0 be Complex;

end;
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) ) ) );

( 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) ) ) );

:: 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) ) ) ) );

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) )

( 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) )

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)

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).| )

for Ns being V42() sequence of NAT holds

( (- seq) * Ns = - (seq * Ns) & |.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)

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) )

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)

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

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

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) "

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))

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))

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) )

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)

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) "

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

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

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

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

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;

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

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

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

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 )

ex seq1 being Complex_Sequence st

( seq1 is subsequence of seq & seq1 is non-zero )

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

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

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) "

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) )

( 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;

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) ) ) ) )

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 ) ) ) ) )

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 )

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

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;

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

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

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 ;

end;
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 ) );

( X c= dom f & ( for x0 being Complex st x0 in X holds

f | X is_continuous_in x0 ) );

:: 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 ) ) );

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) ) ) ) )

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 ) ) ) ) )

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 )

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

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}

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 )

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 )

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

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;

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

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

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

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

f is_continuous_on COMPLEX

proof end;

definition

let X be set ;

end;
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 );

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 );

:: 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 ) );

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

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

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;

:: COMPLEX SEQUENCE

::