let X, X1 be set ; for S being RealNormSpace
for f being PartFunc of S,REAL st f is_continuous_on X & X1 c= X holds
f is_continuous_on X1
let S be RealNormSpace; for f being PartFunc of S,REAL st f is_continuous_on X & X1 c= X holds
f is_continuous_on X1
let f be PartFunc of S,REAL; ( f is_continuous_on X & X1 c= X implies f is_continuous_on X1 )
assume that
A1:
f is_continuous_on X
and
A2:
X1 c= X
; f is_continuous_on X1
X c= dom f
by A1;
hence A3:
X1 c= dom f
by A2; NFCONT_1:def 8 for b1 being Element of the carrier of S holds
( not b1 in X1 or f | X1 is_continuous_in b1 )
let r be Point of S; ( not r in X1 or f | X1 is_continuous_in r )
assume A4:
r in X1
; f | X1 is_continuous_in r
then A5:
f | X is_continuous_in r
by A1, A2;
thus
f | X1 is_continuous_in r
verumproof
(dom f) /\ X1 c= (dom f) /\ X
by A2, XBOOLE_1:26;
then
dom (f | X1) c= (dom f) /\ X
by RELAT_1:61;
then A6:
dom (f | X1) c= dom (f | X)
by RELAT_1:61;
r in (dom f) /\ X1
by A3, A4, XBOOLE_0:def 4;
hence A7:
r in dom (f | X1)
by RELAT_1:61;
NFCONT_1:def 6 for b1 being Element of bool [:NAT, the carrier of S:] holds
( not rng b1 c= dom (f | X1) or not b1 is convergent or not lim b1 = r or ( (f | X1) /* b1 is convergent & (f | X1) /. r = lim ((f | X1) /* b1) ) )
then A8:
(f | X) /. r =
f /. r
by A6, PARTFUN2:15
.=
(f | X1) /. r
by A7, PARTFUN2:15
;
let s1 be
sequence of
S;
( not rng s1 c= dom (f | X1) or not s1 is convergent or not lim s1 = r or ( (f | X1) /* s1 is convergent & (f | X1) /. r = lim ((f | X1) /* s1) ) )
assume that A9:
rng s1 c= dom (f | X1)
and A10:
(
s1 is
convergent &
lim s1 = r )
;
( (f | X1) /* s1 is convergent & (f | X1) /. r = lim ((f | X1) /* s1) )
A11:
rng s1 c= dom (f | X)
by A9, A6;
(
(f | X) /* s1 is
convergent &
(f | X) /. r = lim ((f | X) /* s1) )
by A5, A10, A11;
hence
(
(f | X1) /* s1 is
convergent &
(f | X1) /. r = lim ((f | X1) /* s1) )
by A8, A12, FUNCT_2:63;
verum
end;