let CNS be ComplexNormSpace; for RNS being RealNormSpace
for X being set
for f being PartFunc of RNS,CNS 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 RNS,CNS 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 RNS,CNS st f is_continuous_on X holds
( ||.f.|| is_continuous_on X & - f is_continuous_on X )
let f be PartFunc of RNS,CNS; ( 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;
NFCONT_1:def 8 for b1 being Element of the carrier of RNS holds
( not b1 in X or ||.f.|| | X is_continuous_in b1 )
let r be
Point of
RNS;
( not r in X or ||.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;
NFCONT_1:def 6 for b1 being Element of K16(K17(NAT, the carrier of RNS)) holds
( not rng b1 c= dom (||.f.|| | X) or not b1 is convergent or not lim b1 = r or ( (||.f.|| | X) /* b1 is convergent & (||.f.|| | X) /. r = lim ((||.f.|| | X) /* b1) ) )
let s1 be
sequence of
RNS;
( not rng s1 c= dom (||.f.|| | X) or not s1 is convergent or not lim s1 = r or ( (||.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, CLVECT_1:117;
(||.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, CLOPBAN1:19;
verum
end;
end;
(- 1r) (#) f is_continuous_on X
by A1, Th70;
hence
- f is_continuous_on X
by VFUNCT_2:23; verum