let X be non empty set ; for f being PartFunc of X,ExtREAL
for S being SigmaField of X
for A being Element of S st f is A -measurable & A c= dom f holds
max- f is A -measurable
let f be PartFunc of X,ExtREAL; for S being SigmaField of X
for A being Element of S st f is A -measurable & A c= dom f holds
max- f is A -measurable
let S be SigmaField of X; for A being Element of S st f is A -measurable & A c= dom f holds
max- f is A -measurable
let A be Element of S; ( f is A -measurable & A c= dom f implies max- f is A -measurable )
assume A1:
( f is A -measurable & A c= dom f )
; max- f is A -measurable
for r being Real holds A /\ (less_dom ((max- f),r)) in S
proof
let r be
Real;
A /\ (less_dom ((max- f),r)) in S
reconsider r =
r as
Real ;
now A /\ (less_dom ((max- f),r)) in Sper cases
( 0 < r or r <= 0 )
;
suppose A2:
0 < r
;
A /\ (less_dom ((max- f),r)) in S
(- 1) (#) f is
A -measurable
by A1, MESFUNC1:37;
then A3:
- f is
A -measurable
by Th9;
for
x being
object st
x in less_dom (
(max- f),
r) holds
x in less_dom (
(- f),
r)
proof
let x be
object ;
( x in less_dom ((max- f),r) implies x in less_dom ((- f),r) )
assume A4:
x in less_dom (
(max- f),
r)
;
x in less_dom ((- f),r)
then A5:
x in dom (max- f)
by MESFUNC1:def 11;
A6:
(max- f) . x < r
by A4, MESFUNC1:def 11;
reconsider x =
x as
Element of
X by A4;
A7:
max (
(- (f . x)),
0.)
< r
by A5, A6, Def3;
then A8:
- (f . x) <= r
by XXREAL_0:30;
- (f . x) <> r
then A10:
- (f . x) < r
by A8, XXREAL_0:1;
x in dom f
by A5, Def3;
then A11:
x in dom (- f)
by MESFUNC1:def 7;
then
(- f) . x = - (f . x)
by MESFUNC1:def 7;
hence
x in less_dom (
(- f),
r)
by A10, A11, MESFUNC1:def 11;
verum
end; then A12:
less_dom (
(max- f),
r)
c= 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 (
(- f),
r)
c= less_dom (
(max- f),
r)
;
then
less_dom (
(max- f),
r)
= less_dom (
(- f),
r)
by A12;
hence
A /\ (less_dom ((max- f),r)) in S
by A3;
verum end; end; end;
hence
A /\ (less_dom ((max- f),r)) in S
;
verum
end;
hence
max- f is A -measurable
; verum