let CNS be ComplexNormSpace; for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS st f is_continuous_on X holds
( ||.f.|| is_continuous_on X & - f is_continuous_on X )
let RNS be RealNormSpace; for X being set
for f being PartFunc of CNS,RNS st f is_continuous_on X holds
( ||.f.|| is_continuous_on X & - f is_continuous_on X )
let X be set ; for f being PartFunc of CNS,RNS st f is_continuous_on X holds
( ||.f.|| is_continuous_on X & - f is_continuous_on X )
let f be PartFunc of CNS,RNS; ( f is_continuous_on X implies ( ||.f.|| is_continuous_on X & - f is_continuous_on X ) )
assume A1:
f is_continuous_on X
; ( ||.f.|| is_continuous_on X & - f is_continuous_on X )
thus
||.f.|| is_continuous_on X
- f is_continuous_on Xproof
A2:
X c= dom f
by A1;
hence A3:
X c= dom ||.f.||
by NORMSP_0:def 3;
NCFCONT1:def 15 for x0 being Point of CNS st x0 in X holds
||.f.|| | X is_continuous_in x0
let r be
Point of
CNS;
( r in X implies ||.f.|| | X is_continuous_in r )
assume A4:
r in X
;
||.f.|| | X is_continuous_in r
then A5:
f | X is_continuous_in r
by A1;
thus
||.f.|| | X is_continuous_in r
verumproof
A6:
r in (dom ||.f.||) /\ X
by A3, A4, XBOOLE_0:def 4;
hence
r in dom (||.f.|| | X)
by RELAT_1:61;
NCFCONT1:def 9 for seq being sequence of CNS st rng seq c= dom (||.f.|| | X) & seq is convergent & lim seq = r holds
( (||.f.|| | X) /* seq is convergent & (||.f.|| | X) /. r = lim ((||.f.|| | X) /* seq) )
let s1 be
sequence of
CNS;
( rng s1 c= dom (||.f.|| | X) & s1 is convergent & lim s1 = r implies ( (||.f.|| | X) /* s1 is convergent & (||.f.|| | X) /. r = lim ((||.f.|| | X) /* s1) ) )
assume that A7:
rng s1 c= dom (||.f.|| | X)
and A8:
(
s1 is
convergent &
lim s1 = r )
;
( (||.f.|| | X) /* s1 is convergent & (||.f.|| | X) /. r = lim ((||.f.|| | X) /* s1) )
rng s1 c= (dom ||.f.||) /\ X
by A7, RELAT_1:61;
then
rng s1 c= (dom f) /\ X
by NORMSP_0:def 3;
then A9:
rng s1 c= dom (f | X)
by RELAT_1:61;
then A10:
(f | X) /. r = lim ((f | X) /* s1)
by A5, A8;
then A15:
||.((f | X) /* s1).|| = (||.f.|| | X) /* s1
by FUNCT_2:63;
A16:
(f | X) /* s1 is
convergent
by A5, A8, A9;
hence
(||.f.|| | X) /* s1 is
convergent
by A15, NORMSP_1:23;
(||.f.|| | X) /. r = lim ((||.f.|| | X) /* s1)
||.((f | X) /. r).|| =
||.(f /. r).||
by A2, A4, PARTFUN2:17
.=
||.f.|| . r
by A3, A4, NORMSP_0:def 3
.=
||.f.|| /. r
by A3, A4, PARTFUN1:def 6
.=
(||.f.|| | X) /. r
by A6, PARTFUN2:16
;
hence
(||.f.|| | X) /. r = lim ((||.f.|| | X) /* s1)
by A16, A10, A15, LOPBAN_1:20;
verum
end;
end;
(- 1) (#) f is_continuous_on X
by A1, Th69;
hence
- f is_continuous_on X
by VFUNCT_1:23; verum