let X be 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) ) ) ) )
let f be PartFunc of COMPLEX,COMPLEX; ( 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) ) ) ) )
( 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
;
( 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
;
now 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;
( 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
;
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) )A6:
f | X is_continuous_in lim s1
by A1, A5;
A7:
dom (f | X) =
(dom f) /\ X
by RELAT_1:61
.=
X
by A2, XBOOLE_1:28
;
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
;
hence
(
f /* s1 is
convergent &
f /. (lim s1) = lim (f /* s1) )
by A3, A4, A7, A6, A9;
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;
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) )
; f is_continuous_on X
now for x1 being Complex st x1 in X holds
f | X is_continuous_in x1A12:
dom (f | X) =
(dom f) /\ X
by RELAT_1:61
.=
X
by A10, XBOOLE_1:28
;
let x1 be
Complex;
( x1 in X implies f | X is_continuous_in x1 )assume A13:
x1 in X
;
f | X is_continuous_in x1now 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;
( 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
;
( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) )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;
verum end; hence
f | X is_continuous_in x1
by A13, A12;
verum end;
hence
f is_continuous_on X
by A10; verum