let X be set ; for f being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds
( (abs f) | X is continuous & (- f) | X is continuous )
let f be PartFunc of REAL,REAL; ( X c= dom f & f | X is continuous implies ( (abs f) | X is continuous & (- f) | X is continuous ) )
assume A1:
X c= dom f
; ( not f | X is continuous or ( (abs f) | X is continuous & (- f) | X is continuous ) )
assume A2:
f | X is continuous
; ( (abs f) | X is continuous & (- f) | X is continuous )
thus
(abs f) | X is continuous
(- f) | X is continuous proof
let r be
Real;
FCONT_1:def 2 ( r in dom ((abs f) | X) implies (abs f) | X is_continuous_in r )
assume A3:
r in dom ((abs f) | X)
;
(abs f) | X is_continuous_in r
then
r in dom (abs f)
by RELAT_1:57;
then A4:
r in dom f
by VALUED_1:def 11;
r in X
by A3;
then A5:
r in dom (f | X)
by A4, RELAT_1:57;
then A6:
f | X is_continuous_in r
by A2;
thus
(abs f) | X is_continuous_in r
verumproof
let s1 be
Real_Sequence;
FCONT_1:def 1 ( rng s1 c= dom ((abs f) | X) & s1 is convergent & lim s1 = r implies ( ((abs f) | X) /* s1 is convergent & ((abs f) | X) . r = lim (((abs f) | X) /* s1) ) )
assume that A7:
rng s1 c= dom ((abs f) | X)
and A8:
(
s1 is
convergent &
lim s1 = r )
;
( ((abs f) | X) /* s1 is convergent & ((abs f) | X) . r = lim (((abs f) | X) /* s1) )
rng s1 c= (dom (abs f)) /\ X
by A7, RELAT_1:61;
then
rng s1 c= (dom f) /\ X
by VALUED_1:def 11;
then A9:
rng s1 c= dom (f | X)
by RELAT_1:61;
then A12:
abs ((f | X) /* s1) = ((abs f) | X) /* s1
by FUNCT_2:63;
A13:
|.((f | X) . r).| =
|.(f . r).|
by A5, FUNCT_1:47
.=
(abs f) . r
by VALUED_1:18
.=
((abs f) | X) . r
by A3, FUNCT_1:47
;
A14:
(f | X) /* s1 is
convergent
by A6, A8, A9;
hence
((abs f) | X) /* s1 is
convergent
by A12, SEQ_4:13;
((abs f) | X) . r = lim (((abs f) | X) /* s1)
(f | X) . r = lim ((f | X) /* s1)
by A6, A8, A9;
hence
((abs f) | X) . r = lim (((abs f) | X) /* s1)
by A14, A12, A13, SEQ_4:14;
verum
end;
end;
thus
(- f) | X is continuous
by A1, A2, Th20; verum