:: CFCONT_1 semantic presentation

definition

let h be PartFunc of COMPLEX , COMPLEX ;
let seq be Complex_Sequence;
assume A1: rng seq c= dom h ;
func h * seq -> Complex_Sequence equals :Def1: :: CFCONT_1:def 1
h * seq;
coherence

proof end;

end;

:: deftheorem Def1 defines * CFCONT_1:def 1 :

definition

let f be PartFunc of COMPLEX , COMPLEX ;
let x0 be Element of COMPLEX ;
pred f is_continuous_in x0 means :Def2: :: CFCONT_1:def 2
( 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 Def2 defines is_continuous_in CFCONT_1:def 2 :

theorem :: CFCONT_1:1

canceled;

theorem Th2: :: CFCONT_1:2

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 Th3: :: CFCONT_1:3

for n being Nat
for seq being Complex_Sequence holds rng (seq ^\ n) c= rng seq

proof end;

theorem Th4: :: CFCONT_1:4

for n being Nat
for seq being Complex_Sequence
for f being PartFunc of COMPLEX , COMPLEX st rng seq c= dom f holds
seq . n in dom f

proof end;

theorem Th5: :: CFCONT_1:5

for x being set
for seq being Complex_Sequence holds
( x in rng seq iff ex n being Nat st x = seq . n )

proof end;

theorem :: CFCONT_1:6

for n being Nat
for seq being Complex_Sequence holds seq . n in rng seq by Th5;

theorem Th7: :: CFCONT_1:7

for seq1, seq being Complex_Sequence st seq1 is subsequence of seq holds
rng seq1 c= rng seq

proof end;

theorem :: CFCONT_1:8

for seq1, seq being Complex_Sequence st seq1 is subsequence of seq & seq is non-zero holds
seq1 is non-zero

proof end;

theorem Th9: :: CFCONT_1:9

for seq1, seq2 being Complex_Sequence
for Ns being increasing Seq_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 Th10: :: CFCONT_1:10

for g being Element of COMPLEX
for seq being Complex_Sequence
for Ns being increasing Seq_of_Nat holds (g (#) seq) * Ns = g (#) (seq * Ns)

proof end;

theorem :: CFCONT_1:11

for seq being Complex_Sequence
for Ns being increasing Seq_of_Nat holds
( (- seq) * Ns = - (seq * Ns) & |.seq.| * Ns = |.(seq * Ns).| )

proof end;

theorem Th12: :: CFCONT_1:12

for seq being Complex_Sequence
for Ns being increasing Seq_of_Nat holds (seq * Ns) " = (seq " ) * Ns

proof end;

theorem :: CFCONT_1:13

for seq1, seq being Complex_Sequence
for Ns being increasing Seq_of_Nat holds (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns)

proof end;

theorem :: CFCONT_1:14

for seq being Complex_Sequence
for Y being Subset of COMPLEX st ( for n being Nat holds seq . n in Y ) holds
rng seq c= Y

proof end;

theorem :: CFCONT_1:15

canceled;

theorem Th16: :: CFCONT_1:16

for n being Nat
for seq being Complex_Sequence
for f being PartFunc of COMPLEX , COMPLEX st rng seq c= dom f holds
(f * seq) . n = f /. (seq . n)

proof end;

theorem Th17: :: CFCONT_1:17

for n being Nat
for seq being Complex_Sequence
for f being PartFunc of COMPLEX , COMPLEX st rng seq c= dom f holds
(f * seq) ^\ n = f * (seq ^\ n)

proof end;

theorem Th18: :: CFCONT_1:18

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 Th19: :: CFCONT_1:19

for g being Element of 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:20

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 Th21: :: CFCONT_1:21

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 Th22: :: CFCONT_1:22

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 Th23: :: CFCONT_1:23

for seq being Complex_Sequence
for h being PartFunc of COMPLEX , COMPLEX
for Ns being increasing Seq_of_Nat st rng seq c= dom h holds
Re ((h * seq) * Ns) = Re (h * (seq * Ns))

proof end;

theorem Th24: :: CFCONT_1:24

for seq being Complex_Sequence
for h being PartFunc of COMPLEX , COMPLEX
for Ns being increasing Seq_of_Nat st rng seq c= dom h holds
Im ((h * seq) * Ns) = Im (h * (seq * Ns))

proof end;

theorem Th25: :: CFCONT_1:25

for seq being Complex_Sequence
for h being PartFunc of COMPLEX , COMPLEX
for Ns being increasing Seq_of_Nat st rng seq c= dom h holds
(h * seq) * Ns = h * (seq * Ns)

proof end;

theorem Th26: :: CFCONT_1:26

for seq1, seq2 being Complex_Sequence
for h being PartFunc of COMPLEX , COMPLEX st rng seq1 c= dom h & seq2 is subsequence of seq1 holds
h * seq2 is subsequence of h * seq1

proof end;

theorem :: CFCONT_1:27

for n being Nat
for seq being Complex_Sequence
for h being PartFunc of COMPLEX , COMPLEX st h is total holds
(h * seq) . n = h /. (seq . n)

proof end;

theorem :: CFCONT_1:28

for n being Nat
for seq being Complex_Sequence
for h being PartFunc of COMPLEX , COMPLEX st h is total holds
h * (seq ^\ n) = (h * seq) ^\ n

proof end;

theorem :: CFCONT_1:29

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:30

for g being Element of 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:31

for X being set
for seq being Complex_Sequence
for h being PartFunc of COMPLEX , COMPLEX st rng seq c= dom (h | X) holds
(h | X) * seq = h * seq

proof end;

theorem :: CFCONT_1:32

for X being set
for seq being Complex_Sequence
for Y being Subset of COMPLEX
for h being PartFunc of COMPLEX , COMPLEX st rng seq c= dom (h | X) & ( rng seq c= dom (h | Y) or X c= Y ) holds
(h | X) * seq = (h | Y) * seq

proof end;

theorem :: CFCONT_1:33

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;

definition

let seq be Complex_Sequence;
canceled;
redefine attr seq is constant means :Def4: :: CFCONT_1:def 4
ex g being Element of COMPLEX st
for n being Nat holds seq . n = g;
compatibility

proof end;

end;

:: deftheorem CFCONT_1:def 3 :

:: deftheorem Def4 defines constant CFCONT_1:def 4 :

Lm1: for seq being Complex_Sequence holds
( ( ex g being Element of COMPLEX st
for n being Nat holds seq . n = g implies ex g being Element of COMPLEX st rng seq = {g} ) & ( ex g being Element of COMPLEX st rng seq = {g} implies for n being Nat holds seq . n = seq . (n + 1) ) & ( ( for n being Nat holds seq . n = seq . (n + 1) ) implies for n, k being Nat holds seq . n = seq . (n + k) ) & ( ( for n, k being Nat holds seq . n = seq . (n + k) ) implies for n, m being Nat holds seq . n = seq . m ) & ( ( for n, m being Nat holds seq . n = seq . m ) implies ex g being Element of COMPLEX st
for n being Nat holds seq . n = g ) )

proof end;

theorem Th34: :: CFCONT_1:34

for seq being Complex_Sequence holds
( seq is constant iff ex g being Element of COMPLEX st rng seq = {g} )

proof end;

theorem Th35: :: CFCONT_1:35

for seq being Complex_Sequence holds
( seq is constant iff for n being Nat holds seq . n = seq . (n + 1) )

proof end;

theorem Th36: :: CFCONT_1:36

for seq being Complex_Sequence holds
( seq is constant iff for n, k being Nat holds seq . n = seq . (n + k) )

proof end;

theorem :: CFCONT_1:37

for seq being Complex_Sequence holds
( seq is constant iff for n, m being Nat holds seq . n = seq . m )

proof end;

theorem Th38: :: CFCONT_1:38

for k being Nat
for seq being Complex_Sequence holds seq ^\ k is subsequence of seq

proof end;

theorem Th39: :: CFCONT_1:39

for seq1, seq being Complex_Sequence st seq1 is subsequence of seq & seq is convergent holds
seq1 is convergent

proof end;

theorem Th40: :: CFCONT_1:40

for seq1, seq being Complex_Sequence st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq

proof end;

theorem Th41: :: CFCONT_1:41

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:42

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 Th43: :: CFCONT_1:43

for k being Nat
for seq being Complex_Sequence st seq is convergent holds
( seq ^\ k is convergent & lim (seq ^\ k) = lim seq )

proof end;

theorem Th44: :: CFCONT_1:44

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:45

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 Th46: :: CFCONT_1:46

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:47

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 Th48: :: CFCONT_1:48

for seq being Complex_Sequence st seq is constant holds
seq is convergent

proof end;

theorem Th49: :: CFCONT_1:49

for g being Element of 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:50

for seq being Complex_Sequence st seq is constant holds
for n being Nat holds lim seq = seq . n by Th49;

theorem :: CFCONT_1:51

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:52

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₁[ set , set ] } :

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

provided

A1: for n being Nat ex g being Element of COMPLEX st P₁[n,g]

proof end;

theorem :: CFCONT_1:53

for x0 being Element of 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 Th54: :: CFCONT_1:54

for x0 being Element of 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 Element of COMPLEX st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )

