let X be non empty set ; for f being PartFunc of X,ExtREAL
for A being set holds
( max+ (f | A) = (max+ f) | A & max- (f | A) = (max- f) | A )
let f be PartFunc of X,ExtREAL; for A being set holds
( max+ (f | A) = (max+ f) | A & max- (f | A) = (max- f) | A )
let A be set ; ( max+ (f | A) = (max+ f) | A & max- (f | A) = (max- f) | A )
A1: dom (max+ (f | A)) =
dom (f | A)
by MESFUNC2:def 2
.=
(dom f) /\ A
by RELAT_1:61
.=
(dom (max+ f)) /\ A
by MESFUNC2:def 2
.=
dom ((max+ f) | A)
by RELAT_1:61
;
for x being Element of X st x in dom (max+ (f | A)) holds
(max+ (f | A)) . x = ((max+ f) | A) . x
proof
let x be
Element of
X;
( x in dom (max+ (f | A)) implies (max+ (f | A)) . x = ((max+ f) | A) . x )
assume A2:
x in dom (max+ (f | A))
;
(max+ (f | A)) . x = ((max+ f) | A) . x
then A3:
((max+ f) | A) . x = (max+ f) . x
by A1, FUNCT_1:47;
A4:
x in (dom (max+ f)) /\ A
by A1, A2, RELAT_1:61;
then A5:
x in dom (max+ f)
by XBOOLE_0:def 4;
A6:
x in A
by A4, XBOOLE_0:def 4;
(max+ (f | A)) . x =
max (
((f | A) . x),
0)
by A2, MESFUNC2:def 2
.=
max (
(f . x),
0)
by A6, FUNCT_1:49
;
hence
(max+ (f | A)) . x = ((max+ f) | A) . x
by A5, A3, MESFUNC2:def 2;
verum
end;
hence
max+ (f | A) = (max+ f) | A
by A1, PARTFUN1:5; max- (f | A) = (max- f) | A
A7: dom (max- (f | A)) =
dom (f | A)
by MESFUNC2:def 3
.=
(dom f) /\ A
by RELAT_1:61
.=
(dom (max- f)) /\ A
by MESFUNC2:def 3
.=
dom ((max- f) | A)
by RELAT_1:61
;
for x being Element of X st x in dom (max- (f | A)) holds
(max- (f | A)) . x = ((max- f) | A) . x
proof
let x be
Element of
X;
( x in dom (max- (f | A)) implies (max- (f | A)) . x = ((max- f) | A) . x )
assume A8:
x in dom (max- (f | A))
;
(max- (f | A)) . x = ((max- f) | A) . x
then A9:
((max- f) | A) . x = (max- f) . x
by A7, FUNCT_1:47;
A10:
x in (dom (max- f)) /\ A
by A7, A8, RELAT_1:61;
then A11:
x in dom (max- f)
by XBOOLE_0:def 4;
A12:
x in A
by A10, XBOOLE_0:def 4;
(max- (f | A)) . x =
max (
(- ((f | A) . x)),
0)
by A8, MESFUNC2:def 3
.=
max (
(- (f . x)),
0)
by A12, FUNCT_1:49
;
hence
(max- (f | A)) . x = ((max- f) | A) . x
by A11, A9, MESFUNC2:def 3;
verum
end;
hence
max- (f | A) = (max- f) | A
by A7, PARTFUN1:5; verum