let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
( max+ f is_simple_func_in S & max- f is_simple_func_in S )
let S be SigmaField of X; for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
( max+ f is_simple_func_in S & max- f is_simple_func_in S )
let M be sigma_Measure of S; for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
( max+ f is_simple_func_in S & max- f is_simple_func_in S )
let f be PartFunc of X,ExtREAL; ( f is_simple_func_in S implies ( max+ f is_simple_func_in S & max- f is_simple_func_in S ) )
assume A1:
f is_simple_func_in S
; ( max+ f is_simple_func_in S & max- f is_simple_func_in S )
then A2:
f is V55()
by MESFUNC2:def 4;
consider F being Finite_Sep_Sequence of S such that
A3:
dom f = union (rng F)
and
A4:
for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
f . x = f . y
by A1, MESFUNC2:def 4;
A5:
dom (max+ f) = union (rng F)
by A3, MESFUNC2:def 2;
for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
(max+ f) . x = (max+ f) . y
proof
let n be
Nat;
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
(max+ f) . x = (max+ f) . ylet x,
y be
Element of
X;
( n in dom F & x in F . n & y in F . n implies (max+ f) . x = (max+ f) . y )
assume that A6:
n in dom F
and A7:
x in F . n
and A8:
y in F . n
;
(max+ f) . x = (max+ f) . y
F . n in rng F
by A6, FUNCT_1:3;
then
(
x in dom (max+ f) &
y in dom (max+ f) )
by A5, A7, A8, TARSKI:def 4;
then
(
(max+ f) . x = max (
(f . x),
0) &
(max+ f) . y = max (
(f . y),
0) )
by MESFUNC2:def 2;
hence
(max+ f) . x = (max+ f) . y
by A4, A6, A7, A8;
verum
end;
hence
max+ f is_simple_func_in S
by A2, A5, Th2, MESFUNC2:def 4; max- f is_simple_func_in S
A9:
dom (max- f) = union (rng F)
by A3, MESFUNC2:def 3;
for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
(max- f) . x = (max- f) . y
proof
let n be
Nat;
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
(max- f) . x = (max- f) . ylet x,
y be
Element of
X;
( n in dom F & x in F . n & y in F . n implies (max- f) . x = (max- f) . y )
assume that A10:
n in dom F
and A11:
x in F . n
and A12:
y in F . n
;
(max- f) . x = (max- f) . y
F . n in rng F
by A10, FUNCT_1:3;
then
(
x in dom (max- f) &
y in dom (max- f) )
by A9, A11, A12, TARSKI:def 4;
then
(
(max- f) . x = max (
(- (f . x)),
0) &
(max- f) . y = max (
(- (f . y)),
0) )
by MESFUNC2:def 3;
hence
(max- f) . x = (max- f) . y
by A4, A10, A11, A12;
verum
end;
hence
max- f is_simple_func_in S
by A2, A9, Th2, MESFUNC2:def 4; verum