proof end;

theorem Th55: :: CFCONT_1:55

for x0 being Element of 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 Th56: :: CFCONT_1:56

for x0, g being Element of 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:57

for x0 being Element of COMPLEX
for f being PartFunc of COMPLEX , COMPLEX st f is_continuous_in x0 holds
- f is_continuous_in x0

proof end;

theorem Th58: :: CFCONT_1:58

for x0 being Element of 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:59

for x0 being Element of 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 :Def5: :: CFCONT_1:def 5
( X c= dom f & ( for x0 being Element of COMPLEX st x0 in X holds
f | X is_continuous_in x0 ) );

end;

:: deftheorem Def5 defines is_continuous_on CFCONT_1:def 5 :

theorem Th60: :: CFCONT_1:60

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 Th61: :: CFCONT_1:61

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 Element of COMPLEX
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )

proof end;

theorem Th62: :: CFCONT_1:62

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 Th63: :: CFCONT_1:63

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:64

for x0 being Element of COMPLEX
for f being PartFunc of COMPLEX , COMPLEX st x0 in dom f holds
f is_continuous_on {x0}

proof end;

theorem Th65: :: CFCONT_1:65

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:66

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 Th67: :: CFCONT_1:67

for g being Element of 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:68

for X being set
for f being PartFunc of COMPLEX , COMPLEX st f is_continuous_on X holds
- f is_continuous_on X

proof end;

theorem Th69: :: CFCONT_1:69

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:70

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:71

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:72

for f being PartFunc of COMPLEX , COMPLEX st f is total & ( for x1, x2 being Element of COMPLEX holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Element of 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 :Def6: :: CFCONT_1:def 6
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 Def6 defines compact CFCONT_1:def 6 :

theorem Th73: :: CFCONT_1:73

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:74

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;