let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL

for S being SigmaField of X

for A being Element of S st f is A -measurable holds

max+ f is A -measurable

let f be PartFunc of X,ExtREAL; :: thesis: for S being SigmaField of X

for A being Element of S st f is A -measurable holds

max+ f is A -measurable

let S be SigmaField of X; :: thesis: for A being Element of S st f is A -measurable holds

max+ f is A -measurable

let A be Element of S; :: thesis: ( f is A -measurable implies max+ f is A -measurable )

assume A1: f is A -measurable ; :: thesis: max+ f is A -measurable

for r being Real holds A /\ (less_dom ((max+ f),r)) in S

for S being SigmaField of X

for A being Element of S st f is A -measurable holds

max+ f is A -measurable

let f be PartFunc of X,ExtREAL; :: thesis: for S being SigmaField of X

for A being Element of S st f is A -measurable holds

max+ f is A -measurable

let S be SigmaField of X; :: thesis: for A being Element of S st f is A -measurable holds

max+ f is A -measurable

let A be Element of S; :: thesis: ( f is A -measurable implies max+ f is A -measurable )

assume A1: f is A -measurable ; :: thesis: max+ f is A -measurable

for r being Real holds A /\ (less_dom ((max+ f),r)) in S

proof

hence
max+ f is A -measurable
; :: thesis: verum
let r be Real; :: thesis: A /\ (less_dom ((max+ f),r)) in S

reconsider r = r as Real ;

end;reconsider r = r as Real ;

now :: thesis: A /\ (less_dom ((max+ f),r)) in Send;

hence
A /\ (less_dom ((max+ f),r)) in S
; :: thesis: verumper cases
( 0 < r or r <= 0 )
;

end;

suppose A2:
0 < r
; :: thesis: A /\ (less_dom ((max+ f),r)) in S

for x being object st x in less_dom ((max+ f),r) holds

x in less_dom (f,r)

for x being object st x in less_dom (f,r) holds

x in less_dom ((max+ f),r)

then less_dom ((max+ f),r) = less_dom (f,r) by A10;

hence A /\ (less_dom ((max+ f),r)) in S by A1; :: thesis: verum

end;x in less_dom (f,r)

proof

then A10:
less_dom ((max+ f),r) c= less_dom (f,r)
;
let x be object ; :: thesis: ( x in less_dom ((max+ f),r) implies x in less_dom (f,r) )

assume A3: x in less_dom ((max+ f),r) ; :: thesis: x in less_dom (f,r)

then A4: x in dom (max+ f) by MESFUNC1:def 11;

A5: (max+ f) . x < r by A3, MESFUNC1:def 11;

reconsider x = x as Element of X by A3;

A6: max ((f . x),0.) < r by A4, A5, Def2;

then A7: f . x <= r by XXREAL_0:30;

f . x <> r

x in dom f by A4, Def2;

hence x in less_dom (f,r) by A9, MESFUNC1:def 11; :: thesis: verum

end;assume A3: x in less_dom ((max+ f),r) ; :: thesis: x in less_dom (f,r)

then A4: x in dom (max+ f) by MESFUNC1:def 11;

A5: (max+ f) . x < r by A3, MESFUNC1:def 11;

reconsider x = x as Element of X by A3;

A6: max ((f . x),0.) < r by A4, A5, Def2;

then A7: f . x <= r by XXREAL_0:30;

f . x <> r

proof

then A9:
f . x < r
by A7, XXREAL_0:1;
assume A8:
f . x = r
; :: thesis: contradiction

then max ((f . x),0.) = 0. by A6, XXREAL_0:16;

hence contradiction by A6, A8, XXREAL_0:def 10; :: thesis: verum

end;then max ((f . x),0.) = 0. by A6, XXREAL_0:16;

hence contradiction by A6, A8, XXREAL_0:def 10; :: thesis: verum

x in dom f by A4, Def2;

hence x in less_dom (f,r) by A9, MESFUNC1:def 11; :: thesis: verum

for x being object st x in less_dom (f,r) holds

x in less_dom ((max+ f),r)

proof

then
less_dom (f,r) c= less_dom ((max+ f),r)
;
let x be object ; :: thesis: ( x in less_dom (f,r) implies x in less_dom ((max+ f),r) )

assume A11: x in less_dom (f,r) ; :: thesis: x in less_dom ((max+ f),r)

then A12: x in dom f by MESFUNC1:def 11;

A13: f . x < r by A11, MESFUNC1:def 11;

reconsider x = x as Element of X by A11;

A14: x in dom (max+ f) by A12, Def2;

end;assume A11: x in less_dom (f,r) ; :: thesis: x in less_dom ((max+ f),r)

then A12: x in dom f by MESFUNC1:def 11;

A13: f . x < r by A11, MESFUNC1:def 11;

reconsider x = x as Element of X by A11;

A14: x in dom (max+ f) by A12, Def2;

now :: thesis: x in less_dom ((max+ f),r)

hence
x in less_dom ((max+ f),r)
; :: thesis: verumend;

then less_dom ((max+ f),r) = less_dom (f,r) by A10;

hence A /\ (less_dom ((max+ f),r)) in S by A1; :: thesis: verum

suppose A15:
r <= 0
; :: thesis: A /\ (less_dom ((max+ f),r)) in S

for x being Element of X holds not x in less_dom ((max+ f),r)

hence A /\ (less_dom ((max+ f),r)) in S by PROB_1:4; :: thesis: verum

end;proof

then
less_dom ((max+ f),r) = {}
by SUBSET_1:4;
let x be Element of X; :: thesis: not x in less_dom ((max+ f),r)

assume A16: x in less_dom ((max+ f),r) ; :: thesis: contradiction

then A17: x in dom (max+ f) by MESFUNC1:def 11;

A18: (max+ f) . x < r by A16, MESFUNC1:def 11;

(max+ f) . x = max ((f . x),0.) by A17, Def2;

hence contradiction by A15, A18, XXREAL_0:25; :: thesis: verum

end;assume A16: x in less_dom ((max+ f),r) ; :: thesis: contradiction

then A17: x in dom (max+ f) by MESFUNC1:def 11;

A18: (max+ f) . x < r by A16, MESFUNC1:def 11;

(max+ f) . x = max ((f . x),0.) by A17, Def2;

hence contradiction by A15, A18, XXREAL_0:25; :: thesis: verum

hence A /\ (less_dom ((max+ f),r)) in S by PROB_1:4; :: thesis: verum