:: CFCONT_1 semantic presentation
begin
definition
let f be PartFunc of COMPLEX,COMPLEX;
let x0 be Element of COMPLEX ;
predf is_continuous_in x0 means :Def1: :: 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 Def1 defines is_continuous_in CFCONT_1:def_1_:_
for f being PartFunc of COMPLEX,COMPLEX
for x0 being Element of 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 Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) )
proof
let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: ( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) )
thus ( seq1 = seq2 - seq3 implies for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) ::_thesis: ( ( for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) implies seq1 = seq2 - seq3 )
proof
assume A1: seq1 = seq2 - seq3 ; ::_thesis: for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n)
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_(seq2_._n)_-_(seq3_._n)
let n be Element of NAT ; ::_thesis: seq1 . n = (seq2 . n) - (seq3 . n)
seq1 . n = (seq2 . n) + ((- seq3) . n) by A1, VALUED_1:1;
then seq1 . n = (seq2 . n) + (- (seq3 . n)) by VALUED_1:8;
hence seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: verum
end;
hence for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: verum
end;
assume A2: for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: seq1 = seq2 - seq3
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_(seq2_+_(-_seq3))_._n
let n be Element of NAT ; ::_thesis: seq1 . n = (seq2 + (- seq3)) . n
thus seq1 . n = (seq2 . n) - (seq3 . n) by A2
.= (seq2 . n) + (- (seq3 . n))
.= (seq2 . n) + ((- seq3) . n) by VALUED_1:8
.= (seq2 + (- seq3)) . n by VALUED_1:1 ; ::_thesis: verum
end;
hence seq1 = seq2 - seq3 by FUNCT_2:63; ::_thesis: verum
end;
theorem Th2: :: CFCONT_1:2
for seq1, seq2 being Complex_Sequence
for Ns being V37() 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
let seq1, seq2 be Complex_Sequence; ::_thesis: for Ns being V37() 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) )
let Ns be V37() sequence of NAT; ::_thesis: ( (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) & (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_+_seq2)_*_Ns)_._n_=_((seq1_*_Ns)_+_(seq2_*_Ns))_._n
let n be Element of NAT ; ::_thesis: ((seq1 + seq2) * Ns) . n = ((seq1 * Ns) + (seq2 * Ns)) . n
thus ((seq1 + seq2) * Ns) . n = (seq1 + seq2) . (Ns . n) by FUNCT_2:15
.= (seq1 . (Ns . n)) + (seq2 . (Ns . n)) by VALUED_1:1
.= ((seq1 * Ns) . n) + (seq2 . (Ns . n)) by FUNCT_2:15
.= ((seq1 * Ns) . n) + ((seq2 * Ns) . n) by FUNCT_2:15
.= ((seq1 * Ns) + (seq2 * Ns)) . n by VALUED_1:1 ; ::_thesis: verum
end;
hence (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) by FUNCT_2:63; ::_thesis: ( (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_-_seq2)_*_Ns)_._n_=_((seq1_*_Ns)_-_(seq2_*_Ns))_._n
let n be Element of NAT ; ::_thesis: ((seq1 - seq2) * Ns) . n = ((seq1 * Ns) - (seq2 * Ns)) . n
thus ((seq1 - seq2) * Ns) . n = (seq1 - seq2) . (Ns . n) by FUNCT_2:15
.= (seq1 . (Ns . n)) - (seq2 . (Ns . n)) by Th1
.= ((seq1 * Ns) . n) - (seq2 . (Ns . n)) by FUNCT_2:15
.= ((seq1 * Ns) . n) - ((seq2 * Ns) . n) by FUNCT_2:15
.= ((seq1 * Ns) - (seq2 * Ns)) . n by Th1 ; ::_thesis: verum
end;
hence (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) by FUNCT_2:63; ::_thesis: (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_(#)_seq2)_*_Ns)_._n_=_((seq1_*_Ns)_(#)_(seq2_*_Ns))_._n
let n be Element of NAT ; ::_thesis: ((seq1 (#) seq2) * Ns) . n = ((seq1 * Ns) (#) (seq2 * Ns)) . n
thus ((seq1 (#) seq2) * Ns) . n = (seq1 (#) seq2) . (Ns . n) by FUNCT_2:15
.= (seq1 . (Ns . n)) * (seq2 . (Ns . n)) by VALUED_1:5
.= ((seq1 * Ns) . n) * (seq2 . (Ns . n)) by FUNCT_2:15
.= ((seq1 * Ns) . n) * ((seq2 * Ns) . n) by FUNCT_2:15
.= ((seq1 * Ns) (#) (seq2 * Ns)) . n by VALUED_1:5 ; ::_thesis: verum
end;
hence (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th3: :: CFCONT_1:3
for g being Element of COMPLEX
for seq being Complex_Sequence
for Ns being V37() sequence of NAT holds (g (#) seq) * Ns = g (#) (seq * Ns)
proof
let g be Element of COMPLEX ; ::_thesis: for seq being Complex_Sequence
for Ns being V37() sequence of NAT holds (g (#) seq) * Ns = g (#) (seq * Ns)
let seq be Complex_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds (g (#) seq) * Ns = g (#) (seq * Ns)
let Ns be V37() sequence of NAT; ::_thesis: (g (#) seq) * Ns = g (#) (seq * Ns)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((g_(#)_seq)_*_Ns)_._n_=_(g_(#)_(seq_*_Ns))_._n
let n be Element of NAT ; ::_thesis: ((g (#) seq) * Ns) . n = (g (#) (seq * Ns)) . n
thus ((g (#) seq) * Ns) . n = (g (#) seq) . (Ns . n) by FUNCT_2:15
.= g * (seq . (Ns . n)) by VALUED_1:6
.= g * ((seq * Ns) . n) by FUNCT_2:15
.= (g (#) (seq * Ns)) . n by VALUED_1:6 ; ::_thesis: verum
end;
hence (g (#) seq) * Ns = g (#) (seq * Ns) by FUNCT_2:63; ::_thesis: verum
end;
theorem :: CFCONT_1:4
for seq being Complex_Sequence
for Ns being V37() sequence of NAT holds
( (- seq) * Ns = - (seq * Ns) & |.seq.| * Ns = |.(seq * Ns).| )
proof
let seq be Complex_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds
( (- seq) * Ns = - (seq * Ns) & |.seq.| * Ns = |.(seq * Ns).| )
let Ns be V37() sequence of NAT; ::_thesis: ( (- seq) * Ns = - (seq * Ns) & |.seq.| * Ns = |.(seq * Ns).| )
thus (- seq) * Ns = ((- 1r) (#) seq) * Ns by COMSEQ_1:11
.= (- 1r) (#) (seq * Ns) by Th3
.= - (seq * Ns) by COMSEQ_1:11 ; ::_thesis: |.seq.| * Ns = |.(seq * Ns).|
now__::_thesis:_for_n_being_Element_of_NAT_holds_(|.seq.|_*_Ns)_._n_=_|.(seq_*_Ns).|_._n
let n be Element of NAT ; ::_thesis: (|.seq.| * Ns) . n = |.(seq * Ns).| . n
thus (|.seq.| * Ns) . n = |.seq.| . (Ns . n) by FUNCT_2:15
.= |.(seq . (Ns . n)).| by VALUED_1:18
.= |.((seq * Ns) . n).| by FUNCT_2:15
.= |.(seq * Ns).| . n by VALUED_1:18 ; ::_thesis: verum
end;
hence |.seq.| * Ns = |.(seq * Ns).| by FUNCT_2:63; ::_thesis: verum
end;
theorem Th5: :: CFCONT_1:5
for seq being Complex_Sequence
for Ns being V37() sequence of NAT holds (seq * Ns) " = (seq ") * Ns
proof
let seq be Complex_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds (seq * Ns) " = (seq ") * Ns
let Ns be V37() sequence of NAT; ::_thesis: (seq * Ns) " = (seq ") * Ns
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_*_Ns)_")_._n_=_((seq_")_*_Ns)_._n
let n be Element of NAT ; ::_thesis: ((seq * Ns) ") . n = ((seq ") * Ns) . n
thus ((seq * Ns) ") . n = ((seq * Ns) . n) " by VALUED_1:10
.= (seq . (Ns . n)) " by FUNCT_2:15
.= (seq ") . (Ns . n) by VALUED_1:10
.= ((seq ") * Ns) . n by FUNCT_2:15 ; ::_thesis: verum
end;
hence (seq * Ns) " = (seq ") * Ns by FUNCT_2:63; ::_thesis: verum
end;
theorem :: CFCONT_1:6
for seq1, seq being Complex_Sequence
for Ns being V37() sequence of NAT holds (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns)
proof
let seq1, seq be Complex_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns)
let Ns be V37() sequence of NAT; ::_thesis: (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns)
thus (seq1 /" seq) * Ns = (seq1 * Ns) (#) ((seq ") * Ns) by Th2
.= (seq1 * Ns) /" (seq * Ns) by Th5 ; ::_thesis: verum
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
let seq be Complex_Sequence; ::_thesis: 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) )
let h1, h2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( 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) ) )
A1: (dom h1) /\ (dom h2) c= dom h1 by XBOOLE_1:17;
A2: (dom h1) /\ (dom h2) c= dom h2 by XBOOLE_1:17;
assume A3: rng seq c= (dom h1) /\ (dom h2) ; ::_thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
then A4: rng seq c= dom (h1 + h2) by VALUED_1:def_1;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_+_h2)_/*_seq)_._n_=_((h1_/*_seq)_+_(h2_/*_seq))_._n
let n be Element of NAT ; ::_thesis: ((h1 + h2) /* seq) . n = ((h1 /* seq) + (h2 /* seq)) . n
A5: seq . n in rng seq by VALUED_0:28;
thus ((h1 + h2) /* seq) . n = (h1 + h2) /. (seq . n) by A4, FUNCT_2:109
.= (h1 /. (seq . n)) + (h2 /. (seq . n)) by A4, A5, CFUNCT_1:1
.= ((h1 /* seq) . n) + (h2 /. (seq . n)) by A3, A1, FUNCT_2:109, XBOOLE_1:1
.= ((h1 /* seq) . n) + ((h2 /* seq) . n) by A3, A2, FUNCT_2:109, XBOOLE_1:1
.= ((h1 /* seq) + (h2 /* seq)) . n by VALUED_1:1 ; ::_thesis: verum
end;
hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by FUNCT_2:63; ::_thesis: ( (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
A6: rng seq c= dom (h1 - h2) by A3, CFUNCT_1:2;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_-_h2)_/*_seq)_._n_=_((h1_/*_seq)_._n)_-_((h2_/*_seq)_._n)
let n be Element of NAT ; ::_thesis: ((h1 - h2) /* seq) . n = ((h1 /* seq) . n) - ((h2 /* seq) . n)
A7: seq . n in rng seq by VALUED_0:28;
thus ((h1 - h2) /* seq) . n = (h1 - h2) /. (seq . n) by A6, FUNCT_2:109
.= (h1 /. (seq . n)) - (h2 /. (seq . n)) by A6, A7, CFUNCT_1:2
.= ((h1 /* seq) . n) - (h2 /. (seq . n)) by A3, A1, FUNCT_2:109, XBOOLE_1:1
.= ((h1 /* seq) . n) - ((h2 /* seq) . n) by A3, A2, FUNCT_2:109, XBOOLE_1:1 ; ::_thesis: verum
end;
hence (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by Th1; ::_thesis: (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq)
A8: rng seq c= dom (h1 (#) h2) by A3, VALUED_1:def_4;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_(#)_h2)_/*_seq)_._n_=_((h1_/*_seq)_(#)_(h2_/*_seq))_._n
let n be Element of NAT ; ::_thesis: ((h1 (#) h2) /* seq) . n = ((h1 /* seq) (#) (h2 /* seq)) . n
A9: seq . n in rng seq by VALUED_0:28;
thus ((h1 (#) h2) /* seq) . n = (h1 (#) h2) /. (seq . n) by A8, FUNCT_2:109
.= (h1 /. (seq . n)) * (h2 /. (seq . n)) by A8, A9, CFUNCT_1:3
.= ((h1 /* seq) . n) * (h2 /. (seq . n)) by A3, A1, FUNCT_2:109, XBOOLE_1:1
.= ((h1 /* seq) . n) * ((h2 /* seq) . n) by A3, A2, FUNCT_2:109, XBOOLE_1:1
.= ((h1 /* seq) (#) (h2 /* seq)) . n by VALUED_1:5 ; ::_thesis: verum
end;
hence (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th8: :: CFCONT_1:8
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
let g be Element of COMPLEX ; ::_thesis: 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)
let seq be Complex_Sequence; ::_thesis: for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom h holds
(g (#) h) /* seq = g (#) (h /* seq)
let h be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( rng seq c= dom h implies (g (#) h) /* seq = g (#) (h /* seq) )
assume A1: rng seq c= dom h ; ::_thesis: (g (#) h) /* seq = g (#) (h /* seq)
then A2: rng seq c= dom (g (#) h) by VALUED_1:def_5;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((g_(#)_h)_/*_seq)_._n_=_(g_(#)_(h_/*_seq))_._n
let n be Element of NAT ; ::_thesis: ((g (#) h) /* seq) . n = (g (#) (h /* seq)) . n
A3: seq . n in rng seq by VALUED_0:28;
thus ((g (#) h) /* seq) . n = (g (#) h) /. (seq . n) by A2, FUNCT_2:109
.= g * (h /. (seq . n)) by A2, A3, CFUNCT_1:4
.= g * ((h /* seq) . n) by A1, FUNCT_2:109
.= (g (#) (h /* seq)) . n by VALUED_1:6 ; ::_thesis: verum
end;
hence (g (#) h) /* seq = g (#) (h /* seq) by FUNCT_2:63; ::_thesis: verum
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
proof
let seq be Complex_Sequence; ::_thesis: for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom h holds
- (h /* seq) = (- h) /* seq
let h be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( rng seq c= dom h implies - (h /* seq) = (- h) /* seq )
assume A1: rng seq c= dom h ; ::_thesis: - (h /* seq) = (- h) /* seq
thus - (h /* seq) = (- 1r) (#) (h /* seq) by COMSEQ_1:11
.= ((- 1r) (#) h) /* seq by A1, Th8
.= (- h) /* seq by CFUNCT_1:31 ; ::_thesis: verum
end;
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
let seq be Complex_Sequence; ::_thesis: for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h ^) holds
h /* seq is non-zero
let h be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( rng seq c= dom (h ^) implies h /* seq is non-zero )
assume A1: rng seq c= dom (h ^) ; ::_thesis: h /* seq is non-zero
then A2: ( (dom h) \ (h " {0c}) c= dom h & rng seq c= (dom h) \ (h " {0c}) ) by CFUNCT_1:def_2, XBOOLE_1:36;
now__::_thesis:_for_n_being_Element_of_NAT_holds_not_(h_/*_seq)_._n_=_0c
given n being Element of NAT such that A3: (h /* seq) . n = 0c ; ::_thesis: contradiction
seq . n in rng seq by VALUED_0:28;
then seq . n in dom (h ^) by A1;
then seq . n in (dom h) \ (h " {0c}) by CFUNCT_1:def_2;
then ( seq . n in dom h & not seq . n in h " {0c} ) by XBOOLE_0:def_5;
then A4: not h /. (seq . n) in {0c} by PARTFUN2:26;
h /. (seq . n) = 0c by A2, A3, FUNCT_2:109, XBOOLE_1:1;
hence contradiction by A4, TARSKI:def_1; ::_thesis: verum
end;
hence h /* seq is non-zero by COMSEQ_1:4; ::_thesis: verum
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
let seq be Complex_Sequence; ::_thesis: for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h ^) holds
(h ^) /* seq = (h /* seq) "
let h be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( rng seq c= dom (h ^) implies (h ^) /* seq = (h /* seq) " )
assume A1: rng seq c= dom (h ^) ; ::_thesis: (h ^) /* seq = (h /* seq) "
then A2: ( (dom h) \ (h " {0c}) c= dom h & rng seq c= (dom h) \ (h " {0c}) ) by CFUNCT_1:def_2, XBOOLE_1:36;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h_^)_/*_seq)_._n_=_((h_/*_seq)_")_._n
let n be Element of NAT ; ::_thesis: ((h ^) /* seq) . n = ((h /* seq) ") . n
A3: seq . n in rng seq by VALUED_0:28;
thus ((h ^) /* seq) . n = (h ^) /. (seq . n) by A1, FUNCT_2:109
.= (h /. (seq . n)) " by A1, A3, CFUNCT_1:def_2
.= ((h /* seq) . n) " by A2, FUNCT_2:109, XBOOLE_1:1
.= ((h /* seq) ") . n by VALUED_1:10 ; ::_thesis: verum
end;
hence (h ^) /* seq = (h /* seq) " by FUNCT_2:63; ::_thesis: verum
end;
theorem :: CFCONT_1:12
for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX
for Ns being V37() sequence of NAT st rng seq c= dom h holds
Re ((h /* seq) * Ns) = Re (h /* (seq * Ns))
proof
let seq be Complex_Sequence; ::_thesis: for h being PartFunc of COMPLEX,COMPLEX
for Ns being V37() sequence of NAT st rng seq c= dom h holds
Re ((h /* seq) * Ns) = Re (h /* (seq * Ns))
let h be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Ns being V37() sequence of NAT st rng seq c= dom h holds
Re ((h /* seq) * Ns) = Re (h /* (seq * Ns))
let Ns be V37() sequence of NAT; ::_thesis: ( rng seq c= dom h implies Re ((h /* seq) * Ns) = Re (h /* (seq * Ns)) )
assume A1: rng seq c= dom h ; ::_thesis: Re ((h /* seq) * Ns) = Re (h /* (seq * Ns))
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Re_((h_/*_seq)_*_Ns))_._n_=_(Re_(h_/*_(seq_*_Ns)))_._n
let n be Element of NAT ; ::_thesis: (Re ((h /* seq) * Ns)) . n = (Re (h /* (seq * Ns))) . n
seq * Ns is subsequence of seq by VALUED_0:def_17;
then A2: rng (seq * Ns) c= rng seq by VALUED_0:21;
thus (Re ((h /* seq) * Ns)) . n = Re (((h /* seq) * Ns) . n) by COMSEQ_3:def_5
.= Re ((h /* seq) . (Ns . n)) by FUNCT_2:15
.= Re (h /. (seq . (Ns . n))) by A1, FUNCT_2:109
.= Re (h /. ((seq * Ns) . n)) by FUNCT_2:15
.= Re ((h /* (seq * Ns)) . n) by A1, A2, FUNCT_2:109, XBOOLE_1:1
.= (Re (h /* (seq * Ns))) . n by COMSEQ_3:def_5 ; ::_thesis: verum
end;
hence Re ((h /* seq) * Ns) = Re (h /* (seq * Ns)) by FUNCT_2:63; ::_thesis: verum
end;
theorem :: CFCONT_1:13
for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX
for Ns being V37() sequence of NAT st rng seq c= dom h holds
Im ((h /* seq) * Ns) = Im (h /* (seq * Ns))
proof
let seq be Complex_Sequence; ::_thesis: for h being PartFunc of COMPLEX,COMPLEX
for Ns being V37() sequence of NAT st rng seq c= dom h holds
Im ((h /* seq) * Ns) = Im (h /* (seq * Ns))
let h be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Ns being V37() sequence of NAT st rng seq c= dom h holds
Im ((h /* seq) * Ns) = Im (h /* (seq * Ns))
let Ns be V37() sequence of NAT; ::_thesis: ( rng seq c= dom h implies Im ((h /* seq) * Ns) = Im (h /* (seq * Ns)) )
assume A1: rng seq c= dom h ; ::_thesis: Im ((h /* seq) * Ns) = Im (h /* (seq * Ns))
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Im_((h_/*_seq)_*_Ns))_._n_=_(Im_(h_/*_(seq_*_Ns)))_._n
let n be Element of NAT ; ::_thesis: (Im ((h /* seq) * Ns)) . n = (Im (h /* (seq * Ns))) . n
seq * Ns is subsequence of seq by VALUED_0:def_17;
then A2: rng (seq * Ns) c= rng seq by VALUED_0:21;
thus (Im ((h /* seq) * Ns)) . n = Im (((h /* seq) * Ns) . n) by COMSEQ_3:def_6
.= Im ((h /* seq) . (Ns . n)) by FUNCT_2:15
.= Im (h /. (seq . (Ns . n))) by A1, FUNCT_2:109
.= Im (h /. ((seq * Ns) . n)) by FUNCT_2:15
.= Im ((h /* (seq * Ns)) . n) by A1, A2, FUNCT_2:109, XBOOLE_1:1
.= (Im (h /* (seq * Ns))) . n by COMSEQ_3:def_6 ; ::_thesis: verum
end;
hence Im ((h /* seq) * Ns) = Im (h /* (seq * Ns)) by FUNCT_2:63; ::_thesis: verum
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
let seq be Complex_Sequence; ::_thesis: 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) )
let h1, h2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( 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) ) )
assume ( h1 is total & h2 is total ) ; ::_thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
then dom (h1 + h2) = COMPLEX by PARTFUN1:def_2;
then (dom h1) /\ (dom h2) = COMPLEX by VALUED_1:def_1;
then A1: rng seq c= (dom h1) /\ (dom h2) ;
hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by Th7; ::_thesis: ( (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) )
thus (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by A1, Th7; ::_thesis: (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq)
thus (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) by A1, Th7; ::_thesis: verum
end;
theorem :: CFCONT_1:15
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
let g be Element of COMPLEX ; ::_thesis: for seq being Complex_Sequence
for h being PartFunc of COMPLEX,COMPLEX st h is total holds
(g (#) h) /* seq = g (#) (h /* seq)
let seq be Complex_Sequence; ::_thesis: for h being PartFunc of COMPLEX,COMPLEX st h is total holds
(g (#) h) /* seq = g (#) (h /* seq)
let h be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( h is total implies (g (#) h) /* seq = g (#) (h /* seq) )
assume h is total ; ::_thesis: (g (#) h) /* seq = g (#) (h /* seq)
then dom h = COMPLEX by PARTFUN1:def_2;
then rng seq c= dom h ;
hence (g (#) h) /* seq = g (#) (h /* seq) by Th8; ::_thesis: verum
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
let X be set ; ::_thesis: 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) "
let seq be Complex_Sequence; ::_thesis: for h being PartFunc of COMPLEX,COMPLEX st rng seq c= dom (h | X) & h " {0} = {} holds
((h ^) | X) /* seq = ((h | X) /* seq) "
let h be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( rng seq c= dom (h | X) & h " {0} = {} implies ((h ^) | X) /* seq = ((h | X) /* seq) " )
assume that
A1: rng seq c= dom (h | X) and
A2: h " {0} = {} ; ::_thesis: ((h ^) | X) /* seq = ((h | X) /* seq) "
now__::_thesis:_for_x_being_set_st_x_in_rng_seq_holds_
x_in_dom_((h_^)_|_X)
let x be set ; ::_thesis: ( x in rng seq implies x in dom ((h ^) | X) )
assume x in rng seq ; ::_thesis: x in dom ((h ^) | X)
then x in dom (h | X) by A1;
then A3: x in (dom h) /\ X by RELAT_1:61;
then x in (dom h) \ (h " {0c}) by A2, XBOOLE_0:def_4;
then A4: x in dom (h ^) by CFUNCT_1:def_2;
x in X by A3, XBOOLE_0:def_4;
then x in (dom (h ^)) /\ X by A4, XBOOLE_0:def_4;
hence x in dom ((h ^) | X) by RELAT_1:61; ::_thesis: verum
end;
then A5: rng seq c= dom ((h ^) | X) by TARSKI:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(((h_^)_|_X)_/*_seq)_._n_=_(((h_|_X)_/*_seq)_")_._n
let n be Element of NAT ; ::_thesis: (((h ^) | X) /* seq) . n = (((h | X) /* seq) ") . n
A6: seq . n in rng seq by VALUED_0:28;
then seq . n in dom (h | X) by A1;
then A7: seq . n in (dom h) /\ X by RELAT_1:61;
then seq . n in (dom h) \ (h " {0c}) by A2, XBOOLE_0:def_4;
then A8: seq . n in dom (h ^) by CFUNCT_1:def_2;
seq . n in X by A7, XBOOLE_0:def_4;
then seq . n in (dom (h ^)) /\ X by A8, XBOOLE_0:def_4;
then A9: seq . n in dom ((h ^) | X) by RELAT_1:61;
thus (((h ^) | X) /* seq) . n = ((h ^) | X) /. (seq . n) by A5, FUNCT_2:109
.= (h ^) /. (seq . n) by A9, PARTFUN2:15
.= (h /. (seq . n)) " by A8, CFUNCT_1:def_2
.= ((h | X) /. (seq . n)) " by A1, A6, PARTFUN2:15
.= (((h | X) /* seq) . n) " by A1, FUNCT_2:109
.= (((h | X) /* seq) ") . n by VALUED_1:10 ; ::_thesis: verum
end;
hence ((h ^) | X) /* seq = ((h | X) /* seq) " by FUNCT_2:63; ::_thesis: verum
end;
theorem Th17: :: CFCONT_1:17
for seq1, seq being Complex_Sequence st seq1 is subsequence of seq & seq is convergent holds
seq1 is convergent
proof
let seq1, seq be Complex_Sequence; ::_thesis: ( seq1 is subsequence of seq & seq is convergent implies seq1 is convergent )
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent ; ::_thesis: seq1 is convergent
consider g being Element of COMPLEX such that
A3: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g).| < p by A2, COMSEQ_2:def_5;
take t = g; :: according to COMSEQ_2:def_5 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= |.K65((seq1 . b3),t).| ) )
let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= |.K65((seq1 . b2),t).| ) )
assume 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= |.K65((seq1 . b2),t).| )
then consider n1 being Element of NAT such that
A4: for m being Element of NAT st n1 <= m holds
|.((seq . m) - g).| < p by A3;
take n = n1; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= |.K65((seq1 . b1),t).| )
let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= |.K65((seq1 . m),t).| )
assume A5: n <= m ; ::_thesis: not p <= |.K65((seq1 . m),t).|
consider Nseq being V37() sequence of NAT such that
A6: seq1 = seq * Nseq by A1, VALUED_0:def_17;
m <= Nseq . m by SEQM_3:14;
then A7: n <= Nseq . m by A5, XXREAL_0:2;
seq1 . m = seq . (Nseq . m) by A6, FUNCT_2:15;
hence |.((seq1 . m) - t).| < p by A4, A7; ::_thesis: verum
end;
theorem Th18: :: CFCONT_1:18
for seq1, seq being Complex_Sequence st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq
proof
let seq1, seq be Complex_Sequence; ::_thesis: ( seq1 is subsequence of seq & seq is convergent implies lim seq1 = lim seq )
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent ; ::_thesis: lim seq1 = lim seq
consider Nseq being V37() sequence of NAT such that
A3: seq1 = seq * Nseq by A1, VALUED_0:def_17;
A4: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.((seq1_._m)_-_(lim_seq)).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq1 . m) - (lim seq)).| < p )
assume 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
then consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
|.((seq . m) - (lim seq)).| < p by A2, COMSEQ_2:def_6;
take n = n1; ::_thesis: for m being Element of NAT st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((seq1 . m) - (lim seq)).| < p )
assume A6: n <= m ; ::_thesis: |.((seq1 . m) - (lim seq)).| < p
m <= Nseq . m by SEQM_3:14;
then A7: n <= Nseq . m by A6, XXREAL_0:2;
seq1 . m = seq . (Nseq . m) by A3, FUNCT_2:15;
hence |.((seq1 . m) - (lim seq)).| < p by A5, A7; ::_thesis: verum
end;
seq1 is convergent by A1, A2, Th17;
hence lim seq1 = lim seq by A4, COMSEQ_2:def_6; ::_thesis: verum
end;
theorem Th19: :: CFCONT_1:19
for seq, seq1 being Complex_Sequence st seq is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n holds
seq1 is convergent
proof
let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n implies seq1 is convergent )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n ; ::_thesis: seq1 is convergent
consider g1 being Element of COMPLEX such that
A3: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g1).| < p by A1, COMSEQ_2:def_5;
consider k being Element of NAT such that
A4: for n being Element of NAT st k <= n holds
seq1 . n = seq . n by A2;
take g = g1; :: according to COMSEQ_2:def_5 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= |.K65((seq1 . b3),g).| ) )
let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= |.K65((seq1 . b2),g).| ) )
assume 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= |.K65((seq1 . b2),g).| )
then consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
|.((seq . m) - g1).| < p by A3;
A6: now__::_thesis:_(_n1_<=_k_implies_ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.((seq1_._m)_-_g).|_<_p_)
assume A7: n1 <= k ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq1 . m) - g).| < p
take n = k; ::_thesis: for m being Element of NAT st n <= m holds
|.((seq1 . m) - g).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((seq1 . m) - g).| < p )
assume A8: n <= m ; ::_thesis: |.((seq1 . m) - g).| < p
then n1 <= m by A7, XXREAL_0:2;
then |.((seq . m) - g1).| < p by A5;
hence |.((seq1 . m) - g).| < p by A4, A8; ::_thesis: verum
end;
now__::_thesis:_(_k_<=_n1_implies_ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.((seq1_._m)_-_g).|_<_p_)
assume A9: k <= n1 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq1 . m) - g).| < p
take n = n1; ::_thesis: for m being Element of NAT st n <= m holds
|.((seq1 . m) - g).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((seq1 . m) - g).| < p )
assume A10: n <= m ; ::_thesis: |.((seq1 . m) - g).| < p
then seq1 . m = seq . m by A4, A9, XXREAL_0:2;
hence |.((seq1 . m) - g).| < p by A5, A10; ::_thesis: verum
end;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq1 . m) - g).| < p by A6; ::_thesis: verum
end;
theorem :: CFCONT_1:20
for seq, seq1 being Complex_Sequence st seq is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n holds
lim seq = lim seq1
proof
let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n implies lim seq = lim seq1 )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n ; ::_thesis: lim seq = lim seq1
consider k being Element of NAT such that
A3: for n being Element of NAT st k <= n holds
seq1 . n = seq . n by A2;
A4: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.((seq1_._m)_-_(lim_seq)).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq1 . m) - (lim seq)).| < p )
assume 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
then consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
|.((seq . m) - (lim seq)).| < p by A1, COMSEQ_2:def_6;
A6: now__::_thesis:_(_n1_<=_k_implies_ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.((seq1_._m)_-_(lim_seq)).|_<_p_)
assume A7: n1 <= k ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
take n = k; ::_thesis: for m being Element of NAT st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((seq1 . m) - (lim seq)).| < p )
assume A8: n <= m ; ::_thesis: |.((seq1 . m) - (lim seq)).| < p
then n1 <= m by A7, XXREAL_0:2;
then |.((seq . m) - (lim seq)).| < p by A5;
hence |.((seq1 . m) - (lim seq)).| < p by A3, A8; ::_thesis: verum
end;
now__::_thesis:_(_k_<=_n1_implies_ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.((seq1_._m)_-_(lim_seq)).|_<_p_)
assume A9: k <= n1 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
take n = n1; ::_thesis: for m being Element of NAT st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((seq1 . m) - (lim seq)).| < p )
assume A10: n <= m ; ::_thesis: |.((seq1 . m) - (lim seq)).| < p
then seq1 . m = seq . m by A3, A9, XXREAL_0:2;
hence |.((seq1 . m) - (lim seq)).| < p by A5, A10; ::_thesis: verum
end;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq1 . m) - (lim seq)).| < p by A6; ::_thesis: verum
end;
seq1 is convergent by A1, A2, Th19;
hence lim seq = lim seq1 by A4, COMSEQ_2:def_6; ::_thesis: verum
end;
theorem :: CFCONT_1:21
for k being Element of 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 Element of NAT st seq = seq1 ^\ k holds
seq1 is convergent
proof
let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k implies seq1 is convergent )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st seq = seq1 ^\ k ; ::_thesis: seq1 is convergent
consider k being Element of NAT such that
A3: seq = seq1 ^\ k by A2;
consider g1 being Element of COMPLEX such that
A4: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g1).| < p by A1, COMSEQ_2:def_5;
take g = g1; :: according to COMSEQ_2:def_5 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= |.K65((seq1 . b3),g).| ) )
let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= |.K65((seq1 . b2),g).| ) )
assume 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= |.K65((seq1 . b2),g).| )
then consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
|.((seq . m) - g1).| < p by A4;
take n = n1 + k; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= |.K65((seq1 . b1),g).| )
let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= |.K65((seq1 . m),g).| )
assume A6: n <= m ; ::_thesis: not p <= |.K65((seq1 . m),g).|
then consider l being Nat such that
A7: m = (n1 + k) + l by NAT_1:10;
reconsider l = l as Element of NAT by ORDINAL1:def_12;
m - k = ((n1 + l) + k) + (- k) by A7;
then consider m1 being Element of NAT such that
A8: m1 = m - k ;
now__::_thesis:_n1_<=_m1
assume not n1 <= m1 ; ::_thesis: contradiction
then m1 + k < n1 + k by XREAL_1:6;
hence contradiction by A6, A8; ::_thesis: verum
end;
then A9: |.((seq . m1) - g1).| < p by A5;
m1 + k = m by A8;
hence |.((seq1 . m) - g).| < p by A3, A9, NAT_1:def_3; ::_thesis: verum
end;
theorem :: CFCONT_1:23
for seq, seq1 being Complex_Sequence st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds
lim seq1 = lim seq
proof
let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k implies lim seq1 = lim seq )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st seq = seq1 ^\ k ; ::_thesis: lim seq1 = lim seq
consider k being Element of NAT such that
A3: seq = seq1 ^\ k by A2;
A4: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.((seq1_._m)_-_(lim_seq)).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq1 . m) - (lim seq)).| < p )
assume 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
then consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
|.((seq . m) - (lim seq)).| < p by A1, COMSEQ_2:def_6;
take n = n1 + k; ::_thesis: for m being Element of NAT st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((seq1 . m) - (lim seq)).| < p )
assume A6: n <= m ; ::_thesis: |.((seq1 . m) - (lim seq)).| < p
then consider l being Nat such that
A7: m = (n1 + k) + l by NAT_1:10;
reconsider l = l as Element of NAT by ORDINAL1:def_12;
m - k = ((n1 + l) + k) + (- k) by A7;
then consider m1 being Element of NAT such that
A8: m1 = m - k ;
now__::_thesis:_n1_<=_m1
assume not n1 <= m1 ; ::_thesis: contradiction
then m1 + k < n1 + k by XREAL_1:6;
hence contradiction by A6, A8; ::_thesis: verum
end;
then A9: |.((seq . m1) - (lim seq)).| < p by A5;
m1 + k = m by A8;
hence |.((seq1 . m) - (lim seq)).| < p by A3, A9, NAT_1:def_3; ::_thesis: verum
end;
seq1 is convergent by A1, A2, Th22;
hence lim seq1 = lim seq by A4, COMSEQ_2:def_6; ::_thesis: verum
end;
theorem Th24: :: CFCONT_1:24
for seq being Complex_Sequence st seq is convergent & lim seq <> 0 holds
ex k being Element of NAT st seq ^\ k is non-zero
proof
let seq be Complex_Sequence; ::_thesis: ( seq is convergent & lim seq <> 0 implies ex k being Element of NAT st seq ^\ k is non-zero )
assume that
A1: seq is convergent and
A2: lim seq <> 0 ; ::_thesis: ex k being Element of NAT st seq ^\ k is non-zero
consider n1 being Element of NAT such that
A3: for m being Element of NAT st n1 <= m holds
|.(lim seq).| / 2 < |.(seq . m).| by A1, A2, COMSEQ_2:33;
take k = n1; ::_thesis: seq ^\ k is non-zero
now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_^\_k)_._n_<>_0c
let n be Element of NAT ; ::_thesis: (seq ^\ k) . n <> 0c
0 <= n by NAT_1:2;
then 0 + k <= n + k by XREAL_1:7;
then |.(lim seq).| / 2 < |.(seq . (n + k)).| by A3;
then A4: |.(lim seq).| / 2 < |.((seq ^\ k) . n).| by NAT_1:def_3;
0 < |.(lim seq).| by A2, COMPLEX1:47;
then 0 / 2 < |.(lim seq).| / 2 by XREAL_1:74;
then 0 < |.((seq ^\ k) . n).| by A4, XXREAL_0:2;
hence (seq ^\ k) . n <> 0c by COMPLEX1:47; ::_thesis: verum
end;
hence seq ^\ k is non-zero by COMSEQ_1:4; ::_thesis: verum
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
let seq be Complex_Sequence; ::_thesis: ( seq is convergent & lim seq <> 0 implies ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is non-zero ) )
assume ( seq is convergent & lim seq <> 0 ) ; ::_thesis: ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is non-zero )
then consider k being Element of NAT such that
A1: seq ^\ k is non-zero by Th24;
take seq ^\ k ; ::_thesis: ( seq ^\ k is subsequence of seq & seq ^\ k is non-zero )
thus ( seq ^\ k is subsequence of seq & seq ^\ k is non-zero ) by A1; ::_thesis: verum
end;
theorem Th26: :: CFCONT_1:26
for seq being Complex_Sequence st seq is constant holds
seq is convergent
proof
let seq be Complex_Sequence; ::_thesis: ( seq is constant implies seq is convergent )
assume seq is constant ; ::_thesis: seq is convergent
then consider t being Element of COMPLEX such that
A1: for n being Nat holds seq . n = t by VALUED_0:def_18;
take g = t; :: according to COMSEQ_2:def_5 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= |.K65((seq . b3),g).| ) )
let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= |.K65((seq . b2),g).| ) )
assume A2: 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= |.K65((seq . b2),g).| )
take n = 0 ; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= |.K65((seq . b1),g).| )
let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= |.K65((seq . m),g).| )
assume n <= m ; ::_thesis: not p <= |.K65((seq . m),g).|
|.((seq . m) - g).| = |.(t - g).| by A1
.= 0 by COMPLEX1:44 ;
hence |.((seq . m) - g).| < p by A2; ::_thesis: verum
end;
theorem Th27: :: CFCONT_1:27
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 Element of NAT st seq . n = g ) ) holds
lim seq = g
proof
let g be Element of COMPLEX ; ::_thesis: for seq being Complex_Sequence st ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) holds
lim seq = g
let seq be Complex_Sequence; ::_thesis: ( ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) implies lim seq = g )
A1: now__::_thesis:_(_seq_is_constant_&_g_in_rng_seq_&_(_(_seq_is_constant_&_g_in_rng_seq_)_or_(_seq_is_constant_&_ex_n_being_Element_of_NAT_st_seq_._n_=_g_)_)_implies_lim_seq_=_g_)
assume that
A2: seq is constant and
A3: g in rng seq ; ::_thesis: ( ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) implies lim seq = g )
consider g1 being Element of COMPLEX such that
A4: rng seq = {g1} by A2, FUNCT_2:111;
consider g2 being Element of COMPLEX such that
A5: for n being Nat holds seq . n = g2 by A2, VALUED_0:def_18;
A6: g = g1 by A3, A4, TARSKI:def_1;
A7: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.((seq_._m)_-_g).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g).| < p )
assume A8: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g).| < p
take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds
|.((seq . m) - g).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((seq . m) - g).| < p )
assume n <= m ; ::_thesis: |.((seq . m) - g).| < p
m in NAT ;
then m in dom seq by COMSEQ_1:2;
then seq . m in rng seq by FUNCT_1:def_3;
then g2 in rng seq by A5;
then g2 = g by A4, A6, TARSKI:def_1;
then seq . m = g by A5;
hence |.((seq . m) - g).| < p by A8, COMPLEX1:44; ::_thesis: verum
end;
seq is convergent by A2, Th26;
hence ( ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) implies lim seq = g ) by A7, COMSEQ_2:def_6; ::_thesis: verum
end;
A9: now__::_thesis:_(_seq_is_constant_&_ex_n_being_Element_of_NAT_st_seq_._n_=_g_&_(_(_seq_is_constant_&_g_in_rng_seq_)_or_(_seq_is_constant_&_ex_n_being_Element_of_NAT_st_seq_._n_=_g_)_)_implies_lim_seq_=_g_)
assume that
seq is constant and
A10: ex n being Element of NAT st seq . n = g ; ::_thesis: ( ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) implies lim seq = g )
consider n being Element of NAT such that
A11: seq . n = g by A10;
n in NAT ;
then n in dom seq by COMSEQ_1:2;
hence ( ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) implies lim seq = g ) by A1, A11, FUNCT_1:def_3; ::_thesis: verum
end;
assume ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Element of NAT st seq . n = g ) ) ; ::_thesis: lim seq = g
hence lim seq = g by A1, A9; ::_thesis: verum
end;
theorem :: CFCONT_1:28
for seq being Complex_Sequence st seq is constant holds
for n being Element of 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
let seq be Complex_Sequence; ::_thesis: ( seq is convergent & lim seq <> 0 implies for seq1 being Complex_Sequence st seq1 is subsequence of seq & seq1 is non-zero holds
lim (seq1 ") = (lim seq) " )
assume that
A1: seq is convergent and
A2: lim seq <> 0 ; ::_thesis: for seq1 being Complex_Sequence st seq1 is subsequence of seq & seq1 is non-zero holds
lim (seq1 ") = (lim seq) "
let seq1 be Complex_Sequence; ::_thesis: ( seq1 is subsequence of seq & seq1 is non-zero implies lim (seq1 ") = (lim seq) " )
assume that
A3: seq1 is subsequence of seq and
A4: seq1 is non-zero ; ::_thesis: lim (seq1 ") = (lim seq) "
lim seq1 = lim seq by A1, A3, Th18;
hence lim (seq1 ") = (lim seq) " by A1, A2, A3, A4, Th17, COMSEQ_2:35; ::_thesis: verum
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
let seq, seq1 be Complex_Sequence; ::_thesis: ( 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) ) )
assume that
A1: seq is constant and
A2: seq1 is convergent ; ::_thesis: ( 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) )
A3: seq is convergent by A1, Th26;
hence lim (seq + seq1) = (lim seq) + (lim seq1) by A2, COMSEQ_2:14
.= (seq . 0) + (lim seq1) by A1, Th27 ;
::_thesis: ( lim (seq - seq1) = (seq . 0) - (lim seq1) & lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) )
thus lim (seq - seq1) = (lim seq) - (lim seq1) by A2, A3, COMSEQ_2:26
.= (seq . 0) - (lim seq1) by A1, Th27 ; ::_thesis: ( lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) )
thus lim (seq1 - seq) = (lim seq1) - (lim seq) by A2, A3, COMSEQ_2:26
.= (lim seq1) - (seq . 0) by A1, Th27 ; ::_thesis: lim (seq (#) seq1) = (seq . 0) * (lim seq1)
thus lim (seq (#) seq1) = (lim seq) * (lim seq1) by A2, A3, COMSEQ_2:30
.= (seq . 0) * (lim seq1) by A1, Th27 ; ::_thesis: verum
end;
scheme :: CFCONT_1:sch 1
CompSeqChoice{ P1[ set , set ] } :
ex s1 being Complex_Sequence st
for n being Element of NAT holds P1[n,s1 . n]
provided
A1: for n being Element of NAT ex g being Element of COMPLEX st P1[n,g]
proof
A2: for t being Element of NAT ex ff being Element of COMPLEX st P1[t,ff] by A1;
consider f being Function of NAT,COMPLEX such that
A3: for t being Element of NAT holds P1[t,f . t] from FUNCT_2:sch_3(A2);
reconsider s = f as Complex_Sequence ;
take s ; ::_thesis: for n being Element of NAT holds P1[n,s . n]
let n be Element of NAT ; ::_thesis: P1[n,s . n]
thus P1[n,s . n] by A3; ::_thesis: verum
end;
begin
theorem :: CFCONT_1:31
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 Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )
proof
let x0 be Element of COMPLEX ; ::_thesis: 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 Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( 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 Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )
thus ( f is_continuous_in x0 implies ( x0 in dom f & ( for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ) by Def1; ::_thesis: ( x0 in dom f & ( for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) implies f is_continuous_in x0 )
assume that
A1: x0 in dom f and
A2: for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ; ::_thesis: f is_continuous_in x0
thus x0 in dom f by A1; :: according to CFCONT_1:def_1 ::_thesis: 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) )
let s2 be Complex_Sequence; ::_thesis: ( rng s2 c= dom f & s2 is convergent & lim s2 = x0 implies ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) )
assume that
A3: rng s2 c= dom f and
A4: ( s2 is convergent & lim s2 = x0 ) ; ::_thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )
now__::_thesis:_(_f_/*_s2_is_convergent_&_f_/._x0_=_lim_(f_/*_s2)_)
percases ( ex n being Element of NAT st
for m being Element of NAT st n <= m holds
s2 . m = x0 or for n being Element of NAT ex m being Element of NAT st
( n <= m & s2 . m <> x0 ) ) ;
suppose ex n being Element of NAT st
for m being Element of NAT st n <= m holds
s2 . m = x0 ; ::_thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )
then consider N being Element of NAT such that
A5: for m being Element of NAT st N <= m holds
s2 . m = x0 ;
A6: for n being Element of NAT holds (s2 ^\ N) . n = x0
proof
let n be Element of NAT ; ::_thesis: (s2 ^\ N) . n = x0
s2 . (n + N) = x0 by A5, NAT_1:12;
hence (s2 ^\ N) . n = x0 by NAT_1:def_3; ::_thesis: verum
end;
A7: f /* (s2 ^\ N) = (f /* s2) ^\ N by A3, VALUED_0:27;
A8: rng (s2 ^\ N) c= rng s2 by VALUED_0:21;
A9: now__::_thesis:_for_p_being_Real_st_p_>_0_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.(((f_/*_(s2_^\_N))_._m)_-_(f_/._x0)).|_<_p
let p be Real; ::_thesis: ( p > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p )
assume A10: p > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p
take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds
|.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p )
assume n <= m ; ::_thesis: |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p
|.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| = |.((f /. ((s2 ^\ N) . m)) - (f /. x0)).| by A3, A8, FUNCT_2:109, XBOOLE_1:1
.= |.((f /. x0) - (f /. x0)).| by A6
.= 0 by COMPLEX1:44 ;
hence |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p by A10; ::_thesis: verum
end;
then A11: f /* (s2 ^\ N) is convergent by COMSEQ_2:def_5;
then f /. x0 = lim ((f /* s2) ^\ N) by A9, A7, COMSEQ_2:def_6;
hence ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) by A11, A7, Th18, Th22; ::_thesis: verum
end;
supposeA12: for n being Element of NAT ex m being Element of NAT st
( n <= m & s2 . m <> x0 ) ; ::_thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )
defpred S1[ set , set ] means for n, m being Element of NAT st $1 = n & $2 = m holds
( n < m & s2 . m <> x0 & ( for k being Element of NAT st n < k & s2 . k <> x0 holds
m <= k ) );
defpred S2[ set , set , set ] means S1[$2,$3];
defpred S3[ set ] means s2 . $1 <> x0;
ex m1 being Element of NAT st
( 0 <= m1 & s2 . m1 <> x0 ) by A12;
then A13: ex m being Nat st S3[m] ;
consider M being Nat such that
A14: ( S3[M] & ( for n being Nat st S3[n] holds
M <= n ) ) from NAT_1:sch_5(A13);
reconsider M9 = M as Element of NAT by ORDINAL1:def_12;
A15: now__::_thesis:_for_n_being_Element_of_NAT_ex_m_being_Element_of_NAT_st_
(_n_<_m_&_s2_._m_<>_x0_)
let n be Element of NAT ; ::_thesis: ex m being Element of NAT st
( n < m & s2 . m <> x0 )
consider m being Element of NAT such that
A16: ( n + 1 <= m & s2 . m <> x0 ) by A12;
take m = m; ::_thesis: ( n < m & s2 . m <> x0 )
thus ( n < m & s2 . m <> x0 ) by A16, NAT_1:13; ::_thesis: verum
end;
A17: for n, x being Element of NAT ex y being Element of NAT st S2[n,x,y]
proof
let n, x be Element of NAT ; ::_thesis: ex y being Element of NAT st S2[n,x,y]
defpred S4[ Nat] means ( x < $1 & s2 . $1 <> x0 );
ex m being Element of NAT st S4[m] by A15;
then A18: ex m being Nat st S4[m] ;
consider l being Nat such that
A19: ( S4[l] & ( for k being Nat st S4[k] holds
l <= k ) ) from NAT_1:sch_5(A18);
take l ; ::_thesis: ( l is Element of REAL & l is Element of NAT & S2[n,x,l] )
l in NAT by ORDINAL1:def_12;
hence ( l is Element of REAL & l is Element of NAT & S2[n,x,l] ) by A19; ::_thesis: verum
end;
consider F being Function of NAT,NAT such that
A20: ( F . 0 = M9 & ( for n being Element of NAT holds S2[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A17);
A21: for n being Element of NAT holds F . n is real ;
A22: rng F c= NAT ;
A23: dom F = NAT by FUNCT_2:def_1;
then reconsider F = F as Real_Sequence by A21, SEQ_1:2;
A24: now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_is_Element_of_NAT
let n be Element of NAT ; ::_thesis: F . n is Element of NAT
F . n in rng F by A23, FUNCT_1:def_3;
hence F . n is Element of NAT by A22; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_<_F_._(n_+_1)
let n be Element of NAT ; ::_thesis: F . n < F . (n + 1)
( F . n is Element of NAT & F . (n + 1) is Element of NAT ) by A24;
hence F . n < F . (n + 1) by A20; ::_thesis: verum
end;
then reconsider F = F as V37() sequence of NAT by SEQM_3:def_6;
A25: s2 * F is subsequence of s2 by VALUED_0:def_17;
then A26: ( s2 * F is convergent & lim (s2 * F) = x0 ) by A4, Th17, Th18;
A27: for n being Element of NAT st s2 . n <> x0 holds
ex m being Element of NAT st F . m = n
proof
defpred S4[ set ] means ( s2 . $1 <> x0 & ( for m being Element of NAT holds F . m <> $1 ) );
assume ex n being Element of NAT st S4[n] ; ::_thesis: contradiction
then A28: ex n being Nat st S4[n] ;
consider M1 being Nat such that
A29: ( S4[M1] & ( for n being Nat st S4[n] holds
M1 <= n ) ) from NAT_1:sch_5(A28);
defpred S5[ Nat] means ( $1 < M1 & s2 . $1 <> x0 & ex m being Element of NAT st F . m = $1 );
A30: ex n being Nat st S5[n]
proof
take M ; ::_thesis: S5[M]
( M <= M1 & M <> M1 ) by A14, A20, A29;
hence M < M1 by XXREAL_0:1; ::_thesis: ( s2 . M <> x0 & ex m being Element of NAT st F . m = M )
thus s2 . M <> x0 by A14; ::_thesis: ex m being Element of NAT st F . m = M
take 0 ; ::_thesis: F . 0 = M
thus F . 0 = M by A20; ::_thesis: verum
end;
A31: for n being Nat st S5[n] holds
n <= M1 ;
consider MX being Nat such that
A32: ( S5[MX] & ( for n being Nat st S5[n] holds
n <= MX ) ) from NAT_1:sch_6(A31, A30);
A33: for k being Element of NAT st MX < k & k < M1 holds
s2 . k = x0
proof
given k being Element of NAT such that A34: MX < k and
A35: ( k < M1 & s2 . k <> x0 ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( ex m being Element of NAT st F . m = k or for m being Element of NAT holds F . m <> k ) ;
suppose ex m being Element of NAT st F . m = k ; ::_thesis: contradiction
hence contradiction by A32, A34, A35; ::_thesis: verum
end;
suppose for m being Element of NAT holds F . m <> k ; ::_thesis: contradiction
hence contradiction by A29, A35; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
consider m being Element of NAT such that
A36: F . m = MX by A32;
A37: ( MX < F . (m + 1) & s2 . (F . (m + 1)) <> x0 ) by A20, A36;
M1 in NAT by ORDINAL1:def_12;
then A38: F . (m + 1) <= M1 by A20, A29, A32, A36;
now__::_thesis:_not_F_._(m_+_1)_<>_M1
assume F . (m + 1) <> M1 ; ::_thesis: contradiction
then F . (m + 1) < M1 by A38, XXREAL_0:1;
hence contradiction by A33, A37; ::_thesis: verum
end;
hence contradiction by A29; ::_thesis: verum
end;
defpred S4[ Element of NAT ] means (s2 * F) . $1 <> x0;
A39: for k being Element of NAT st S4[k] holds
S4[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S4[k] implies S4[k + 1] )
assume (s2 * F) . k <> x0 ; ::_thesis: S4[k + 1]
S1[F . k,F . (k + 1)] by A20;
then s2 . (F . (k + 1)) <> x0 ;
hence S4[k + 1] by FUNCT_2:15; ::_thesis: verum
end;
A40: S4[ 0 ] by A14, A20, FUNCT_2:15;
A41: for n being Element of NAT holds S4[n] from NAT_1:sch_1(A40, A39);
A42: rng (s2 * F) c= rng s2 by A25, VALUED_0:21;
then rng (s2 * F) c= dom f by A3, XBOOLE_1:1;
then A43: ( f /* (s2 * F) is convergent & f /. x0 = lim (f /* (s2 * F)) ) by A2, A41, A26;
A44: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
|.(((f_/*_s2)_._m)_-_(f_/._x0)).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((f /* s2) . m) - (f /. x0)).| < p )
assume A45: 0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((f /* s2) . m) - (f /. x0)).| < p
then consider n being Element of NAT such that
A46: for m being Element of NAT st n <= m holds
|.(((f /* (s2 * F)) . m) - (f /. x0)).| < p by A43, COMSEQ_2:def_6;
take k = F . n; ::_thesis: for m being Element of NAT st k <= m holds
|.(((f /* s2) . m) - (f /. x0)).| < p
let m be Element of NAT ; ::_thesis: ( k <= m implies |.(((f /* s2) . m) - (f /. x0)).| < p )
assume A47: k <= m ; ::_thesis: |.(((f /* s2) . m) - (f /. x0)).| < p
now__::_thesis:_|.(((f_/*_s2)_._m)_-_(f_/._x0)).|_<_p
percases ( s2 . m = x0 or s2 . m <> x0 ) ;
suppose s2 . m = x0 ; ::_thesis: |.(((f /* s2) . m) - (f /. x0)).| < p
then |.(((f /* s2) . m) - (f /. x0)).| = |.((f /. x0) - (f /. x0)).| by A3, FUNCT_2:109
.= 0 by COMPLEX1:44 ;
hence |.(((f /* s2) . m) - (f /. x0)).| < p by A45; ::_thesis: verum
end;
suppose s2 . m <> x0 ; ::_thesis: |.(((f /* s2) . m) - (f /. x0)).| < p
then consider l being Element of NAT such that
A48: m = F . l by A27;
n <= l by A47, A48, SEQM_3:1;
then |.(((f /* (s2 * F)) . l) - (f /. x0)).| < p by A46;
then |.((f /. ((s2 * F) . l)) - (f /. x0)).| < p by A3, A42, FUNCT_2:109, XBOOLE_1:1;
then |.((f /. (s2 . m)) - (f /. x0)).| < p by A48, FUNCT_2:15;
hence |.(((f /* s2) . m) - (f /. x0)).| < p by A3, FUNCT_2:109; ::_thesis: verum
end;
end;
end;
hence |.(((f /* s2) . m) - (f /. x0)).| < p ; ::_thesis: verum
end;
hence f /* s2 is convergent by COMSEQ_2:def_5; ::_thesis: f /. x0 = lim (f /* s2)
hence f /. x0 = lim (f /* s2) by A44, COMSEQ_2:def_6; ::_thesis: verum
end;
end;
end;
hence ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) ; ::_thesis: verum
end;
theorem Th32: :: CFCONT_1:32
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
let x0 be Element of COMPLEX ; ::_thesis: 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 ) ) ) ) )
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( 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 ) ) ) ) )
thus ( f is_continuous_in x0 implies ( 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 ) ) ) ) ) ::_thesis: ( 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 ) ) ) implies f is_continuous_in x0 )
proof
assume A1: f is_continuous_in x0 ; ::_thesis: ( 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 ) ) ) )
hence x0 in dom f by Def1; ::_thesis: 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 ) )
given r being Real such that A2: 0 < r and
A3: for s being Real holds
( not 0 < s or ex x1 being Element of COMPLEX st
( x1 in dom f & |.(x1 - x0).| < s & not |.((f /. x1) - (f /. x0)).| < r ) ) ; ::_thesis: contradiction
defpred S1[ Element of NAT , Element of COMPLEX ] means ( $2 in dom f & |.($2 - x0).| < 1 / ($1 + 1) & not |.((f /. $2) - (f /. x0)).| < r );
A4: for n being Element of NAT ex g being Element of COMPLEX st S1[n,g]
proof
let n be Element of NAT ; ::_thesis: ex g being Element of COMPLEX st S1[n,g]
0 < n + 1 by NAT_1:3;
then 0 < (n + 1) " by XREAL_1:122;
then 0 < 1 / (n + 1) by XCMPLX_1:215;
then consider g being Element of COMPLEX such that
A5: ( g in dom f & |.(g - x0).| < 1 / (n + 1) & not |.((f /. g) - (f /. x0)).| < r ) by A3;
take g ; ::_thesis: S1[n,g]
thus S1[n,g] by A5; ::_thesis: verum
end;
consider s1 being Complex_Sequence such that
A6: for n being Element of NAT holds S1[n,s1 . n] from CFCONT_1:sch_1(A4);
A7: rng s1 c= dom f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng s1 or x in dom f )
assume x in rng s1 ; ::_thesis: x in dom f
then ex n being Element of NAT st x = s1 . n by FUNCT_2:113;
hence x in dom f by A6; ::_thesis: verum
end;
A8: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_|.(((f_/*_s1)_._n)_-_(f_/._x0)).|_<_r
let n be Element of NAT ; ::_thesis: not |.(((f /* s1) . n) - (f /. x0)).| < r
not |.((f /. (s1 . n)) - (f /. x0)).| < r by A6;
hence not |.(((f /* s1) . n) - (f /. x0)).| < r by A7, FUNCT_2:109; ::_thesis: verum
end;
A9: now__::_thesis:_for_s_being_Real_st_0_<_s_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
|.((s1_._m)_-_x0).|_<_s
let s be Real; ::_thesis: ( 0 < s implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((s1 . m) - x0).| < s )
consider n being Element of NAT such that
A10: s " < n by SEQ_4:3;
assume 0 < s ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((s1 . m) - x0).| < s
then A11: 0 < s " by XREAL_1:122;
(s ") + 0 < n + 1 by A10, XREAL_1:8;
then 1 / (n + 1) < 1 / (s ") by A11, XREAL_1:76;
then A12: 1 / (n + 1) < s by XCMPLX_1:216;
take k = n; ::_thesis: for m being Element of NAT st k <= m holds
|.((s1 . m) - x0).| < s
let m be Element of NAT ; ::_thesis: ( k <= m implies |.((s1 . m) - x0).| < s )
assume k <= m ; ::_thesis: |.((s1 . m) - x0).| < s
then k + 1 <= m + 1 by XREAL_1:6;
then 1 / (m + 1) <= 1 / (k + 1) by NAT_1:3, XREAL_1:118;
then 1 / (m + 1) < s by A12, XXREAL_0:2;
hence |.((s1 . m) - x0).| < s by A6, XXREAL_0:2; ::_thesis: verum
end;
then A13: s1 is convergent by COMSEQ_2:def_5;
then lim s1 = x0 by A9, COMSEQ_2:def_6;
then ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A1, A7, A13, Def1;
then consider n being Element of NAT such that
A14: for m being Element of NAT st n <= m holds
|.(((f /* s1) . m) - (f /. x0)).| < r by A2, COMSEQ_2:def_6;
|.(((f /* s1) . n) - (f /. x0)).| < r by A14;
hence contradiction by A8; ::_thesis: verum
end;
assume that
A15: x0 in dom f and
A16: 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 ) ) ; ::_thesis: f is_continuous_in x0
now__::_thesis:_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)_)
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 implies ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) )
assume that
A17: rng s1 c= dom f and
A18: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) )
A19: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
|.(((f_/*_s1)_._m)_-_(f_/._x0)).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((f /* s1) . m) - (f /. x0)).| < p )
assume 0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((f /* s1) . m) - (f /. x0)).| < p
then consider s being Real such that
A20: 0 < s and
A21: for x1 being Element of COMPLEX st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < p by A16;
consider n being Element of NAT such that
A22: for m being Element of NAT st n <= m holds
|.((s1 . m) - x0).| < s by A18, A20, COMSEQ_2:def_6;
take k = n; ::_thesis: for m being Element of NAT st k <= m holds
|.(((f /* s1) . m) - (f /. x0)).| < p
let m be Element of NAT ; ::_thesis: ( k <= m implies |.(((f /* s1) . m) - (f /. x0)).| < p )
assume k <= m ; ::_thesis: |.(((f /* s1) . m) - (f /. x0)).| < p
then ( s1 . m in rng s1 & |.((s1 . m) - x0).| < s ) by A22, VALUED_0:28;
then |.((f /. (s1 . m)) - (f /. x0)).| < p by A17, A21;
hence |.(((f /* s1) . m) - (f /. x0)).| < p by A17, FUNCT_2:109; ::_thesis: verum
end;
then f /* s1 is convergent by COMSEQ_2:def_5;
hence ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A19, COMSEQ_2:def_6; ::_thesis: verum
end;
hence f is_continuous_in x0 by A15, Def1; ::_thesis: verum
end;
theorem Th33: :: CFCONT_1:33
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
let x0 be Element of COMPLEX ; ::_thesis: 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 )
let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( 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 ) )
assume that
A1: f1 is_continuous_in x0 and
A2: f2 is_continuous_in x0 ; ::_thesis: ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 )
A3: ( x0 in dom f1 & x0 in dom f2 ) by A1, A2, Def1;
now__::_thesis:_(_x0_in_dom_(f1_+_f2)_&_(_for_s1_being_Complex_Sequence_st_rng_s1_c=_dom_(f1_+_f2)_&_s1_is_convergent_&_lim_s1_=_x0_holds_
(_(f1_+_f2)_/*_s1_is_convergent_&_(f1_+_f2)_/._x0_=_lim_((f1_+_f2)_/*_s1)_)_)_)
x0 in (dom f1) /\ (dom f2) by A3, XBOOLE_0:def_4;
hence A4: x0 in dom (f1 + f2) by VALUED_1:def_1; ::_thesis: for s1 being Complex_Sequence st rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 = x0 holds
( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) )
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 = x0 implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) ) )
assume that
A5: rng s1 c= dom (f1 + f2) and
A6: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) )
A7: rng s1 c= (dom f1) /\ (dom f2) by A5, VALUED_1:def_1;
dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def_1;
then dom (f1 + f2) c= dom f2 by XBOOLE_1:17;
then A8: rng s1 c= dom f2 by A5, XBOOLE_1:1;
then A9: f2 /* s1 is convergent by A2, A6, Def1;
dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def_1;
then dom (f1 + f2) c= dom f1 by XBOOLE_1:17;
then A10: rng s1 c= dom f1 by A5, XBOOLE_1:1;
then A11: f1 /* s1 is convergent by A1, A6, Def1;
then (f1 /* s1) + (f2 /* s1) is convergent by A9;
hence (f1 + f2) /* s1 is convergent by A7, Th7; ::_thesis: (f1 + f2) /. x0 = lim ((f1 + f2) /* s1)
A12: f1 /. x0 = lim (f1 /* s1) by A1, A6, A10, Def1;
A13: f2 /. x0 = lim (f2 /* s1) by A2, A6, A8, Def1;
thus (f1 + f2) /. x0 = (f1 /. x0) + (f2 /. x0) by A4, CFUNCT_1:1
.= lim ((f1 /* s1) + (f2 /* s1)) by A11, A12, A9, A13, COMSEQ_2:14
.= lim ((f1 + f2) /* s1) by A7, Th7 ; ::_thesis: verum
end;
hence f1 + f2 is_continuous_in x0 by Def1; ::_thesis: ( f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 )
now__::_thesis:_(_x0_in_dom_(f1_-_f2)_&_(_for_s1_being_Complex_Sequence_st_rng_s1_c=_dom_(f1_-_f2)_&_s1_is_convergent_&_lim_s1_=_x0_holds_
(_(f1_-_f2)_/*_s1_is_convergent_&_(f1_-_f2)_/._x0_=_lim_((f1_-_f2)_/*_s1)_)_)_)
x0 in (dom f1) /\ (dom f2) by A3, XBOOLE_0:def_4;
hence A14: x0 in dom (f1 - f2) by CFUNCT_1:2; ::_thesis: for s1 being Complex_Sequence st rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 = x0 holds
( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) )
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 = x0 implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) ) )
assume that
A15: rng s1 c= dom (f1 - f2) and
A16: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) )
A17: rng s1 c= (dom f1) /\ (dom f2) by A15, CFUNCT_1:2;
dom (f1 - f2) = (dom f1) /\ (dom f2) by CFUNCT_1:2;
then dom (f1 - f2) c= dom f2 by XBOOLE_1:17;
then A18: rng s1 c= dom f2 by A15, XBOOLE_1:1;
then A19: f2 /* s1 is convergent by A2, A16, Def1;
dom (f1 - f2) = (dom f1) /\ (dom f2) by CFUNCT_1:2;
then dom (f1 - f2) c= dom f1 by XBOOLE_1:17;
then A20: rng s1 c= dom f1 by A15, XBOOLE_1:1;
then A21: f1 /* s1 is convergent by A1, A16, Def1;
then (f1 /* s1) - (f2 /* s1) is convergent by A19;
hence (f1 - f2) /* s1 is convergent by A17, Th7; ::_thesis: (f1 - f2) /. x0 = lim ((f1 - f2) /* s1)
A22: f1 /. x0 = lim (f1 /* s1) by A1, A16, A20, Def1;
A23: f2 /. x0 = lim (f2 /* s1) by A2, A16, A18, Def1;
thus (f1 - f2) /. x0 = (f1 /. x0) - (f2 /. x0) by A14, CFUNCT_1:2
.= lim ((f1 /* s1) - (f2 /* s1)) by A21, A22, A19, A23, COMSEQ_2:26
.= lim ((f1 - f2) /* s1) by A17, Th7 ; ::_thesis: verum
end;
hence f1 - f2 is_continuous_in x0 by Def1; ::_thesis: f1 (#) f2 is_continuous_in x0
x0 in (dom f1) /\ (dom f2) by A3, XBOOLE_0:def_4;
hence A24: x0 in dom (f1 (#) f2) by VALUED_1:def_4; :: according to CFCONT_1:def_1 ::_thesis: for s1 being Complex_Sequence st rng s1 c= dom (f1 (#) f2) & s1 is convergent & lim s1 = x0 holds
( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. x0 = lim ((f1 (#) f2) /* s1) )
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom (f1 (#) f2) & s1 is convergent & lim s1 = x0 implies ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. x0 = lim ((f1 (#) f2) /* s1) ) )
assume that
A25: rng s1 c= dom (f1 (#) f2) and
A26: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. x0 = lim ((f1 (#) f2) /* s1) )
dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def_4;
then dom (f1 (#) f2) c= dom f2 by XBOOLE_1:17;
then A27: rng s1 c= dom f2 by A25, XBOOLE_1:1;
then A28: f2 /* s1 is convergent by A2, A26, Def1;
A29: rng s1 c= (dom f1) /\ (dom f2) by A25, VALUED_1:def_4;
dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def_4;
then dom (f1 (#) f2) c= dom f1 by XBOOLE_1:17;
then A30: rng s1 c= dom f1 by A25, XBOOLE_1:1;
then A31: f1 /* s1 is convergent by A1, A26, Def1;
then (f1 /* s1) (#) (f2 /* s1) is convergent by A28;
hence (f1 (#) f2) /* s1 is convergent by A29, Th7; ::_thesis: (f1 (#) f2) /. x0 = lim ((f1 (#) f2) /* s1)
A32: f1 /. x0 = lim (f1 /* s1) by A1, A26, A30, Def1;
A33: f2 /. x0 = lim (f2 /* s1) by A2, A26, A27, Def1;
thus (f1 (#) f2) /. x0 = (f1 /. x0) * (f2 /. x0) by A24, CFUNCT_1:3
.= lim ((f1 /* s1) (#) (f2 /* s1)) by A31, A32, A28, A33, COMSEQ_2:30
.= lim ((f1 (#) f2) /* s1) by A29, Th7 ; ::_thesis: verum
end;
theorem Th34: :: CFCONT_1:34
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
let x0, g be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_in x0 holds
g (#) f is_continuous_in x0
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_in x0 implies g (#) f is_continuous_in x0 )
assume A1: f is_continuous_in x0 ; ::_thesis: g (#) f is_continuous_in x0
then x0 in dom f by Def1;
hence A2: x0 in dom (g (#) f) by VALUED_1:def_5; :: according to CFCONT_1:def_1 ::_thesis: for s1 being Complex_Sequence st rng s1 c= dom (g (#) f) & s1 is convergent & lim s1 = x0 holds
( (g (#) f) /* s1 is convergent & (g (#) f) /. x0 = lim ((g (#) f) /* s1) )
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom (g (#) f) & s1 is convergent & lim s1 = x0 implies ( (g (#) f) /* s1 is convergent & (g (#) f) /. x0 = lim ((g (#) f) /* s1) ) )
assume that
A3: rng s1 c= dom (g (#) f) and
A4: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (g (#) f) /* s1 is convergent & (g (#) f) /. x0 = lim ((g (#) f) /* s1) )
A5: rng s1 c= dom f by A3, VALUED_1:def_5;
then A6: f /. x0 = lim (f /* s1) by A1, A4, Def1;
A7: f /* s1 is convergent by A1, A4, A5, Def1;
then g (#) (f /* s1) is convergent ;
hence (g (#) f) /* s1 is convergent by A5, Th8; ::_thesis: (g (#) f) /. x0 = lim ((g (#) f) /* s1)
thus (g (#) f) /. x0 = g * (f /. x0) by A2, CFUNCT_1:4
.= lim (g (#) (f /* s1)) by A7, A6, COMSEQ_2:18
.= lim ((g (#) f) /* s1) by A5, Th8 ; ::_thesis: verum
end;
theorem :: CFCONT_1:35
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
let x0 be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_in x0 holds
- f is_continuous_in x0
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_in x0 implies - f is_continuous_in x0 )
A1: - f = (- 1r) (#) f by CFUNCT_1:31;
assume f is_continuous_in x0 ; ::_thesis: - f is_continuous_in x0
hence - f is_continuous_in x0 by A1, Th34; ::_thesis: verum
end;
theorem Th36: :: CFCONT_1:36
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
let x0 be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_in x0 & f /. x0 <> 0 holds
f ^ is_continuous_in x0
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_in x0 & f /. x0 <> 0 implies f ^ is_continuous_in x0 )
assume that
A1: f is_continuous_in x0 and
A2: f /. x0 <> 0 ; ::_thesis: f ^ is_continuous_in x0
not f /. x0 in {0c} by A2, TARSKI:def_1;
then A3: not x0 in f " {0c} by PARTFUN2:26;
x0 in dom f by A1, Def1;
then x0 in (dom f) \ (f " {0c}) by A3, XBOOLE_0:def_5;
hence A4: x0 in dom (f ^) by CFUNCT_1:def_2; :: according to CFCONT_1:def_1 ::_thesis: 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) )
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom (f ^) & s1 is convergent & lim s1 = x0 implies ( (f ^) /* s1 is convergent & (f ^) /. x0 = lim ((f ^) /* s1) ) )
assume that
A5: rng s1 c= dom (f ^) and
A6: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f ^) /* s1 is convergent & (f ^) /. x0 = lim ((f ^) /* s1) )
( (dom f) \ (f " {0c}) c= dom f & rng s1 c= (dom f) \ (f " {0c}) ) by A5, CFUNCT_1:def_2, XBOOLE_1:36;
then rng s1 c= dom f by XBOOLE_1:1;
then A7: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A1, A6, Def1;
f /* s1 is non-zero by A5, Th10;
then (f /* s1) " is convergent by A2, A7, COMSEQ_2:34;
hence (f ^) /* s1 is convergent by A5, Th11; ::_thesis: (f ^) /. x0 = lim ((f ^) /* s1)
thus (f ^) /. x0 = (f /. x0) " by A4, CFUNCT_1:def_2
.= lim ((f /* s1) ") by A2, A5, A7, Th10, COMSEQ_2:35
.= lim ((f ^) /* s1) by A5, Th11 ; ::_thesis: verum
end;
theorem :: CFCONT_1:37
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
let x0 be Element of COMPLEX ; ::_thesis: 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
let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f1 is_continuous_in x0 & f1 /. x0 <> 0 & f2 is_continuous_in x0 implies f2 / f1 is_continuous_in x0 )
assume that
A1: ( f1 is_continuous_in x0 & f1 /. x0 <> 0 ) and
A2: f2 is_continuous_in x0 ; ::_thesis: f2 / f1 is_continuous_in x0
f1 ^ is_continuous_in x0 by A1, Th36;
then f2 (#) (f1 ^) is_continuous_in x0 by A2, Th33;
hence f2 / f1 is_continuous_in x0 by CFUNCT_1:39; ::_thesis: verum
end;
definition
let f be PartFunc of COMPLEX,COMPLEX;
let X be set ;
predf is_continuous_on X means :Def2: :: CFCONT_1:def 2
( X c= dom f & ( for x0 being Element of COMPLEX st x0 in X holds
f | X is_continuous_in x0 ) );
end;
:: deftheorem Def2 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 Element of 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
let X be set ; ::_thesis: 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) ) ) ) )
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( 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) ) ) ) )
thus ( f is_continuous_on X implies ( 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) ) ) ) ) ::_thesis: ( 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) ) ) implies f is_continuous_on X )
proof
assume A1: f is_continuous_on X ; ::_thesis: ( 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) ) ) )
then A2: X c= dom f by Def2;
now__::_thesis:_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)_)
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) )
assume that
A3: rng s1 c= X and
A4: s1 is convergent and
A5: lim s1 in X ; ::_thesis: ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) )
A6: f | X is_continuous_in lim s1 by A1, A5, Def2;
A7: dom (f | X) = (dom f) /\ X by RELAT_1:61
.= X by A2, XBOOLE_1:28 ;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((f_|_X)_/*_s1)_._n_=_(f_/*_s1)_._n
let n be Element of NAT ; ::_thesis: ((f | X) /* s1) . n = (f /* s1) . n
A8: s1 . n in rng s1 by VALUED_0:28;
thus ((f | X) /* s1) . n = (f | X) /. (s1 . n) by A3, A7, FUNCT_2:109
.= f /. (s1 . n) by A3, A7, A8, PARTFUN2:15
.= (f /* s1) . n by A2, A3, FUNCT_2:109, XBOOLE_1:1 ; ::_thesis: verum
end;
then A9: (f | X) /* s1 = f /* s1 by FUNCT_2:63;
f /. (lim s1) = (f | X) /. (lim s1) by A5, A7, PARTFUN2:15
.= lim (f /* s1) by A3, A4, A7, A6, A9, Def1 ;
hence ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) by A3, A4, A7, A6, A9, Def1; ::_thesis: verum
end;
hence ( 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) ) ) ) by A1, Def2; ::_thesis: verum
end;
assume that
A10: X c= dom f and
A11: 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) ) ; ::_thesis: f is_continuous_on X
now__::_thesis:_for_x1_being_Element_of_COMPLEX_st_x1_in_X_holds_
f_|_X_is_continuous_in_x1
A12: dom (f | X) = (dom f) /\ X by RELAT_1:61
.= X by A10, XBOOLE_1:28 ;
let x1 be Element of COMPLEX ; ::_thesis: ( x1 in X implies f | X is_continuous_in x1 )
assume A13: x1 in X ; ::_thesis: f | X is_continuous_in x1
now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_dom_(f_|_X)_&_s1_is_convergent_&_lim_s1_=_x1_holds_
(_(f_|_X)_/*_s1_is_convergent_&_(f_|_X)_/._x1_=_lim_((f_|_X)_/*_s1)_)
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom (f | X) & s1 is convergent & lim s1 = x1 implies ( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) ) )
assume that
A14: rng s1 c= dom (f | X) and
A15: s1 is convergent and
A16: lim s1 = x1 ; ::_thesis: ( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_((f_|_X)_/*_s1)_._n_=_(f_/*_s1)_._n
let n be Element of NAT ; ::_thesis: ((f | X) /* s1) . n = (f /* s1) . n
A17: s1 . n in rng s1 by VALUED_0:28;
thus ((f | X) /* s1) . n = (f | X) /. (s1 . n) by A14, FUNCT_2:109
.= f /. (s1 . n) by A14, A17, PARTFUN2:15
.= (f /* s1) . n by A10, A12, A14, FUNCT_2:109, XBOOLE_1:1 ; ::_thesis: verum
end;
then A18: (f | X) /* s1 = f /* s1 by FUNCT_2:63;
(f | X) /. (lim s1) = f /. (lim s1) by A13, A12, A16, PARTFUN2:15
.= lim ((f | X) /* s1) by A11, A13, A12, A14, A15, A16, A18 ;
hence ( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) ) by A11, A13, A12, A14, A15, A16, A18; ::_thesis: verum
end;
hence f | X is_continuous_in x1 by A13, A12, Def1; ::_thesis: verum
end;
hence f is_continuous_on X by A10, Def2; ::_thesis: verum
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 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
let X be set ; ::_thesis: 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 ) ) ) ) )
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( 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 ) ) ) ) )
thus ( f is_continuous_on X implies ( 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 ) ) ) ) ) ::_thesis: ( 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 ) ) ) implies f is_continuous_on X )
proof
assume A1: f is_continuous_on X ; ::_thesis: ( 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 ) ) ) )
hence X c= dom f by Def2; ::_thesis: 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 ) )
A2: X c= dom f by A1, Def2;
let x0 be Element of COMPLEX ; ::_thesis: 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 ) )
let r be Real; ::_thesis: ( x0 in X & 0 < r implies 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 ) ) )
assume that
A3: x0 in X and
A4: 0 < r ; ::_thesis: 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 ) )
f | X is_continuous_in x0 by A1, A3, Def2;
then consider s being Real such that
A5: 0 < s and
A6: for x1 being Element of COMPLEX st x1 in dom (f | X) & |.(x1 - x0).| < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r by A4, Th32;
take s ; ::_thesis: ( 0 < s & ( for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
thus 0 < s by A5; ::_thesis: for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r
let x1 be Element of COMPLEX ; ::_thesis: ( x1 in X & |.(x1 - x0).| < s implies |.((f /. x1) - (f /. x0)).| < r )
assume that
A7: x1 in X and
A8: |.(x1 - x0).| < s ; ::_thesis: |.((f /. x1) - (f /. x0)).| < r
A9: dom (f | X) = (dom f) /\ X by RELAT_1:61
.= X by A2, XBOOLE_1:28 ;
then |.((f /. x1) - (f /. x0)).| = |.(((f | X) /. x1) - (f /. x0)).| by A7, PARTFUN2:15
.= |.(((f | X) /. x1) - ((f | X) /. x0)).| by A3, A9, PARTFUN2:15 ;
hence |.((f /. x1) - (f /. x0)).| < r by A6, A9, A7, A8; ::_thesis: verum
end;
assume that
A10: X c= dom f and
A11: 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 ) ) ; ::_thesis: f is_continuous_on X
A12: dom (f | X) = (dom f) /\ X by RELAT_1:61
.= X by A10, XBOOLE_1:28 ;
now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_X_holds_
f_|_X_is_continuous_in_x0
let x0 be Element of COMPLEX ; ::_thesis: ( x0 in X implies f | X is_continuous_in x0 )
assume A13: x0 in X ; ::_thesis: f | X is_continuous_in x0
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 | X) & |.(x1 - x0).| < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) )
proof
let r be Real; ::_thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Element of COMPLEX st x1 in dom (f | X) & |.(x1 - x0).| < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) ) )
assume 0 < r ; ::_thesis: ex s being Real st
( 0 < s & ( for x1 being Element of COMPLEX st x1 in dom (f | X) & |.(x1 - x0).| < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) )
then consider s being Real such that
A14: 0 < s and
A15: for x1 being Element of COMPLEX st x1 in X & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r by A11, A13;
take s ; ::_thesis: ( 0 < s & ( for x1 being Element of COMPLEX st x1 in dom (f | X) & |.(x1 - x0).| < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) )
thus 0 < s by A14; ::_thesis: for x1 being Element of COMPLEX st x1 in dom (f | X) & |.(x1 - x0).| < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r
let x1 be Element of COMPLEX ; ::_thesis: ( x1 in dom (f | X) & |.(x1 - x0).| < s implies |.(((f | X) /. x1) - ((f | X) /. x0)).| < r )
assume that
A16: x1 in dom (f | X) and
A17: |.(x1 - x0).| < s ; ::_thesis: |.(((f | X) /. x1) - ((f | X) /. x0)).| < r
|.(((f | X) /. x1) - ((f | X) /. x0)).| = |.(((f | X) /. x1) - (f /. x0)).| by A12, A13, PARTFUN2:15
.= |.((f /. x1) - (f /. x0)).| by A16, PARTFUN2:15 ;
hence |.(((f | X) /. x1) - ((f | X) /. x0)).| < r by A12, A15, A16, A17; ::_thesis: verum
end;
hence f | X is_continuous_in x0 by A12, A13, Th32; ::_thesis: verum
end;
hence f is_continuous_on X by A10, Def2; ::_thesis: verum
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
let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX holds
( f is_continuous_on X iff f | X is_continuous_on X )
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_on X iff f | X is_continuous_on X )
thus ( f is_continuous_on X implies f | X is_continuous_on X ) ::_thesis: ( f | X is_continuous_on X implies f is_continuous_on X )
proof
assume A1: f is_continuous_on X ; ::_thesis: f | X is_continuous_on X
then X c= dom f by Def2;
then X c= (dom f) /\ X by XBOOLE_1:28;
hence X c= dom (f | X) by RELAT_1:61; :: according to CFCONT_1:def_2 ::_thesis: for x0 being Element of COMPLEX st x0 in X holds
(f | X) | X is_continuous_in x0
let g be Element of COMPLEX ; ::_thesis: ( g in X implies (f | X) | X is_continuous_in g )
assume g in X ; ::_thesis: (f | X) | X is_continuous_in g
then f | X is_continuous_in g by A1, Def2;
hence (f | X) | X is_continuous_in g by RELAT_1:72; ::_thesis: verum
end;
assume A2: f | X is_continuous_on X ; ::_thesis: f is_continuous_on X
then X c= dom (f | X) by Def2;
then ( (dom f) /\ X c= dom f & X c= (dom f) /\ X ) by RELAT_1:61, XBOOLE_1:17;
hence X c= dom f by XBOOLE_1:1; :: according to CFCONT_1:def_2 ::_thesis: for x0 being Element of COMPLEX st x0 in X holds
f | X is_continuous_in x0
let g be Element of COMPLEX ; ::_thesis: ( g in X implies f | X is_continuous_in g )
assume g in X ; ::_thesis: f | X is_continuous_in g
then (f | X) | X is_continuous_in g by A2, Def2;
hence f | X is_continuous_in g by RELAT_1:72; ::_thesis: verum
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
let X, X1 be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X & X1 c= X holds
f is_continuous_on X1
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_on X & X1 c= X implies f is_continuous_on X1 )
assume that
A1: f is_continuous_on X and
A2: X1 c= X ; ::_thesis: f is_continuous_on X1
X c= dom f by A1, Def2;
hence A3: X1 c= dom f by A2, XBOOLE_1:1; :: according to CFCONT_1:def_2 ::_thesis: for x0 being Element of COMPLEX st x0 in X1 holds
f | X1 is_continuous_in x0
let g be Element of COMPLEX ; ::_thesis: ( g in X1 implies f | X1 is_continuous_in g )
assume A4: g in X1 ; ::_thesis: f | X1 is_continuous_in g
then A5: f | X is_continuous_in g by A1, A2, Def2;
thus f | X1 is_continuous_in g ::_thesis: verum
proof
(dom f) /\ X1 c= (dom f) /\ X by A2, XBOOLE_1:26;
then dom (f | X1) c= (dom f) /\ X by RELAT_1:61;
then A6: dom (f | X1) c= dom (f | X) by RELAT_1:61;
g in (dom f) /\ X1 by A3, A4, XBOOLE_0:def_4;
hence A7: g in dom (f | X1) by RELAT_1:61; :: according to CFCONT_1:def_1 ::_thesis: for s1 being Complex_Sequence st rng s1 c= dom (f | X1) & s1 is convergent & lim s1 = g holds
( (f | X1) /* s1 is convergent & (f | X1) /. g = lim ((f | X1) /* s1) )
then A8: (f | X) /. g = f /. g by A6, PARTFUN2:15
.= (f | X1) /. g by A7, PARTFUN2:15 ;
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom (f | X1) & s1 is convergent & lim s1 = g implies ( (f | X1) /* s1 is convergent & (f | X1) /. g = lim ((f | X1) /* s1) ) )
assume that
A9: rng s1 c= dom (f | X1) and
A10: ( s1 is convergent & lim s1 = g ) ; ::_thesis: ( (f | X1) /* s1 is convergent & (f | X1) /. g = lim ((f | X1) /* s1) )
A11: rng s1 c= dom (f | X) by A9, A6, XBOOLE_1:1;
A12: now__::_thesis:_for_n_being_Element_of_NAT_holds_((f_|_X)_/*_s1)_._n_=_((f_|_X1)_/*_s1)_._n
let n be Element of NAT ; ::_thesis: ((f | X) /* s1) . n = ((f | X1) /* s1) . n
A13: s1 . n in rng s1 by VALUED_0:28;
thus ((f | X) /* s1) . n = (f | X) /. (s1 . n) by A9, A6, FUNCT_2:109, XBOOLE_1:1
.= f /. (s1 . n) by A11, A13, PARTFUN2:15
.= (f | X1) /. (s1 . n) by A9, A13, PARTFUN2:15
.= ((f | X1) /* s1) . n by A9, FUNCT_2:109 ; ::_thesis: verum
end;
( (f | X) /* s1 is convergent & (f | X) /. g = lim ((f | X) /* s1) ) by A5, A10, A11, Def1;
hence ( (f | X1) /* s1 is convergent & (f | X1) /. g = lim ((f | X1) /* s1) ) by A8, A12, FUNCT_2:63; ::_thesis: verum
end;
end;
theorem :: CFCONT_1:42
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
let x0 be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st x0 in dom f holds
f is_continuous_on {x0}
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( x0 in dom f implies f is_continuous_on {x0} )
assume A1: x0 in dom f ; ::_thesis: f is_continuous_on {x0}
thus {x0} c= dom f :: according to CFCONT_1:def_2 ::_thesis: for x0 being Element of COMPLEX st x0 in {x0} holds
f | {x0} is_continuous_in x0
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x0} or x in dom f )
assume x in {x0} ; ::_thesis: x in dom f
hence x in dom f by A1, TARSKI:def_1; ::_thesis: verum
end;
let t be Element of COMPLEX ; ::_thesis: ( t in {x0} implies f | {x0} is_continuous_in t )
assume A2: t in {x0} ; ::_thesis: f | {x0} is_continuous_in t
thus f | {x0} is_continuous_in t ::_thesis: verum
proof
t in dom f by A1, A2, TARSKI:def_1;
then t in (dom f) /\ {x0} by A2, XBOOLE_0:def_4;
hence t in dom (f | {x0}) by RELAT_1:61; :: according to CFCONT_1:def_1 ::_thesis: for s1 being Complex_Sequence st rng s1 c= dom (f | {x0}) & s1 is convergent & lim s1 = t holds
( (f | {x0}) /* s1 is convergent & (f | {x0}) /. t = lim ((f | {x0}) /* s1) )
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom (f | {x0}) & s1 is convergent & lim s1 = t implies ( (f | {x0}) /* s1 is convergent & (f | {x0}) /. t = lim ((f | {x0}) /* s1) ) )
assume that
A3: rng s1 c= dom (f | {x0}) and
s1 is convergent and
lim s1 = t ; ::_thesis: ( (f | {x0}) /* s1 is convergent & (f | {x0}) /. t = lim ((f | {x0}) /* s1) )
A4: (dom f) /\ {x0} c= {x0} by XBOOLE_1:17;
rng s1 c= (dom f) /\ {x0} by A3, RELAT_1:61;
then A5: rng s1 c= {x0} by A4, XBOOLE_1:1;
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_=_x0
let n be Element of NAT ; ::_thesis: s1 . n = x0
s1 . n in rng s1 by VALUED_0:28;
hence s1 . n = x0 by A5, TARSKI:def_1; ::_thesis: verum
end;
A7: t = x0 by A2, TARSKI:def_1;
A8: now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.((((f_|_{x0})_/*_s1)_._m)_-_((f_|_{x0})_/._t)).|_<_r
let r be Real; ::_thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r )
assume A9: 0 < r ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r
take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds
|.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r )
assume n <= m ; ::_thesis: |.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r
|.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| = |.(((f | {x0}) /. (s1 . m)) - ((f | {x0}) /. x0)).| by A7, A3, FUNCT_2:109
.= |.(((f | {x0}) /. x0) - ((f | {x0}) /. x0)).| by A6
.= 0 by COMPLEX1:44 ;
hence |.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r by A9; ::_thesis: verum
end;
hence (f | {x0}) /* s1 is convergent by COMSEQ_2:def_5; ::_thesis: (f | {x0}) /. t = lim ((f | {x0}) /* s1)
hence (f | {x0}) /. t = lim ((f | {x0}) /* s1) by A8, COMSEQ_2:def_6; ::_thesis: verum
end;
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
let X be set ; ::_thesis: 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 )
let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f1 is_continuous_on X & f2 is_continuous_on X implies ( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X & f1 (#) f2 is_continuous_on X ) )
assume A1: ( f1 is_continuous_on X & f2 is_continuous_on X ) ; ::_thesis: ( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X & f1 (#) f2 is_continuous_on X )
then ( X c= dom f1 & X c= dom f2 ) by Th38;
then A2: X c= (dom f1) /\ (dom f2) by XBOOLE_1:19;
then A3: X c= dom (f1 + f2) by CFUNCT_1:1;
now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_
(_(f1_+_f2)_/*_s1_is_convergent_&_(f1_+_f2)_/._(lim_s1)_=_lim_((f1_+_f2)_/*_s1)_)
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) )
assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X ; ::_thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) )
A7: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A1, A4, A5, A6, Th38;
then A8: (f1 /* s1) + (f2 /* s1) is convergent ;
A9: rng s1 c= (dom f1) /\ (dom f2) by A2, A4, XBOOLE_1:1;
( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A1, A4, A5, A6, Th38;
then (f1 + f2) /. (lim s1) = (lim (f1 /* s1)) + (lim (f2 /* s1)) by A3, A6, CFUNCT_1:1
.= lim ((f1 /* s1) + (f2 /* s1)) by A7, COMSEQ_2:14
.= lim ((f1 + f2) /* s1) by A9, Th7 ;
hence ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) by A9, A8, Th7; ::_thesis: verum
end;
hence f1 + f2 is_continuous_on X by A3, Th38; ::_thesis: ( f1 - f2 is_continuous_on X & f1 (#) f2 is_continuous_on X )
A10: X c= dom (f1 - f2) by A2, CFUNCT_1:2;
now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_
(_(f1_-_f2)_/*_s1_is_convergent_&_(f1_-_f2)_/._(lim_s1)_=_lim_((f1_-_f2)_/*_s1)_)
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) )
assume that
A11: rng s1 c= X and
A12: s1 is convergent and
A13: lim s1 in X ; ::_thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) )
A14: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A1, A11, A12, A13, Th38;
then A15: (f1 /* s1) - (f2 /* s1) is convergent ;
A16: rng s1 c= (dom f1) /\ (dom f2) by A2, A11, XBOOLE_1:1;
( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A1, A11, A12, A13, Th38;
then (f1 - f2) /. (lim s1) = (lim (f1 /* s1)) - (lim (f2 /* s1)) by A10, A13, CFUNCT_1:2
.= lim ((f1 /* s1) - (f2 /* s1)) by A14, COMSEQ_2:26
.= lim ((f1 - f2) /* s1) by A16, Th7 ;
hence ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) by A16, A15, Th7; ::_thesis: verum
end;
hence f1 - f2 is_continuous_on X by A10, Th38; ::_thesis: f1 (#) f2 is_continuous_on X
A17: X c= dom (f1 (#) f2) by A2, CFUNCT_1:3;
now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_
(_(f1_(#)_f2)_/*_s1_is_convergent_&_(f1_(#)_f2)_/._(lim_s1)_=_lim_((f1_(#)_f2)_/*_s1)_)
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. (lim s1) = lim ((f1 (#) f2) /* s1) ) )
assume that
A18: rng s1 c= X and
A19: s1 is convergent and
A20: lim s1 in X ; ::_thesis: ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. (lim s1) = lim ((f1 (#) f2) /* s1) )
A21: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A1, A18, A19, A20, Th38;
then A22: (f1 /* s1) (#) (f2 /* s1) is convergent ;
A23: rng s1 c= (dom f1) /\ (dom f2) by A2, A18, XBOOLE_1:1;
( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A1, A18, A19, A20, Th38;
then (f1 (#) f2) /. (lim s1) = (lim (f1 /* s1)) * (lim (f2 /* s1)) by A17, A20, CFUNCT_1:3
.= lim ((f1 /* s1) (#) (f2 /* s1)) by A21, COMSEQ_2:30
.= lim ((f1 (#) f2) /* s1) by A23, Th7 ;
hence ( (f1 (#) f2) /* s1 is convergent & (f1 (#) f2) /. (lim s1) = lim ((f1 (#) f2) /* s1) ) by A23, A22, Th7; ::_thesis: verum
end;
hence f1 (#) f2 is_continuous_on X by A17, Th38; ::_thesis: verum
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
let X, X1 be set ; ::_thesis: 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 )
let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f1 is_continuous_on X & f2 is_continuous_on X1 implies ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 & f1 (#) f2 is_continuous_on X /\ X1 ) )
assume ( f1 is_continuous_on X & f2 is_continuous_on X1 ) ; ::_thesis: ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 & f1 (#) f2 is_continuous_on X /\ X1 )
then ( f1 is_continuous_on X /\ X1 & f2 is_continuous_on X /\ X1 ) by Th41, XBOOLE_1:17;
hence ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 & f1 (#) f2 is_continuous_on X /\ X1 ) by Th43; ::_thesis: verum
end;
theorem Th45: :: CFCONT_1:45
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
let g be Element of COMPLEX ; ::_thesis: for X being set
for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X holds
g (#) f is_continuous_on X
let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X holds
g (#) f is_continuous_on X
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_on X implies g (#) f is_continuous_on X )
assume A1: f is_continuous_on X ; ::_thesis: g (#) f is_continuous_on X
then A2: X c= dom f by Th38;
then A3: X c= dom (g (#) f) by CFUNCT_1:4;
now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_
(_(g_(#)_f)_/*_s1_is_convergent_&_(g_(#)_f)_/._(lim_s1)_=_lim_((g_(#)_f)_/*_s1)_)
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (g (#) f) /* s1 is convergent & (g (#) f) /. (lim s1) = lim ((g (#) f) /* s1) ) )
assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X ; ::_thesis: ( (g (#) f) /* s1 is convergent & (g (#) f) /. (lim s1) = lim ((g (#) f) /* s1) )
A7: f /* s1 is convergent by A1, A4, A5, A6, Th38;
then A8: g (#) (f /* s1) is convergent ;
f /. (lim s1) = lim (f /* s1) by A1, A4, A5, A6, Th38;
then (g (#) f) /. (lim s1) = g * (lim (f /* s1)) by A3, A6, CFUNCT_1:4
.= lim (g (#) (f /* s1)) by A7, COMSEQ_2:18
.= lim ((g (#) f) /* s1) by A2, A4, Th8, XBOOLE_1:1 ;
hence ( (g (#) f) /* s1 is convergent & (g (#) f) /. (lim s1) = lim ((g (#) f) /* s1) ) by A2, A4, A8, Th8, XBOOLE_1:1; ::_thesis: verum
end;
hence g (#) f is_continuous_on X by A3, Th38; ::_thesis: verum
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
proof
let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X holds
- f is_continuous_on X
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_on X implies - f is_continuous_on X )
A1: - f = (- 1r) (#) f by CFUNCT_1:31;
assume f is_continuous_on X ; ::_thesis: - f is_continuous_on X
hence - f is_continuous_on X by A1, Th45; ::_thesis: verum
end;
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
let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X & f " {0} = {} holds
f ^ is_continuous_on X
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_on X & f " {0} = {} implies f ^ is_continuous_on X )
assume that
A1: f is_continuous_on X and
A2: f " {0} = {} ; ::_thesis: f ^ is_continuous_on X
A3: dom (f ^) = (dom f) \ {} by A2, CFUNCT_1:def_2
.= dom f ;
hence A4: X c= dom (f ^) by A1, Def2; :: according to CFCONT_1:def_2 ::_thesis: for x0 being Element of COMPLEX st x0 in X holds
(f ^) | X is_continuous_in x0
let g be Element of COMPLEX ; ::_thesis: ( g in X implies (f ^) | X is_continuous_in g )
assume A5: g in X ; ::_thesis: (f ^) | X is_continuous_in g
then A6: f | X is_continuous_in g by A1, Def2;
g in (dom (f ^)) /\ X by A4, A5, XBOOLE_0:def_4;
then A7: g in dom ((f ^) | X) by RELAT_1:61;
now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_dom_((f_^)_|_X)_&_s1_is_convergent_&_lim_s1_=_g_holds_
(_((f_^)_|_X)_/*_s1_is_convergent_&_lim_(((f_^)_|_X)_/*_s1)_=_((f_^)_|_X)_/._g_)
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom ((f ^) | X) & s1 is convergent & lim s1 = g implies ( ((f ^) | X) /* s1 is convergent & lim (((f ^) | X) /* s1) = ((f ^) | X) /. g ) )
assume that
A8: rng s1 c= dom ((f ^) | X) and
A9: ( s1 is convergent & lim s1 = g ) ; ::_thesis: ( ((f ^) | X) /* s1 is convergent & lim (((f ^) | X) /* s1) = ((f ^) | X) /. g )
rng s1 c= (dom (f ^)) /\ X by A8, RELAT_1:61;
then A10: rng s1 c= dom (f | X) by A3, RELAT_1:61;
then A11: (f | X) /* s1 is convergent by A6, A9, Def1;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((f_|_X)_/*_s1)_._n_<>_0c
let n be Element of NAT ; ::_thesis: ((f | X) /* s1) . n <> 0c
A12: s1 . n in rng s1 by VALUED_0:28;
( rng s1 c= (dom f) /\ X & (dom f) /\ X c= dom f ) by A3, A8, RELAT_1:61, XBOOLE_1:17;
then A13: rng s1 c= dom f by XBOOLE_1:1;
A14: now__::_thesis:_not_f_/._(s1_._n)_=_0c
assume f /. (s1 . n) = 0c ; ::_thesis: contradiction
then f /. (s1 . n) in {0c} by TARSKI:def_1;
hence contradiction by A2, A13, A12, PARTFUN2:26; ::_thesis: verum
end;
((f | X) /* s1) . n = (f | X) /. (s1 . n) by A10, FUNCT_2:109
.= f /. (s1 . n) by A10, A12, PARTFUN2:15 ;
hence ((f | X) /* s1) . n <> 0c by A14; ::_thesis: verum
end;
then A15: (f | X) /* s1 is non-zero by COMSEQ_1:4;
g in (dom f) /\ X by A3, A4, A5, XBOOLE_0:def_4;
then A16: g in dom (f | X) by RELAT_1:61;
then A17: (f | X) /. g = f /. g by PARTFUN2:15;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(((f_^)_|_X)_/*_s1)_._n_=_(((f_|_X)_/*_s1)_")_._n
let n be Element of NAT ; ::_thesis: (((f ^) | X) /* s1) . n = (((f | X) /* s1) ") . n
A18: s1 . n in rng s1 by VALUED_0:28;
then s1 . n in dom ((f ^) | X) by A8;
then s1 . n in (dom (f ^)) /\ X by RELAT_1:61;
then A19: s1 . n in dom (f ^) by XBOOLE_0:def_4;
thus (((f ^) | X) /* s1) . n = ((f ^) | X) /. (s1 . n) by A8, FUNCT_2:109
.= (f ^) /. (s1 . n) by A8, A18, PARTFUN2:15
.= (f /. (s1 . n)) " by A19, CFUNCT_1:def_2
.= ((f | X) /. (s1 . n)) " by A10, A18, PARTFUN2:15
.= (((f | X) /* s1) . n) " by A10, FUNCT_2:109
.= (((f | X) /* s1) ") . n by VALUED_1:10 ; ::_thesis: verum
end;
then A20: ((f ^) | X) /* s1 = ((f | X) /* s1) " by FUNCT_2:63;
A21: now__::_thesis:_not_f_/._g_=_0c
assume f /. g = 0c ; ::_thesis: contradiction
then f /. g in {0c} by TARSKI:def_1;
hence contradiction by A2, A3, A4, A5, PARTFUN2:26; ::_thesis: verum
end;
then lim ((f | X) /* s1) <> 0c by A6, A9, A10, A17, Def1;
hence ((f ^) | X) /* s1 is convergent by A11, A15, A20, COMSEQ_2:34; ::_thesis: lim (((f ^) | X) /* s1) = ((f ^) | X) /. g
(f | X) /. g = lim ((f | X) /* s1) by A6, A9, A10, Def1;
hence lim (((f ^) | X) /* s1) = ((f | X) /. g) " by A11, A17, A21, A15, A20, COMSEQ_2:35
.= (f /. g) " by A16, PARTFUN2:15
.= (f ^) /. g by A4, A5, CFUNCT_1:def_2
.= ((f ^) | X) /. g by A7, PARTFUN2:15 ;
::_thesis: verum
end;
hence (f ^) | X is_continuous_in g by A7, Def1; ::_thesis: verum
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
let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X & (f | X) " {0} = {} holds
f ^ is_continuous_on X
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_continuous_on X & (f | X) " {0} = {} implies f ^ is_continuous_on X )
assume that
A1: f is_continuous_on X and
A2: (f | X) " {0} = {} ; ::_thesis: f ^ is_continuous_on X
f | X is_continuous_on X by A1, Th40;
then (f | X) ^ is_continuous_on X by A2, Th47;
then (f ^) | X is_continuous_on X by CFUNCT_1:54;
hence f ^ is_continuous_on X by Th40; ::_thesis: verum
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
let X be set ; ::_thesis: 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
let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f1 is_continuous_on X & f1 " {0} = {} & f2 is_continuous_on X implies f2 / f1 is_continuous_on X )
assume that
A1: ( f1 is_continuous_on X & f1 " {0} = {} ) and
A2: f2 is_continuous_on X ; ::_thesis: f2 / f1 is_continuous_on X
f1 ^ is_continuous_on X by A1, Th47;
then f2 (#) (f1 ^) is_continuous_on X by A2, Th43;
hence f2 / f1 is_continuous_on X by CFUNCT_1:39; ::_thesis: verum
end;
theorem :: CFCONT_1:50
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
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( 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 implies f is_continuous_on COMPLEX )
assume that
A1: f is total and
A2: for x1, x2 being Element of COMPLEX holds f /. (x1 + x2) = (f /. x1) + (f /. x2) and
A3: ex x0 being Element of COMPLEX st f is_continuous_in x0 ; ::_thesis: f is_continuous_on COMPLEX
A4: dom f = COMPLEX by A1, PARTFUN1:def_2;
consider x0 being Element of COMPLEX such that
A5: f is_continuous_in x0 by A3;
A6: (f /. x0) + 0c = f /. (x0 + 0c)
.= (f /. x0) + (f /. 0c) by A2 ;
A7: now__::_thesis:_for_x1_being_Element_of_COMPLEX_holds_-_(f_/._x1)_=_f_/._(-_x1)
let x1 be Element of COMPLEX ; ::_thesis: - (f /. x1) = f /. (- x1)
0c = f /. (x1 + (- x1)) by A6
.= (f /. x1) + (f /. (- x1)) by A2 ;
hence - (f /. x1) = f /. (- x1) ; ::_thesis: verum
end;
A8: now__::_thesis:_for_x1,_x2_being_Element_of_COMPLEX_holds_f_/._(x1_-_x2)_=_(f_/._x1)_-_(f_/._x2)
let x1, x2 be Element of COMPLEX ; ::_thesis: f /. (x1 - x2) = (f /. x1) - (f /. x2)
thus f /. (x1 - x2) = f /. (x1 + (- x2))
.= (f /. x1) + (f /. (- x2)) by A2
.= (f /. x1) + (- (f /. x2)) by A7
.= (f /. x1) - (f /. x2) ; ::_thesis: verum
end;
now__::_thesis:_for_x1_being_Element_of_COMPLEX_
for_r_being_Real_st_x1_in_COMPLEX_&_r_>_0_holds_
ex_s_being_Real_st_
(_s_>_0_&_(_for_x2_being_Element_of_COMPLEX_st_x2_in_COMPLEX_&_|.(x2_-_x1).|_<_s_holds_
|.((f_/._x2)_-_(f_/._x1)).|_<_r_)_)
let x1 be Element of COMPLEX ; ::_thesis: for r being Real st x1 in COMPLEX & r > 0 holds
ex s being Real st
( s > 0 & ( for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.((f /. x2) - (f /. x1)).| < r ) )
let r be Real; ::_thesis: ( x1 in COMPLEX & r > 0 implies ex s being Real st
( s > 0 & ( for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.((f /. x2) - (f /. x1)).| < r ) ) )
assume that
x1 in COMPLEX and
A9: r > 0 ; ::_thesis: ex s being Real st
( s > 0 & ( for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.((f /. x2) - (f /. x1)).| < r ) )
set y = x1 - x0;
consider s being Real such that
A10: 0 < s and
A11: for x1 being Element of COMPLEX st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r by A5, A9, Th32;
take s = s; ::_thesis: ( s > 0 & ( for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.((f /. x2) - (f /. x1)).| < r ) )
thus s > 0 by A10; ::_thesis: for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.((f /. x2) - (f /. x1)).| < r
let x2 be Element of COMPLEX ; ::_thesis: ( x2 in COMPLEX & |.(x2 - x1).| < s implies |.((f /. x2) - (f /. x1)).| < r )
assume that
x2 in COMPLEX and
A12: |.(x2 - x1).| < s ; ::_thesis: |.((f /. x2) - (f /. x1)).| < r
A13: |.((x2 - (x1 - x0)) - x0).| = |.(x2 - x1).| ;
(x1 - x0) + x0 = x1 ;
then |.((f /. x2) - (f /. x1)).| = |.((f /. x2) - ((f /. (x1 - x0)) + (f /. x0))).| by A2
.= |.(((f /. x2) - (f /. (x1 - x0))) - (f /. x0)).|
.= |.((f /. (x2 - (x1 - x0))) - (f /. x0)).| by A8 ;
hence |.((f /. x2) - (f /. x1)).| < r by A4, A11, A12, A13; ::_thesis: verum
end;
hence f is_continuous_on COMPLEX by A4, Th39; ::_thesis: verum
end;
definition
let X be set ;
attrX is compact means :Def3: :: 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 Def3 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
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( dom f is compact & f is_continuous_on dom f implies rng f is compact )
assume that
A1: dom f is compact and
A2: f is_continuous_on dom f ; ::_thesis: rng f is compact
now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_rng_f_holds_
ex_q2_being_Element_of_K19(K20(NAT,COMPLEX))_st_
(_q2_is_subsequence_of_s1_&_q2_is_convergent_&_lim_q2_in_rng_f_)
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= rng f implies ex q2 being Element of K19(K20(NAT,COMPLEX)) st
( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) )
assume A3: rng s1 c= rng f ; ::_thesis: ex q2 being Element of K19(K20(NAT,COMPLEX)) st
( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )
defpred S1[ set , set ] means ( $2 in dom f & f /. $2 = s1 . $1 );
A4: for n being Element of NAT ex g being Element of COMPLEX st S1[n,g]
proof
let n be Element of NAT ; ::_thesis: ex g being Element of COMPLEX st S1[n,g]
s1 . n in rng s1 by VALUED_0:28;
then consider g being Element of COMPLEX such that
A5: ( g in dom f & s1 . n = f . g ) by A3, PARTFUN1:3;
take g ; ::_thesis: S1[n,g]
thus S1[n,g] by A5, PARTFUN1:def_6; ::_thesis: verum
end;
consider q1 being Complex_Sequence such that
A6: for n being Element of NAT holds S1[n,q1 . n] from CFCONT_1:sch_1(A4);
now__::_thesis:_for_x_being_set_st_x_in_rng_q1_holds_
x_in_dom_f
let x be set ; ::_thesis: ( x in rng q1 implies x in dom f )
assume x in rng q1 ; ::_thesis: x in dom f
then ex n being Element of NAT st x = q1 . n by FUNCT_2:113;
hence x in dom f by A6; ::_thesis: verum
end;
then A7: rng q1 c= dom f by TARSKI:def_3;
then consider s2 being Complex_Sequence such that
A8: s2 is subsequence of q1 and
A9: s2 is convergent and
A10: lim s2 in dom f by A1, Def3;
take q2 = f /* s2; ::_thesis: ( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )
rng s2 c= rng q1 by A8, VALUED_0:21;
then A11: rng s2 c= dom f by A7, XBOOLE_1:1;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(f_/*_q1)_._n_=_s1_._n
let n be Element of NAT ; ::_thesis: (f /* q1) . n = s1 . n
f /. (q1 . n) = s1 . n by A6;
hence (f /* q1) . n = s1 . n by A7, FUNCT_2:109; ::_thesis: verum
end;
then A12: f /* q1 = s1 by FUNCT_2:63;
f | (dom f) is_continuous_in lim s2 by A2, A10, Def2;
then A13: f is_continuous_in lim s2 by RELAT_1:68;
then f /. (lim s2) = lim (f /* s2) by A9, A11, Def1;
then f . (lim s2) = lim (f /* s2) by A10, PARTFUN1:def_6;
hence ( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) by A7, A12, A8, A9, A10, A13, A11, Def1, FUNCT_1:def_3, VALUED_0:22; ::_thesis: verum
end;
hence rng f is compact by Def3; ::_thesis: verum
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
let Y be Subset of COMPLEX; ::_thesis: 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
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( Y c= dom f & Y is compact & f is_continuous_on Y implies f .: Y is compact )
assume that
A1: Y c= dom f and
A2: Y is compact and
A3: f is_continuous_on Y ; ::_thesis: f .: Y is compact
A4: dom (f | Y) = (dom f) /\ Y by RELAT_1:61
.= Y by A1, XBOOLE_1:28 ;
f | Y is_continuous_on Y
proof
thus Y c= dom (f | Y) by A4; :: according to CFCONT_1:def_2 ::_thesis: for x0 being Element of COMPLEX st x0 in Y holds
(f | Y) | Y is_continuous_in x0
let g be Element of COMPLEX ; ::_thesis: ( g in Y implies (f | Y) | Y is_continuous_in g )
assume g in Y ; ::_thesis: (f | Y) | Y is_continuous_in g
then f | Y is_continuous_in g by A3, Def2;
hence (f | Y) | Y is_continuous_in g by RELAT_1:72; ::_thesis: verum
end;
then rng (f | Y) is compact by A2, A4, Th51;
hence f .: Y is compact by RELAT_1:115; ::_thesis: verum
end;