let S, T be RealNormSpace; :: thesis: for X being set
for f being PartFunc of S,T holds
( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of S st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) )
let X be set ; :: thesis: for f being PartFunc of S,T holds
( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of S 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 S,T; :: thesis: ( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of S 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 sequence of S 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 sequence of S 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 sequence of S 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 :: thesis: for s1 being sequence of S 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 sequence of S; :: 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;
A7: dom (f | X) = (dom f) /\ X by PARTFUN2:15
.= 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
dom s1 = NAT by FUNCT_2:def 1;
then A8: s1 . n in rng s1 by FUNCT_1:3;
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 ;
hence ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) by A3, A4, A7, A6, A9; :: thesis: verum
end;
hence ( X c= dom f & ( for s1 being sequence of S 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; :: thesis: verum
end;
assume that
A10: X c= dom f and
A11: for s1 being sequence of S 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 Point of S st x1 in X holds
f | X is_continuous_in x1
A12: dom (f | X) = (dom f) /\ X by PARTFUN2:15
.= X by A10, XBOOLE_1:28 ;
let x1 be Point of S; :: 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 sequence of S 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 sequence of S; :: 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
dom s1 = NAT by FUNCT_2:def 1;
then A17: s1 . n in rng s1 by FUNCT_1:3;
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; :: thesis: verum
end;
hence f is_continuous_on X by A10; :: thesis: verum