let x0 be Real; for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S 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 Real st x1 in dom f & |.(x1 - x0).| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )
let S be RealNormSpace; for f being PartFunc of REAL, the carrier of S 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 Real st x1 in dom f & |.(x1 - x0).| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )
let f be PartFunc of REAL, the carrier of S; ( 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 Real 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 Real st x1 in dom f & |.(x1 - x0).| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )
( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real 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
;
( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) )
hence
x0 in dom f
;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real 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
Real st
(
x1 in dom f &
|.(x1 - x0).| < s & not
||.((f /. x1) - (f /. x0)).|| < r ) )
;
contradiction
defpred S1[
Nat,
Real]
means ( $2
in dom f &
|.($2 - x0).| < 1
/ ($1 + 1) & not
||.((f /. $2) - (f /. x0)).|| < r );
A4:
for
n being
Element of
NAT ex
p being
Element of
REAL st
S1[
n,
p]
consider s1 being
Real_Sequence such that A6:
for
n being
Element of
NAT holds
S1[
n,
s1 . n]
from FUNCT_2:sch 3(A4);
then A7:
rng s1 c= dom f
by TARSKI:def 3;
then A13:
s1 is
convergent
by SEQ_2:def 6;
then
lim s1 = x0
by A8, SEQ_2:def 7;
then
(
f /* s1 is
convergent &
f /. x0 = lim (f /* s1) )
by A1, A7, A13;
then consider n being
Nat such that A14:
for
m being
Nat st
n <= m holds
||.(((f /* s1) . m) - (f /. x0)).|| < r
by A2, NORMSP_1:def 7;
A15:
n in NAT
by ORDINAL1:def 12;
||.(((f /* s1) . n) - (f /. x0)).|| < r
by A14;
then
||.((f /. (s1 . n)) - (f /. x0)).|| < r
by A7, FUNCT_2:109, A15;
hence
contradiction
by A6, A15;
verum
end;
assume A16:
( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) )
; f is_continuous_in x0
hence
f is_continuous_in x0
by A16; verum