let x0 be Real; for f being PartFunc of REAL,REAL holds
( f is_continuous_in x0 iff for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f . x0 = lim (f /* s1) ) )
let f be PartFunc of REAL,REAL; ( f is_continuous_in x0 iff for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f . x0 = lim (f /* s1) ) )
thus
( f is_continuous_in x0 implies for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f . x0 = lim (f /* s1) ) )
; ( ( for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f . x0 = lim (f /* s1) ) ) implies f is_continuous_in x0 )
assume A1:
for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f . x0 = lim (f /* s1) )
; f is_continuous_in x0
let s2 be Real_Sequence; FCONT_1:def 1 ( rng s2 c= dom f & s2 is convergent & lim s2 = x0 implies ( f /* s2 is convergent & f . x0 = lim (f /* s2) ) )
assume that
A2:
rng s2 c= dom f
and
A3:
( s2 is convergent & lim s2 = x0 )
; ( f /* s2 is convergent & f . x0 = lim (f /* s2) )
now ( f /* s2 is convergent & f . x0 = lim (f /* s2) )per cases
( 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 A12:
for
n being
Element of
NAT ex
m being
Element of
NAT st
(
n <= m &
s2 . m <> x0 )
;
( f /* s2 is convergent & f . x0 = lim (f /* s2) )defpred S1[
Nat,
set ,
set ]
means for
n,
m being
Element of
NAT st $2
= n & $3
= 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 ]
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
S2[
m]
;
consider M being
Nat such that A14:
(
S2[
M] & ( for
n being
Nat st
S2[
n] holds
M <= n ) )
from NAT_1:sch 5(A13);
reconsider M9 =
M as
Element of
NAT by ORDINAL1:def 12;
A17:
for
n being
Nat for
x being
Element of
NAT ex
y being
Element of
NAT st
S1[
n,
x,
y]
consider F being
sequence of
NAT such that A20:
(
F . 0 = M9 & ( for
n being
Nat holds
S1[
n,
F . n,
F . (n + 1)] ) )
from RECDEF_1:sch 2(A17);
A21:
rng F c= REAL
by NUMBERS:19;
A22:
rng F c= NAT
;
A23:
dom F = NAT
by FUNCT_2:def 1;
then reconsider F =
F as
Real_Sequence by A21, RELSET_1:4;
then reconsider F =
F as
V46()
sequence of
NAT by SEQM_3:def 6;
A25:
(
s2 * F is
convergent &
lim (s2 * F) = x0 )
by A3, SEQ_4:16, SEQ_4:17;
A26:
for
n being
Element of
NAT st
s2 . n <> x0 holds
ex
m being
Element of
NAT st
F . m = n
A38:
for
n being
Nat holds
(s2 * F) . n <> x0
A41:
rng (s2 * F) c= rng s2
by VALUED_0:21;
then
rng (s2 * F) c= dom f
by A2;
then A42:
(
f /* (s2 * F) is
convergent &
f . x0 = lim (f /* (s2 * F)) )
by A1, A38, A25;
hence
f /* s2 is
convergent
by SEQ_2:def 6;
f . x0 = lim (f /* s2)hence
f . x0 = lim (f /* s2)
by A43, SEQ_2:def 7;
verum end; end; end;
hence
( f /* s2 is convergent & f . x0 = lim (f /* s2) )
; verum