let X be set ; for f being PartFunc of REAL,REAL st X c= dom f holds
( f | X is continuous iff for s1 being Real_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 REAL,REAL; ( X c= dom f implies ( f | X is continuous iff for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) ) )
assume A1:
X c= dom f
; ( f | X is continuous iff for s1 being Real_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 | X is continuous implies for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) )
( ( for s1 being Real_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 | X is continuous )proof
assume A2:
f | X is
continuous
;
for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) )
now for s1 being Real_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
Real_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:
dom (f | X) =
(dom f) /\ X
by RELAT_1:61
.=
X
by A1, XBOOLE_1:28
;
then A7:
f | X is_continuous_in lim s1
by A2, A5;
then A9:
(f | X) /* s1 = f /* s1
by FUNCT_2:63;
f . (lim s1) =
(f | X) . (lim s1)
by A5, A6, FUNCT_1:47
.=
lim (f /* s1)
by A3, A4, A6, A7, A9
;
hence
(
f /* s1 is
convergent &
f . (lim s1) = lim (f /* s1) )
by A3, A4, A6, A7, A9;
verum end;
hence
for
s1 being
Real_Sequence st
rng s1 c= X &
s1 is
convergent &
lim s1 in X holds
(
f /* s1 is
convergent &
f . (lim s1) = lim (f /* s1) )
;
verum
end;
assume A10:
for s1 being Real_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 | X is continuous
now for x1 being Real st x1 in dom (f | X) holds
f | X is_continuous_in x1A11:
dom (f | X) =
(dom f) /\ X
by RELAT_1:61
.=
X
by A1, XBOOLE_1:28
;
let x1 be
Real;
( x1 in dom (f | X) implies f | X is_continuous_in x1 )assume A12:
x1 in dom (f | X)
;
f | X is_continuous_in x1now for s1 being Real_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
Real_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 A13:
rng s1 c= dom (f | X)
and A14:
s1 is
convergent
and A15:
lim s1 = x1
;
( (f | X) /* s1 is convergent & (f | X) . x1 = lim ((f | X) /* s1) )then A17:
(f | X) /* s1 = f /* s1
by FUNCT_2:63;
(f | X) . (lim s1) =
f . (lim s1)
by A12, A15, FUNCT_1:47
.=
lim ((f | X) /* s1)
by A10, A12, A11, A13, A14, A15, A17
;
hence
(
(f | X) /* s1 is
convergent &
(f | X) . x1 = lim ((f | X) /* s1) )
by A10, A12, A11, A13, A14, A15, A17;
verum end; hence
f | X is_continuous_in x1
;
verum end;
hence
f | X is continuous
; verum