:: MESFUNC6 semantic presentation
begin
theorem Th1: :: MESFUNC6:1
for X being non empty set
for f being PartFunc of X,REAL holds |.(R_EAL f).| = R_EAL (abs f)
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds |.(R_EAL f).| = R_EAL (abs f)
let f be PartFunc of X,REAL; ::_thesis: |.(R_EAL f).| = R_EAL (abs f)
A1: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_|.(R_EAL_f).|_holds_
|.(R_EAL_f).|_._x_=_(R_EAL_(abs_f))_._x
let x be Element of X; ::_thesis: ( x in dom |.(R_EAL f).| implies |.(R_EAL f).| . x = (R_EAL (abs f)) . x )
assume x in dom |.(R_EAL f).| ; ::_thesis: |.(R_EAL f).| . x = (R_EAL (abs f)) . x
then |.(R_EAL f).| . x = |.((R_EAL f) . x).| by MESFUNC1:def_10;
then |.(R_EAL f).| . x = abs (f . x) by EXTREAL2:1;
hence |.(R_EAL f).| . x = (R_EAL (abs f)) . x by VALUED_1:18; ::_thesis: verum
end;
dom |.(R_EAL f).| = dom (R_EAL f) by MESFUNC1:def_10
.= dom (abs f) by VALUED_1:def_11 ;
hence |.(R_EAL f).| = R_EAL (abs f) by A1, PARTFUN1:5; ::_thesis: verum
end;
theorem Th2: :: MESFUNC6:2
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for r being Real st dom f in S & ( for x being set st x in dom f holds
f . x = r ) holds
f is_simple_func_in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for r being Real st dom f in S & ( for x being set st x in dom f holds
f . x = r ) holds
f is_simple_func_in S
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for r being Real st dom f in S & ( for x being set st x in dom f holds
f . x = r ) holds
f is_simple_func_in S
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,ExtREAL
for r being Real st dom f in S & ( for x being set st x in dom f holds
f . x = r ) holds
f is_simple_func_in S
let f be PartFunc of X,ExtREAL; ::_thesis: for r being Real st dom f in S & ( for x being set st x in dom f holds
f . x = r ) holds
f is_simple_func_in S
let r be Real; ::_thesis: ( dom f in S & ( for x being set st x in dom f holds
f . x = r ) implies f is_simple_func_in S )
assume that
A1: dom f in S and
A2: for x being set st x in dom f holds
f . x = r ; ::_thesis: f is_simple_func_in S
reconsider Df = dom f as Element of S by A1;
A3: ex F being Finite_Sep_Sequence of S st
( dom f = union (rng F) & ( 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 ) )
proof
set F = <*Df*>;
A4: dom <*Df*> = Seg 1 by FINSEQ_1:38;
A5: now__::_thesis:_for_i,_j_being_Nat_st_i_in_dom_<*Df*>_&_j_in_dom_<*Df*>_&_i_<>_j_holds_
<*Df*>_._i_misses_<*Df*>_._j
let i, j be Nat; ::_thesis: ( i in dom <*Df*> & j in dom <*Df*> & i <> j implies <*Df*> . i misses <*Df*> . j )
assume that
A6: i in dom <*Df*> and
A7: ( j in dom <*Df*> & i <> j ) ; ::_thesis: <*Df*> . i misses <*Df*> . j
i = 1 by A4, A6, FINSEQ_1:2, TARSKI:def_1;
hence <*Df*> . i misses <*Df*> . j by A4, A7, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum
end;
A8: for n being Nat st n in dom <*Df*> holds
<*Df*> . n = Df
proof
let n be Nat; ::_thesis: ( n in dom <*Df*> implies <*Df*> . n = Df )
assume n in dom <*Df*> ; ::_thesis: <*Df*> . n = Df
then n = 1 by A4, FINSEQ_1:2, TARSKI:def_1;
hence <*Df*> . n = Df by FINSEQ_1:40; ::_thesis: verum
end;
reconsider F = <*Df*> as Finite_Sep_Sequence of S by A5, MESFUNC3:4;
take F ; ::_thesis: ( dom f = union (rng F) & ( 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 ) )
F = <*(F . 1)*> by FINSEQ_1:40;
then A9: rng F = {(F . 1)} by FINSEQ_1:38;
1 in Seg 1 ;
then F . 1 = Df by A4, A8;
hence dom f = union (rng F) by A9, ZFMISC_1:25; ::_thesis: 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
hereby ::_thesis: verum
let n be Nat; ::_thesis: 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
let x, y be Element of X; ::_thesis: ( n in dom F & x in F . n & y in F . n implies f . x = f . y )
assume that
A10: n in dom F and
A11: x in F . n and
A12: y in F . n ; ::_thesis: f . x = f . y
A13: F . n = Df by A8, A10;
then f . x = r by A2, A11;
hence f . x = f . y by A2, A12, A13; ::_thesis: verum
end;
end;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_f_holds_
|.(f_._x).|_<_+infty
let x be Element of X; ::_thesis: ( x in dom f implies |.(f . x).| < +infty )
assume x in dom f ; ::_thesis: |.(f . x).| < +infty
then A14: f . x = r by A2;
then -infty < f . x by XXREAL_0:12;
then A15: - +infty < f . x by XXREAL_3:def_3;
f . x < +infty by A14, XXREAL_0:9;
hence |.(f . x).| < +infty by A15, EXTREAL2:11; ::_thesis: verum
end;
then f is V68() by MESFUNC2:def_1;
hence f is_simple_func_in S by A3, MESFUNC2:def_4; ::_thesis: verum
end;
theorem :: MESFUNC6:3
for X being non empty set
for f being PartFunc of X,REAL
for a being real number
for x being set holds
( x in less_dom (f,a) iff ( x in dom f & ex y being Real st
( y = f . x & y < a ) ) )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for a being real number
for x being set holds
( x in less_dom (f,a) iff ( x in dom f & ex y being Real st
( y = f . x & y < a ) ) )
let f be PartFunc of X,REAL; ::_thesis: for a being real number
for x being set holds
( x in less_dom (f,a) iff ( x in dom f & ex y being Real st
( y = f . x & y < a ) ) )
let a be real number ; ::_thesis: for x being set holds
( x in less_dom (f,a) iff ( x in dom f & ex y being Real st
( y = f . x & y < a ) ) )
let x be set ; ::_thesis: ( x in less_dom (f,a) iff ( x in dom f & ex y being Real st
( y = f . x & y < a ) ) )
( ex y being Real st
( y = f . x & y < a ) iff f . x < R_EAL a ) ;
hence ( x in less_dom (f,a) iff ( x in dom f & ex y being Real st
( y = f . x & y < a ) ) ) by MESFUNC1:def_11; ::_thesis: verum
end;
theorem :: MESFUNC6:4
for X being non empty set
for f being PartFunc of X,REAL
for a being real number
for x being set holds
( x in less_eq_dom (f,a) iff ( x in dom f & ex y being Real st
( y = f . x & y <= a ) ) )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for a being real number
for x being set holds
( x in less_eq_dom (f,a) iff ( x in dom f & ex y being Real st
( y = f . x & y <= a ) ) )
let f be PartFunc of X,REAL; ::_thesis: for a being real number
for x being set holds
( x in less_eq_dom (f,a) iff ( x in dom f & ex y being Real st
( y = f . x & y <= a ) ) )
let a be real number ; ::_thesis: for x being set holds
( x in less_eq_dom (f,a) iff ( x in dom f & ex y being Real st
( y = f . x & y <= a ) ) )
let x be set ; ::_thesis: ( x in less_eq_dom (f,a) iff ( x in dom f & ex y being Real st
( y = f . x & y <= a ) ) )
( ex y being Real st
( y = f . x & y <= a ) iff f . x <= R_EAL a ) ;
hence ( x in less_eq_dom (f,a) iff ( x in dom f & ex y being Real st
( y = f . x & y <= a ) ) ) by MESFUNC1:def_12; ::_thesis: verum
end;
theorem :: MESFUNC6:5
for X being non empty set
for f being PartFunc of X,REAL
for r being Real
for x being set holds
( x in great_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r < y ) ) )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for r being Real
for x being set holds
( x in great_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r < y ) ) )
let f be PartFunc of X,REAL; ::_thesis: for r being Real
for x being set holds
( x in great_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r < y ) ) )
let r be Real; ::_thesis: for x being set holds
( x in great_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r < y ) ) )
let x be set ; ::_thesis: ( x in great_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r < y ) ) )
( ex y being Real st
( y = f . x & r < y ) iff R_EAL r < f . x ) ;
hence ( x in great_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r < y ) ) ) by MESFUNC1:def_13; ::_thesis: verum
end;
theorem :: MESFUNC6:6
for X being non empty set
for f being PartFunc of X,REAL
for r being Real
for x being set holds
( x in great_eq_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r <= y ) ) )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for r being Real
for x being set holds
( x in great_eq_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r <= y ) ) )
let f be PartFunc of X,REAL; ::_thesis: for r being Real
for x being set holds
( x in great_eq_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r <= y ) ) )
let r be Real; ::_thesis: for x being set holds
( x in great_eq_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r <= y ) ) )
let x be set ; ::_thesis: ( x in great_eq_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r <= y ) ) )
( ex y being Real st
( y = f . x & r <= y ) iff R_EAL r <= f . x ) ;
hence ( x in great_eq_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r <= y ) ) ) by MESFUNC1:def_14; ::_thesis: verum
end;
theorem :: MESFUNC6:7
for X being non empty set
for f being PartFunc of X,REAL
for r being Real
for x being set holds
( x in eq_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r = y ) ) )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for r being Real
for x being set holds
( x in eq_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r = y ) ) )
let f be PartFunc of X,REAL; ::_thesis: for r being Real
for x being set holds
( x in eq_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r = y ) ) )
let r be Real; ::_thesis: for x being set holds
( x in eq_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r = y ) ) )
let x be set ; ::_thesis: ( x in eq_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r = y ) ) )
( ex y being Real st
( y = f . x & r = y ) iff R_EAL r = f . x ) ;
hence ( x in eq_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r = y ) ) ) by MESFUNC1:def_15; ::_thesis: verum
end;
theorem :: MESFUNC6:8
for X being non empty set
for Y being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) holds
Y /\ (great_eq_dom (f,r)) = meet (rng F)
proof
let X be non empty set ; ::_thesis: for Y being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) holds
Y /\ (great_eq_dom (f,r)) = meet (rng F)
let Y be set ; ::_thesis: for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) holds
Y /\ (great_eq_dom (f,r)) = meet (rng F)
let S be SigmaField of X; ::_thesis: for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) holds
Y /\ (great_eq_dom (f,r)) = meet (rng F)
let F be Function of NAT,S; ::_thesis: for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) holds
Y /\ (great_eq_dom (f,r)) = meet (rng F)
let f be PartFunc of X,REAL; ::_thesis: for r being Real st ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) holds
Y /\ (great_eq_dom (f,r)) = meet (rng F)
let r be Real; ::_thesis: ( ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) implies Y /\ (great_eq_dom (f,r)) = meet (rng F) )
assume for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ; ::_thesis: Y /\ (great_eq_dom (f,r)) = meet (rng F)
then for n being Element of NAT holds F . n = Y /\ (great_dom ((R_EAL f),(R_EAL (r - (1 / (n + 1)))))) ;
then Y /\ (great_eq_dom (f,(R_EAL r))) = meet (rng F) by MESFUNC1:19;
hence Y /\ (great_eq_dom (f,r)) = meet (rng F) ; ::_thesis: verum
end;
theorem :: MESFUNC6:9
for X being non empty set
for Y being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (less_eq_dom (f,r)) = meet (rng F)
proof
let X be non empty set ; ::_thesis: for Y being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (less_eq_dom (f,r)) = meet (rng F)
let Y be set ; ::_thesis: for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (less_eq_dom (f,r)) = meet (rng F)
let S be SigmaField of X; ::_thesis: for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (less_eq_dom (f,r)) = meet (rng F)
let F be Function of NAT,S; ::_thesis: for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (less_eq_dom (f,r)) = meet (rng F)
let f be PartFunc of X,REAL; ::_thesis: for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (less_eq_dom (f,r)) = meet (rng F)
let r be Real; ::_thesis: ( ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) implies Y /\ (less_eq_dom (f,r)) = meet (rng F) )
assume for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ; ::_thesis: Y /\ (less_eq_dom (f,r)) = meet (rng F)
then for n being Element of NAT holds F . n = Y /\ (less_dom ((R_EAL f),(R_EAL (r + (1 / (n + 1)))))) ;
then Y /\ (less_eq_dom (f,(R_EAL r))) = meet (rng F) by MESFUNC1:20;
hence Y /\ (less_eq_dom (f,r)) = meet (rng F) ; ::_thesis: verum
end;
theorem :: MESFUNC6:10
for X being non empty set
for Y being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds
Y /\ (less_dom (f,r)) = union (rng F)
proof
let X be non empty set ; ::_thesis: for Y being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds
Y /\ (less_dom (f,r)) = union (rng F)
let Y be set ; ::_thesis: for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds
Y /\ (less_dom (f,r)) = union (rng F)
let S be SigmaField of X; ::_thesis: for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds
Y /\ (less_dom (f,r)) = union (rng F)
let F be Function of NAT,S; ::_thesis: for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds
Y /\ (less_dom (f,r)) = union (rng F)
let f be PartFunc of X,REAL; ::_thesis: for r being Real st ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds
Y /\ (less_dom (f,r)) = union (rng F)
let r be Real; ::_thesis: ( ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) implies Y /\ (less_dom (f,r)) = union (rng F) )
assume for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ; ::_thesis: Y /\ (less_dom (f,r)) = union (rng F)
then for n being Element of NAT holds F . n = Y /\ (less_eq_dom ((R_EAL f),(R_EAL (r - (1 / (n + 1)))))) ;
then Y /\ (less_dom (f,(R_EAL r))) = union (rng F) by MESFUNC1:21;
hence Y /\ (less_dom (f,r)) = union (rng F) ; ::_thesis: verum
end;
theorem :: MESFUNC6:11
for X being non empty set
for Y being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (great_dom (f,r)) = union (rng F)
proof
let X be non empty set ; ::_thesis: for Y being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (great_dom (f,r)) = union (rng F)
let Y be set ; ::_thesis: for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (great_dom (f,r)) = union (rng F)
let S be SigmaField of X; ::_thesis: for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (great_dom (f,r)) = union (rng F)
let F be Function of NAT,S; ::_thesis: for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (great_dom (f,r)) = union (rng F)
let f be PartFunc of X,REAL; ::_thesis: for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (great_dom (f,r)) = union (rng F)
let r be Real; ::_thesis: ( ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) implies Y /\ (great_dom (f,r)) = union (rng F) )
assume for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ; ::_thesis: Y /\ (great_dom (f,r)) = union (rng F)
then for n being Element of NAT holds F . n = Y /\ (great_eq_dom ((R_EAL f),(R_EAL (r + (1 / (n + 1)))))) ;
then Y /\ (great_dom (f,(R_EAL r))) = union (rng F) by MESFUNC1:22;
hence Y /\ (great_dom (f,r)) = union (rng F) ; ::_thesis: verum
end;
definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,REAL;
let A be Element of S;
predf is_measurable_on A means :Def1: :: MESFUNC6:def 1
R_EAL f is_measurable_on A;
end;
:: deftheorem Def1 defines is_measurable_on MESFUNC6:def_1_:_
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S holds
( f is_measurable_on A iff R_EAL f is_measurable_on A );
theorem Th12: :: MESFUNC6:12
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S holds
( f is_measurable_on A iff for r being real number holds A /\ (less_dom (f,r)) in S )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S holds
( f is_measurable_on A iff for r being real number holds A /\ (less_dom (f,r)) in S )
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for A being Element of S holds
( f is_measurable_on A iff for r being real number holds A /\ (less_dom (f,r)) in S )
let f be PartFunc of X,REAL; ::_thesis: for A being Element of S holds
( f is_measurable_on A iff for r being real number holds A /\ (less_dom (f,r)) in S )
let A be Element of S; ::_thesis: ( f is_measurable_on A iff for r being real number holds A /\ (less_dom (f,r)) in S )
A1: ( f is_measurable_on A iff R_EAL f is_measurable_on A ) by Def1;
thus ( f is_measurable_on A implies for r being real number holds A /\ (less_dom (f,r)) in S ) ::_thesis: ( ( for r being real number holds A /\ (less_dom (f,r)) in S ) implies f is_measurable_on A )
proof
assume A2: f is_measurable_on A ; ::_thesis: for r being real number holds A /\ (less_dom (f,r)) in S
let r be real number ; ::_thesis: A /\ (less_dom (f,r)) in S
R_EAL r = r ;
hence A /\ (less_dom (f,r)) in S by A1, A2, MESFUNC1:def_16; ::_thesis: verum
end;
( ( for r being real number holds A /\ (less_dom (f,(R_EAL r))) in S ) implies for r being real number holds A /\ (less_dom (f,(R_EAL r))) in S ) ;
hence ( ( for r being real number holds A /\ (less_dom (f,r)) in S ) implies f is_measurable_on A ) by A1, MESFUNC1:def_16; ::_thesis: verum
end;
theorem Th13: :: MESFUNC6:13
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st A c= dom f holds
( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,r)) in S )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st A c= dom f holds
( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,r)) in S )
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for A being Element of S st A c= dom f holds
( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,r)) in S )
let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st A c= dom f holds
( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,r)) in S )
let A be Element of S; ::_thesis: ( A c= dom f implies ( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,r)) in S ) )
assume A1: A c= dom f ; ::_thesis: ( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,r)) in S )
A2: ( f is_measurable_on A iff R_EAL f is_measurable_on A ) by Def1;
thus ( f is_measurable_on A implies for r being real number holds A /\ (great_eq_dom (f,r)) in S ) ::_thesis: ( ( for r being real number holds A /\ (great_eq_dom (f,r)) in S ) implies f is_measurable_on A )
proof
assume A3: f is_measurable_on A ; ::_thesis: for r being real number holds A /\ (great_eq_dom (f,r)) in S
let r be real number ; ::_thesis: A /\ (great_eq_dom (f,r)) in S
A /\ (great_eq_dom (f,(R_EAL r))) in S by A1, A2, A3, MESFUNC1:27;
hence A /\ (great_eq_dom (f,r)) in S ; ::_thesis: verum
end;
assume for r being real number holds A /\ (great_eq_dom (f,r)) in S ; ::_thesis: f is_measurable_on A
then for r being real number holds A /\ (great_eq_dom (f,(R_EAL r))) in S ;
hence f is_measurable_on A by A1, A2, MESFUNC1:27; ::_thesis: verum
end;
theorem :: MESFUNC6:14
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S holds
( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,r)) in S )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S holds
( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,r)) in S )
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for A being Element of S holds
( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,r)) in S )
let f be PartFunc of X,REAL; ::_thesis: for A being Element of S holds
( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,r)) in S )
let A be Element of S; ::_thesis: ( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,r)) in S )
A1: ( f is_measurable_on A iff R_EAL f is_measurable_on A ) by Def1;
thus ( f is_measurable_on A implies for r being real number holds A /\ (less_eq_dom (f,r)) in S ) ::_thesis: ( ( for r being real number holds A /\ (less_eq_dom (f,r)) in S ) implies f is_measurable_on A )
proof
assume A2: f is_measurable_on A ; ::_thesis: for r being real number holds A /\ (less_eq_dom (f,r)) in S
let r be real number ; ::_thesis: A /\ (less_eq_dom (f,r)) in S
R_EAL r = r ;
hence A /\ (less_eq_dom (f,r)) in S by A1, A2, MESFUNC1:28; ::_thesis: verum
end;
assume for r being real number holds A /\ (less_eq_dom (f,r)) in S ; ::_thesis: f is_measurable_on A
then for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S ;
hence f is_measurable_on A by A1, MESFUNC1:28; ::_thesis: verum
end;
theorem :: MESFUNC6:15
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st A c= dom f holds
( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,r)) in S )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st A c= dom f holds
( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,r)) in S )
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for A being Element of S st A c= dom f holds
( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,r)) in S )
let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st A c= dom f holds
( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,r)) in S )
let A be Element of S; ::_thesis: ( A c= dom f implies ( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,r)) in S ) )
assume A1: A c= dom f ; ::_thesis: ( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,r)) in S )
A2: ( f is_measurable_on A iff R_EAL f is_measurable_on A ) by Def1;
thus ( f is_measurable_on A implies for r being real number holds A /\ (great_dom (f,r)) in S ) ::_thesis: ( ( for r being real number holds A /\ (great_dom (f,r)) in S ) implies f is_measurable_on A )
proof
assume A3: f is_measurable_on A ; ::_thesis: for r being real number holds A /\ (great_dom (f,r)) in S
let r be real number ; ::_thesis: A /\ (great_dom (f,r)) in S
A /\ (great_dom (f,(R_EAL r))) in S by A1, A2, A3, MESFUNC1:29;
hence A /\ (great_dom (f,r)) in S ; ::_thesis: verum
end;
assume for r being real number holds A /\ (great_dom (f,r)) in S ; ::_thesis: f is_measurable_on A
then for r being real number holds A /\ (great_dom (f,(R_EAL r))) in S ;
hence f is_measurable_on A by A1, A2, MESFUNC1:29; ::_thesis: verum
end;
theorem :: MESFUNC6:16
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for B, A being Element of S st B c= A & f is_measurable_on A holds
f is_measurable_on B
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for B, A being Element of S st B c= A & f is_measurable_on A holds
f is_measurable_on B
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for B, A being Element of S st B c= A & f is_measurable_on A holds
f is_measurable_on B
let f be PartFunc of X,REAL; ::_thesis: for B, A being Element of S st B c= A & f is_measurable_on A holds
f is_measurable_on B
let B, A be Element of S; ::_thesis: ( B c= A & f is_measurable_on A implies f is_measurable_on B )
assume that
A1: B c= A and
A2: f is_measurable_on A ; ::_thesis: f is_measurable_on B
R_EAL f is_measurable_on A by A2, Def1;
then R_EAL f is_measurable_on B by A1, MESFUNC1:30;
hence f is_measurable_on B by Def1; ::_thesis: verum
end;
theorem :: MESFUNC6:17
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds
f is_measurable_on A \/ B
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds
f is_measurable_on A \/ B
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds
f is_measurable_on A \/ B
let f be PartFunc of X,REAL; ::_thesis: for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds
f is_measurable_on A \/ B
let A, B be Element of S; ::_thesis: ( f is_measurable_on A & f is_measurable_on B implies f is_measurable_on A \/ B )
assume ( f is_measurable_on A & f is_measurable_on B ) ; ::_thesis: f is_measurable_on A \/ B
then ( R_EAL f is_measurable_on A & R_EAL f is_measurable_on B ) by Def1;
then R_EAL f is_measurable_on A \/ B by MESFUNC1:31;
hence f is_measurable_on A \/ B by Def1; ::_thesis: verum
end;
theorem :: MESFUNC6:18
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S
for r, s being Real st f is_measurable_on A & A c= dom f holds
(A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S
for r, s being Real st f is_measurable_on A & A c= dom f holds
(A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for A being Element of S
for r, s being Real st f is_measurable_on A & A c= dom f holds
(A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S
let f be PartFunc of X,REAL; ::_thesis: for A being Element of S
for r, s being Real st f is_measurable_on A & A c= dom f holds
(A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S
let A be Element of S; ::_thesis: for r, s being Real st f is_measurable_on A & A c= dom f holds
(A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S
let r, s be Real; ::_thesis: ( f is_measurable_on A & A c= dom f implies (A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S )
A1: ( R_EAL r = r & R_EAL s = s ) ;
assume that
A2: f is_measurable_on A and
A3: A c= dom f ; ::_thesis: (A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S
R_EAL f is_measurable_on A by A2, Def1;
hence (A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S by A1, A3, MESFUNC1:32; ::_thesis: verum
end;
theorem :: MESFUNC6:19
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S
for r being Real st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
(A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S
for r being Real st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
(A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL
for A being Element of S
for r being Real st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
(A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S
let f, g be PartFunc of X,REAL; ::_thesis: for A being Element of S
for r being Real st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
(A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S
let A be Element of S; ::_thesis: for r being Real st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
(A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S
let r be Real; ::_thesis: ( f is_measurable_on A & g is_measurable_on A & A c= dom g implies (A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S )
assume that
A1: ( f is_measurable_on A & g is_measurable_on A ) and
A2: A c= dom g ; ::_thesis: (A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S
( R_EAL f is_measurable_on A & R_EAL g is_measurable_on A ) by A1, Def1;
then (A /\ (less_dom (f,(R_EAL r)))) /\ (great_dom (g,(R_EAL r))) in S by A2, MESFUNC1:36;
hence (A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S ; ::_thesis: verum
end;
theorem Th20: :: MESFUNC6:20
for X being non empty set
for f being PartFunc of X,REAL
for r being Real holds R_EAL (r (#) f) = r (#) (R_EAL f)
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for r being Real holds R_EAL (r (#) f) = r (#) (R_EAL f)
let f be PartFunc of X,REAL; ::_thesis: for r being Real holds R_EAL (r (#) f) = r (#) (R_EAL f)
let r be Real; ::_thesis: R_EAL (r (#) f) = r (#) (R_EAL f)
dom (R_EAL (r (#) f)) = dom (R_EAL f) by VALUED_1:def_5;
then A1: dom (R_EAL (r (#) f)) = dom (r (#) (R_EAL f)) by MESFUNC1:def_6;
now__::_thesis:_for_x_being_set_st_x_in_dom_(R_EAL_(r_(#)_f))_holds_
(R_EAL_(r_(#)_f))_._x_=_(r_(#)_(R_EAL_f))_._x
let x be set ; ::_thesis: ( x in dom (R_EAL (r (#) f)) implies (R_EAL (r (#) f)) . x = (r (#) (R_EAL f)) . x )
assume A2: x in dom (R_EAL (r (#) f)) ; ::_thesis: (R_EAL (r (#) f)) . x = (r (#) (R_EAL f)) . x
then (R_EAL (r (#) f)) . x = r * (f . x) by VALUED_1:def_5;
then (R_EAL (r (#) f)) . x = (R_EAL r) * (R_EAL (f . x)) by EXTREAL1:1;
hence (R_EAL (r (#) f)) . x = (r (#) (R_EAL f)) . x by A1, A2, MESFUNC1:def_6; ::_thesis: verum
end;
hence R_EAL (r (#) f) = r (#) (R_EAL f) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th21: :: MESFUNC6:21
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S
for r being Real st f is_measurable_on A & A c= dom f holds
r (#) f is_measurable_on A
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S
for r being Real st f is_measurable_on A & A c= dom f holds
r (#) f is_measurable_on A
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for A being Element of S
for r being Real st f is_measurable_on A & A c= dom f holds
r (#) f is_measurable_on A
let f be PartFunc of X,REAL; ::_thesis: for A being Element of S
for r being Real st f is_measurable_on A & A c= dom f holds
r (#) f is_measurable_on A
let A be Element of S; ::_thesis: for r being Real st f is_measurable_on A & A c= dom f holds
r (#) f is_measurable_on A
let r be Real; ::_thesis: ( f is_measurable_on A & A c= dom f implies r (#) f is_measurable_on A )
assume that
A1: f is_measurable_on A and
A2: A c= dom f ; ::_thesis: r (#) f is_measurable_on A
R_EAL f is_measurable_on A by A1, Def1;
then r (#) (R_EAL f) is_measurable_on A by A2, MESFUNC1:37;
then R_EAL (r (#) f) is_measurable_on A by Th20;
hence r (#) f is_measurable_on A by Def1; ::_thesis: verum
end;
begin
theorem :: MESFUNC6:22
for X being non empty set
for f being PartFunc of X,REAL holds R_EAL f is V68() ;
theorem Th23: :: MESFUNC6:23
for X being non empty set
for f, g being PartFunc of X,REAL holds
( R_EAL (f + g) = (R_EAL f) + (R_EAL g) & R_EAL (f - g) = (R_EAL f) - (R_EAL g) & dom (R_EAL (f + g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f - g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f + g)) = (dom f) /\ (dom g) & dom (R_EAL (f - g)) = (dom f) /\ (dom g) )
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL holds
( R_EAL (f + g) = (R_EAL f) + (R_EAL g) & R_EAL (f - g) = (R_EAL f) - (R_EAL g) & dom (R_EAL (f + g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f - g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f + g)) = (dom f) /\ (dom g) & dom (R_EAL (f - g)) = (dom f) /\ (dom g) )
let f, g be PartFunc of X,REAL; ::_thesis: ( R_EAL (f + g) = (R_EAL f) + (R_EAL g) & R_EAL (f - g) = (R_EAL f) - (R_EAL g) & dom (R_EAL (f + g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f - g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f + g)) = (dom f) /\ (dom g) & dom (R_EAL (f - g)) = (dom f) /\ (dom g) )
dom ((R_EAL f) - (R_EAL g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) by MESFUNC2:2;
then A1: dom ((R_EAL f) - (R_EAL g)) = dom (f - g) by VALUED_1:12;
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_((R_EAL_f)_-_(R_EAL_g))_holds_
((R_EAL_f)_-_(R_EAL_g))_._x_=_(f_-_g)_._x
let x be set ; ::_thesis: ( x in dom ((R_EAL f) - (R_EAL g)) implies ((R_EAL f) - (R_EAL g)) . x = (f - g) . x )
assume A3: x in dom ((R_EAL f) - (R_EAL g)) ; ::_thesis: ((R_EAL f) - (R_EAL g)) . x = (f - g) . x
then ((R_EAL f) - (R_EAL g)) . x = ((R_EAL f) . x) - ((R_EAL g) . x) by MESFUNC1:def_4
.= (f . x) - (g . x) by SUPINF_2:3 ;
hence ((R_EAL f) - (R_EAL g)) . x = (f - g) . x by A1, A3, VALUED_1:13; ::_thesis: verum
end;
dom ((R_EAL f) + (R_EAL g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) by MESFUNC2:2;
then A4: dom ((R_EAL f) + (R_EAL g)) = dom (f + g) by VALUED_1:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_((R_EAL_f)_+_(R_EAL_g))_holds_
((R_EAL_f)_+_(R_EAL_g))_._x_=_(f_+_g)_._x
let x be set ; ::_thesis: ( x in dom ((R_EAL f) + (R_EAL g)) implies ((R_EAL f) + (R_EAL g)) . x = (f + g) . x )
assume A5: x in dom ((R_EAL f) + (R_EAL g)) ; ::_thesis: ((R_EAL f) + (R_EAL g)) . x = (f + g) . x
then ((R_EAL f) + (R_EAL g)) . x = ((R_EAL f) . x) + ((R_EAL g) . x) by MESFUNC1:def_3
.= (f . x) + (g . x) by SUPINF_2:1 ;
hence ((R_EAL f) + (R_EAL g)) . x = (f + g) . x by A4, A5, VALUED_1:def_1; ::_thesis: verum
end;
hence ( R_EAL (f + g) = (R_EAL f) + (R_EAL g) & R_EAL (f - g) = (R_EAL f) - (R_EAL g) & dom (R_EAL (f + g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f - g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f + g)) = (dom f) /\ (dom g) & dom (R_EAL (f - g)) = (dom f) /\ (dom g) ) by A4, A1, A2, FUNCT_1:2, MESFUNC2:2; ::_thesis: verum
end;
theorem :: MESFUNC6:24
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S
for r being Real
for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S
for r being Real
for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL
for A being Element of S
for r being Real
for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let f, g be PartFunc of X,REAL; ::_thesis: for A being Element of S
for r being Real
for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let A be Element of S; ::_thesis: for r being Real
for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let r be Real; ::_thesis: for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let F be Function of RAT,S; ::_thesis: ( ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) implies A /\ (less_dom ((f + g),r)) = union (rng F) )
assume for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ; ::_thesis: A /\ (less_dom ((f + g),r)) = union (rng F)
then for p being Rational holds F . p = (A /\ (less_dom ((R_EAL f),(R_EAL p)))) /\ (A /\ (less_dom ((R_EAL g),(R_EAL (r - p))))) ;
then A1: A /\ (less_dom (((R_EAL f) + (R_EAL g)),(R_EAL r))) = union (rng F) by MESFUNC2:3;
(R_EAL f) + (R_EAL g) = R_EAL (f + g) by Th23;
hence A /\ (less_dom ((f + g),r)) = union (rng F) by A1; ::_thesis: verum
end;
theorem :: MESFUNC6:25
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S
for r being Real st f is_measurable_on A & g is_measurable_on A holds
ex F being Function of RAT,S st
for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S
for r being Real st f is_measurable_on A & g is_measurable_on A holds
ex F being Function of RAT,S st
for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL
for A being Element of S
for r being Real st f is_measurable_on A & g is_measurable_on A holds
ex F being Function of RAT,S st
for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
let f, g be PartFunc of X,REAL; ::_thesis: for A being Element of S
for r being Real st f is_measurable_on A & g is_measurable_on A holds
ex F being Function of RAT,S st
for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
let A be Element of S; ::_thesis: for r being Real st f is_measurable_on A & g is_measurable_on A holds
ex F being Function of RAT,S st
for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
let r be Real; ::_thesis: ( f is_measurable_on A & g is_measurable_on A implies ex F being Function of RAT,S st
for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) )
assume ( f is_measurable_on A & g is_measurable_on A ) ; ::_thesis: ex F being Function of RAT,S st
for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
then ( R_EAL f is_measurable_on A & R_EAL g is_measurable_on A ) by Def1;
then consider F being Function of RAT,S such that
A1: for p being Rational holds F . p = (A /\ (less_dom ((R_EAL f),(R_EAL p)))) /\ (A /\ (less_dom ((R_EAL g),(R_EAL (r - p))))) by MESFUNC2:6;
now__::_thesis:_for_p_being_Rational_holds_F_._p_=_(A_/\_(less_dom_(f,p)))_/\_(A_/\_(less_dom_(g,(r_-_p))))
let p be Rational; ::_thesis: F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
thus F . p = (A /\ (less_dom ((R_EAL f),(R_EAL p)))) /\ (A /\ (less_dom ((R_EAL g),(R_EAL (r - p))))) by A1
.= (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ; ::_thesis: verum
end;
hence ex F being Function of RAT,S st
for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ; ::_thesis: verum
end;
theorem Th26: :: MESFUNC6:26
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A & g is_measurable_on A holds
f + g is_measurable_on A
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A & g is_measurable_on A holds
f + g is_measurable_on A
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A & g is_measurable_on A holds
f + g is_measurable_on A
let f, g be PartFunc of X,REAL; ::_thesis: for A being Element of S st f is_measurable_on A & g is_measurable_on A holds
f + g is_measurable_on A
let A be Element of S; ::_thesis: ( f is_measurable_on A & g is_measurable_on A implies f + g is_measurable_on A )
assume ( f is_measurable_on A & g is_measurable_on A ) ; ::_thesis: f + g is_measurable_on A
then ( R_EAL f is_measurable_on A & R_EAL g is_measurable_on A ) by Def1;
then (R_EAL f) + (R_EAL g) is_measurable_on A by MESFUNC2:7;
then R_EAL (f + g) is_measurable_on A by Th23;
hence f + g is_measurable_on A by Def1; ::_thesis: verum
end;
theorem :: MESFUNC6:27
for X being non empty set
for f, g being PartFunc of X,REAL holds (R_EAL f) - (R_EAL g) = (R_EAL f) + (R_EAL (- g))
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL holds (R_EAL f) - (R_EAL g) = (R_EAL f) + (R_EAL (- g))
let f, g be PartFunc of X,REAL; ::_thesis: (R_EAL f) - (R_EAL g) = (R_EAL f) + (R_EAL (- g))
(R_EAL f) - (R_EAL g) = R_EAL (f - g) by Th23
.= R_EAL (f + (- g)) ;
hence (R_EAL f) - (R_EAL g) = (R_EAL f) + (R_EAL (- g)) by Th23; ::_thesis: verum
end;
theorem Th28: :: MESFUNC6:28
for X being non empty set
for f being PartFunc of X,REAL holds
( - (R_EAL f) = R_EAL ((- 1) (#) f) & - (R_EAL f) = R_EAL (- f) )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds
( - (R_EAL f) = R_EAL ((- 1) (#) f) & - (R_EAL f) = R_EAL (- f) )
let f be PartFunc of X,REAL; ::_thesis: ( - (R_EAL f) = R_EAL ((- 1) (#) f) & - (R_EAL f) = R_EAL (- f) )
- (R_EAL f) = (- 1) (#) (R_EAL f) by MESFUNC2:9;
hence ( - (R_EAL f) = R_EAL ((- 1) (#) f) & - (R_EAL f) = R_EAL (- f) ) by Th20; ::_thesis: verum
end;
theorem :: MESFUNC6:29
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
f - g is_measurable_on A
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
f - g is_measurable_on A
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
f - g is_measurable_on A
let f, g be PartFunc of X,REAL; ::_thesis: for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
f - g is_measurable_on A
let A be Element of S; ::_thesis: ( f is_measurable_on A & g is_measurable_on A & A c= dom g implies f - g is_measurable_on A )
assume that
A1: f is_measurable_on A and
A2: g is_measurable_on A and
A3: A c= dom g ; ::_thesis: f - g is_measurable_on A
R_EAL g is_measurable_on A by A2, Def1;
then (- 1) (#) (R_EAL g) is_measurable_on A by A3, MESFUNC1:37;
then - (R_EAL g) is_measurable_on A by MESFUNC2:9;
then A4: R_EAL (- g) is_measurable_on A by Th28;
R_EAL f is_measurable_on A by A1, Def1;
then (R_EAL f) + (R_EAL (- g)) is_measurable_on A by A4, MESFUNC2:7;
then R_EAL (f - g) is_measurable_on A by Th23;
hence f - g is_measurable_on A by Def1; ::_thesis: verum
end;
begin
theorem Th30: :: MESFUNC6:30
for X being non empty set
for f being PartFunc of X,REAL holds
( max+ (R_EAL f) = max+ f & max- (R_EAL f) = max- f )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds
( max+ (R_EAL f) = max+ f & max- (R_EAL f) = max- f )
let f be PartFunc of X,REAL; ::_thesis: ( max+ (R_EAL f) = max+ f & max- (R_EAL f) = max- f )
A1: dom (max+ (R_EAL f)) = dom (R_EAL f) by MESFUNC2:def_2
.= dom (max+ f) by RFUNCT_3:def_10 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_(max+_(R_EAL_f))_holds_
(max+_(R_EAL_f))_._x_=_(max+_f)_._x
let x be set ; ::_thesis: ( x in dom (max+ (R_EAL f)) implies (max+ (R_EAL f)) . x = (max+ f) . x )
assume A2: x in dom (max+ (R_EAL f)) ; ::_thesis: (max+ (R_EAL f)) . x = (max+ f) . x
then (max+ (R_EAL f)) . x = max+ (f . x) by MESFUNC2:def_2;
hence (max+ (R_EAL f)) . x = (max+ f) . x by A1, A2, RFUNCT_3:def_10; ::_thesis: verum
end;
hence max+ (R_EAL f) = max+ f by A1, FUNCT_1:2; ::_thesis: max- (R_EAL f) = max- f
A3: dom (max- (R_EAL f)) = dom (R_EAL f) by MESFUNC2:def_3
.= dom (max- f) by RFUNCT_3:def_11 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_(max-_(R_EAL_f))_holds_
(max-_(R_EAL_f))_._x_=_(max-_f)_._x
let x be set ; ::_thesis: ( x in dom (max- (R_EAL f)) implies (max- (R_EAL f)) . x = (max- f) . x )
assume A4: x in dom (max- (R_EAL f)) ; ::_thesis: (max- (R_EAL f)) . x = (max- f) . x
then (max- (R_EAL f)) . x = max ((- (R_EAL (f . x))),0.) by MESFUNC2:def_3;
then (max- (R_EAL f)) . x = max- (f . x) by SUPINF_2:2;
hence (max- (R_EAL f)) . x = (max- f) . x by A3, A4, RFUNCT_3:def_11; ::_thesis: verum
end;
hence max- (R_EAL f) = max- f by A3, FUNCT_1:2; ::_thesis: verum
end;
theorem :: MESFUNC6:31
for X being non empty set
for f being PartFunc of X,REAL
for x being Element of X holds 0 <= (max+ f) . x
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for x being Element of X holds 0 <= (max+ f) . x
let f be PartFunc of X,REAL; ::_thesis: for x being Element of X holds 0 <= (max+ f) . x
let x be Element of X; ::_thesis: 0 <= (max+ f) . x
0. <= (max+ (R_EAL f)) . x by MESFUNC2:12;
hence 0 <= (max+ f) . x by Th30; ::_thesis: verum
end;
theorem :: MESFUNC6:32
for X being non empty set
for f being PartFunc of X,REAL
for x being Element of X holds 0 <= (max- f) . x
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for x being Element of X holds 0 <= (max- f) . x
let f be PartFunc of X,REAL; ::_thesis: for x being Element of X holds 0 <= (max- f) . x
let x be Element of X; ::_thesis: 0 <= (max- f) . x
0. <= (max- (R_EAL f)) . x by MESFUNC2:13;
hence 0 <= (max- f) . x by Th30; ::_thesis: verum
end;
theorem :: MESFUNC6:33
for X being non empty set
for f being PartFunc of X,REAL holds max- f = max+ (- f)
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds max- f = max+ (- f)
let f be PartFunc of X,REAL; ::_thesis: max- f = max+ (- f)
max- f = max- (R_EAL f) by Th30;
then max- f = max+ (- (R_EAL f)) by MESFUNC2:14;
then max- f = max+ (R_EAL (- f)) by Th28;
hence max- f = max+ (- f) by Th30; ::_thesis: verum
end;
theorem :: MESFUNC6:34
for X being non empty set
for f being PartFunc of X,REAL
for x being set st x in dom f & 0 < (max+ f) . x holds
(max- f) . x = 0
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for x being set st x in dom f & 0 < (max+ f) . x holds
(max- f) . x = 0
let f be PartFunc of X,REAL; ::_thesis: for x being set st x in dom f & 0 < (max+ f) . x holds
(max- f) . x = 0
let x be set ; ::_thesis: ( x in dom f & 0 < (max+ f) . x implies (max- f) . x = 0 )
assume that
A1: x in dom f and
A2: 0 < (max+ f) . x ; ::_thesis: (max- f) . x = 0
0. < (max+ (R_EAL f)) . x by A2, Th30;
then (max- (R_EAL f)) . x = 0. by A1, MESFUNC2:15;
hence (max- f) . x = 0 by Th30; ::_thesis: verum
end;
theorem :: MESFUNC6:35
for X being non empty set
for f being PartFunc of X,REAL
for x being set st x in dom f & 0 < (max- f) . x holds
(max+ f) . x = 0
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for x being set st x in dom f & 0 < (max- f) . x holds
(max+ f) . x = 0
let f be PartFunc of X,REAL; ::_thesis: for x being set st x in dom f & 0 < (max- f) . x holds
(max+ f) . x = 0
let x be set ; ::_thesis: ( x in dom f & 0 < (max- f) . x implies (max+ f) . x = 0 )
assume that
A1: x in dom f and
A2: 0 < (max- f) . x ; ::_thesis: (max+ f) . x = 0
0. < (max- (R_EAL f)) . x by A2, Th30;
then (max+ (R_EAL f)) . x = 0. by A1, MESFUNC2:16;
hence (max+ f) . x = 0 by Th30; ::_thesis: verum
end;
theorem :: MESFUNC6:36
for X being non empty set
for f being PartFunc of X,REAL holds
( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds
( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) )
let f be PartFunc of X,REAL; ::_thesis: ( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) )
dom f = dom ((max+ (R_EAL f)) - (max- (R_EAL f))) by MESFUNC2:17;
then dom f = dom ((R_EAL (max+ f)) - (max- (R_EAL f))) by Th30;
then dom f = dom ((R_EAL (max+ f)) - (R_EAL (max- f))) by Th30;
then dom f = dom (R_EAL ((max+ f) - (max- f))) by Th23;
hence dom f = dom ((max+ f) - (max- f)) ; ::_thesis: dom f = dom ((max+ f) + (max- f))
dom f = dom ((max+ (R_EAL f)) + (max- (R_EAL f))) by MESFUNC2:17;
then dom f = dom ((R_EAL (max+ f)) + (max- (R_EAL f))) by Th30;
then dom f = dom ((R_EAL (max+ f)) + (R_EAL (max- f))) by Th30;
then dom f = dom (R_EAL ((max+ f) + (max- f))) by Th23;
hence dom f = dom ((max+ f) + (max- f)) ; ::_thesis: verum
end;
theorem :: MESFUNC6:37
for X being non empty set
for f being PartFunc of X,REAL
for x being set st x in dom f holds
( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for x being set st x in dom f holds
( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) )
let f be PartFunc of X,REAL; ::_thesis: for x being set st x in dom f holds
( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) )
let x be set ; ::_thesis: ( x in dom f implies ( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) ) )
A1: - ((R_EAL f) . x) = - (f . x) by SUPINF_2:2;
assume A2: x in dom f ; ::_thesis: ( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) )
then ( (max+ (R_EAL f)) . x = (R_EAL f) . x or (max+ (R_EAL f)) . x = 0. ) by MESFUNC2:18;
hence ( (max+ f) . x = f . x or (max+ f) . x = 0 ) by Th30; ::_thesis: ( (max- f) . x = - (f . x) or (max- f) . x = 0 )
( (max- (R_EAL f)) . x = - ((R_EAL f) . x) or (max- (R_EAL f)) . x = 0. ) by A2, MESFUNC2:18;
hence ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) by A1, Th30; ::_thesis: verum
end;
theorem :: MESFUNC6:38
for X being non empty set
for f being PartFunc of X,REAL
for x being set st x in dom f & (max+ f) . x = f . x holds
(max- f) . x = 0
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for x being set st x in dom f & (max+ f) . x = f . x holds
(max- f) . x = 0
let f be PartFunc of X,REAL; ::_thesis: for x being set st x in dom f & (max+ f) . x = f . x holds
(max- f) . x = 0
let x be set ; ::_thesis: ( x in dom f & (max+ f) . x = f . x implies (max- f) . x = 0 )
assume that
A1: x in dom f and
A2: (max+ f) . x = f . x ; ::_thesis: (max- f) . x = 0
R_EAL (f . x) = (max+ (R_EAL f)) . x by A2, Th30;
then (max- (R_EAL f)) . x = 0. by A1, MESFUNC2:19;
hence (max- f) . x = 0 by Th30; ::_thesis: verum
end;
theorem :: MESFUNC6:39
for X being non empty set
for f being PartFunc of X,REAL
for x being set st x in dom f & (max+ f) . x = 0 holds
(max- f) . x = - (f . x)
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for x being set st x in dom f & (max+ f) . x = 0 holds
(max- f) . x = - (f . x)
let f be PartFunc of X,REAL; ::_thesis: for x being set st x in dom f & (max+ f) . x = 0 holds
(max- f) . x = - (f . x)
let x be set ; ::_thesis: ( x in dom f & (max+ f) . x = 0 implies (max- f) . x = - (f . x) )
assume that
A1: x in dom f and
A2: (max+ f) . x = 0 ; ::_thesis: (max- f) . x = - (f . x)
R_EAL 0 = (max+ (R_EAL f)) . x by A2, Th30;
then (max- (R_EAL f)) . x = - ((R_EAL f) . x) by A1, MESFUNC2:20;
then (max- f) . x = - ((R_EAL f) . x) by Th30;
hence (max- f) . x = - (f . x) by SUPINF_2:2; ::_thesis: verum
end;
theorem :: MESFUNC6:40
for X being non empty set
for f being PartFunc of X,REAL
for x being set st x in dom f & (max- f) . x = - (f . x) holds
(max+ f) . x = 0
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for x being set st x in dom f & (max- f) . x = - (f . x) holds
(max+ f) . x = 0
let f be PartFunc of X,REAL; ::_thesis: for x being set st x in dom f & (max- f) . x = - (f . x) holds
(max+ f) . x = 0
let x be set ; ::_thesis: ( x in dom f & (max- f) . x = - (f . x) implies (max+ f) . x = 0 )
assume that
A1: x in dom f and
A2: (max- f) . x = - (f . x) ; ::_thesis: (max+ f) . x = 0
- (f . x) = (max- (R_EAL f)) . x by A2, Th30;
then - ((R_EAL f) . x) = (max- (R_EAL f)) . x by SUPINF_2:2;
then (max+ (R_EAL f)) . x = 0. by A1, MESFUNC2:21;
hence (max+ f) . x = 0 by Th30; ::_thesis: verum
end;
theorem :: MESFUNC6:41
for X being non empty set
for f being PartFunc of X,REAL
for x being set st x in dom f & (max- f) . x = 0 holds
(max+ f) . x = f . x
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for x being set st x in dom f & (max- f) . x = 0 holds
(max+ f) . x = f . x
let f be PartFunc of X,REAL; ::_thesis: for x being set st x in dom f & (max- f) . x = 0 holds
(max+ f) . x = f . x
let x be set ; ::_thesis: ( x in dom f & (max- f) . x = 0 implies (max+ f) . x = f . x )
assume that
A1: x in dom f and
A2: (max- f) . x = 0 ; ::_thesis: (max+ f) . x = f . x
R_EAL 0 = (max- (R_EAL f)) . x by A2, Th30;
then (max+ (R_EAL f)) . x = (R_EAL f) . x by A1, MESFUNC2:22;
hence (max+ f) . x = f . x by Th30; ::_thesis: verum
end;
theorem :: MESFUNC6:42
for X being non empty set
for f being PartFunc of X,REAL holds f = (max+ f) - (max- f)
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds f = (max+ f) - (max- f)
let f be PartFunc of X,REAL; ::_thesis: f = (max+ f) - (max- f)
f = (max+ (R_EAL f)) - (max- (R_EAL f)) by MESFUNC2:23;
then f = (R_EAL (max+ f)) - (max- (R_EAL f)) by Th30;
then f = (R_EAL (max+ f)) - (R_EAL (max- f)) by Th30;
then f = R_EAL ((max+ f) - (max- f)) by Th23;
hence f = (max+ f) - (max- f) ; ::_thesis: verum
end;
theorem Th43: :: MESFUNC6:43
for r being Real holds |.r.| = |.(R_EAL r).|
proof
let r be Real; ::_thesis: |.r.| = |.(R_EAL r).|
percases ( 0 <= r or r < 0 ) ;
supposeA1: 0 <= r ; ::_thesis: |.r.| = |.(R_EAL r).|
then |.(R_EAL r).| = R_EAL r by EXTREAL1:def_1;
hence |.r.| = |.(R_EAL r).| by A1, ABSVALUE:def_1; ::_thesis: verum
end;
supposeA2: r < 0 ; ::_thesis: |.r.| = |.(R_EAL r).|
then |.(R_EAL r).| = - (R_EAL r) by EXTREAL1:def_1;
then |.(R_EAL r).| = R_EAL (- r) by SUPINF_2:2;
hence |.r.| = |.(R_EAL r).| by A2, ABSVALUE:def_1; ::_thesis: verum
end;
end;
end;
theorem Th44: :: MESFUNC6:44
for X being non empty set
for f being PartFunc of X,REAL holds R_EAL (abs f) = |.(R_EAL f).|
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds R_EAL (abs f) = |.(R_EAL f).|
let f be PartFunc of X,REAL; ::_thesis: R_EAL (abs f) = |.(R_EAL f).|
A1: dom (R_EAL (abs f)) = dom f by VALUED_1:def_11
.= dom |.(R_EAL f).| by MESFUNC1:def_10 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_(R_EAL_(abs_f))_holds_
(R_EAL_(abs_f))_._x_=_|.(R_EAL_f).|_._x
let x be set ; ::_thesis: ( x in dom (R_EAL (abs f)) implies (R_EAL (abs f)) . x = |.(R_EAL f).| . x )
(R_EAL (abs f)) . x = |.(f . x).| by VALUED_1:18;
then A2: (R_EAL (abs f)) . x = |.(R_EAL (f . x)).| by Th43;
assume x in dom (R_EAL (abs f)) ; ::_thesis: (R_EAL (abs f)) . x = |.(R_EAL f).| . x
hence (R_EAL (abs f)) . x = |.(R_EAL f).| . x by A1, A2, MESFUNC1:def_10; ::_thesis: verum
end;
hence R_EAL (abs f) = |.(R_EAL f).| by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem :: MESFUNC6:45
for X being non empty set
for f being PartFunc of X,REAL holds abs f = (max+ f) + (max- f)
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds abs f = (max+ f) + (max- f)
let f be PartFunc of X,REAL; ::_thesis: abs f = (max+ f) + (max- f)
abs f = R_EAL (abs f) ;
then abs f = |.(R_EAL f).| by Th44;
then abs f = (max+ (R_EAL f)) + (max- (R_EAL f)) by MESFUNC2:24;
then abs f = (R_EAL (max+ f)) + (max- (R_EAL f)) by Th30;
then abs f = (R_EAL (max+ f)) + (R_EAL (max- f)) by Th30;
then abs f = R_EAL ((max+ f) + (max- f)) by Th23;
hence abs f = (max+ f) + (max- f) ; ::_thesis: verum
end;
begin
theorem Th46: :: MESFUNC6:46
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A holds
max+ f is_measurable_on A
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A holds
max+ f is_measurable_on A
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A holds
max+ f is_measurable_on A
let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st f is_measurable_on A holds
max+ f is_measurable_on A
let A be Element of S; ::_thesis: ( f is_measurable_on A implies max+ f is_measurable_on A )
assume f is_measurable_on A ; ::_thesis: max+ f is_measurable_on A
then R_EAL f is_measurable_on A by Def1;
then max+ (R_EAL f) is_measurable_on A by MESFUNC2:25;
then R_EAL (max+ f) is_measurable_on A by Th30;
hence max+ f is_measurable_on A by Def1; ::_thesis: verum
end;
theorem Th47: :: MESFUNC6:47
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A & A c= dom f holds
max- f is_measurable_on A
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A & A c= dom f holds
max- f is_measurable_on A
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A & A c= dom f holds
max- f is_measurable_on A
let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds
max- f is_measurable_on A
let A be Element of S; ::_thesis: ( f is_measurable_on A & A c= dom f implies max- f is_measurable_on A )
assume that
A1: f is_measurable_on A and
A2: A c= dom f ; ::_thesis: max- f is_measurable_on A
R_EAL f is_measurable_on A by A1, Def1;
then max- (R_EAL f) is_measurable_on A by A2, MESFUNC2:26;
then R_EAL (max- f) is_measurable_on A by Th30;
hence max- f is_measurable_on A by Def1; ::_thesis: verum
end;
theorem :: MESFUNC6:48
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A & A c= dom f holds
abs f is_measurable_on A
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A & A c= dom f holds
abs f is_measurable_on A
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A & A c= dom f holds
abs f is_measurable_on A
let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds
abs f is_measurable_on A
let A be Element of S; ::_thesis: ( f is_measurable_on A & A c= dom f implies abs f is_measurable_on A )
assume that
A1: f is_measurable_on A and
A2: A c= dom f ; ::_thesis: abs f is_measurable_on A
R_EAL f is_measurable_on A by A1, Def1;
then |.(R_EAL f).| is_measurable_on A by A2, MESFUNC2:27;
then R_EAL (abs f) is_measurable_on A by Th44;
hence abs f is_measurable_on A by Def1; ::_thesis: verum
end;
begin
definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,REAL;
predf is_simple_func_in S means :Def2: :: MESFUNC6:def 2
ex F being Finite_Sep_Sequence of S st
( dom f = union (rng F) & ( 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 ) );
end;
:: deftheorem Def2 defines is_simple_func_in MESFUNC6:def_2_:_
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL holds
( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S st
( dom f = union (rng F) & ( 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 ) ) );
theorem Th49: :: MESFUNC6:49
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL holds
( f is_simple_func_in S iff R_EAL f is_simple_func_in S )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL holds
( f is_simple_func_in S iff R_EAL f is_simple_func_in S )
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL holds
( f is_simple_func_in S iff R_EAL f is_simple_func_in S )
let f be PartFunc of X,REAL; ::_thesis: ( f is_simple_func_in S iff R_EAL f is_simple_func_in S )
hereby ::_thesis: ( R_EAL f is_simple_func_in S implies f is_simple_func_in S )
assume f is_simple_func_in S ; ::_thesis: R_EAL f is_simple_func_in S
then ex F being Finite_Sep_Sequence of S st
( dom f = union (rng F) & ( 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 Def2;
hence R_EAL f is_simple_func_in S by MESFUNC2:def_4; ::_thesis: verum
end;
assume R_EAL f is_simple_func_in S ; ::_thesis: f is_simple_func_in S
then ex F being Finite_Sep_Sequence of S st
( dom (R_EAL f) = union (rng F) & ( 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
(R_EAL f) . x = (R_EAL f) . y ) ) by MESFUNC2:def_4;
hence f is_simple_func_in S by Def2; ::_thesis: verum
end;
theorem :: MESFUNC6:50
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
let A be Element of S; ::_thesis: ( f is_simple_func_in S implies f is_measurable_on A )
assume f is_simple_func_in S ; ::_thesis: f is_measurable_on A
then R_EAL f is_simple_func_in S by Th49;
then R_EAL f is_measurable_on A by MESFUNC2:34;
hence f is_measurable_on A by Def1; ::_thesis: verum
end;
theorem Th51: :: MESFUNC6:51
for X being set
for f being PartFunc of X,REAL holds
( f is nonnegative iff for x being set holds 0 <= f . x )
proof
let X be set ; ::_thesis: for f being PartFunc of X,REAL holds
( f is nonnegative iff for x being set holds 0 <= f . x )
let f be PartFunc of X,REAL; ::_thesis: ( f is nonnegative iff for x being set holds 0 <= f . x )
hereby ::_thesis: ( ( for x being set holds 0 <= f . x ) implies f is nonnegative )
assume f is nonnegative ; ::_thesis: for x being set holds 0 <= f . x
then A1: rng f is nonnegative by SUPINF_2:def_16;
hereby ::_thesis: verum
let x be set ; ::_thesis: 0 <= f . x
now__::_thesis:_(_x_in_dom_f_implies_0_<=_f_._x_)
assume x in dom f ; ::_thesis: 0 <= f . x
then A2: f . x in rng f by FUNCT_1:def_3;
f . x in REAL ;
hence 0 <= f . x by A1, A2, NUMBERS:31, SUPINF_2:def_9; ::_thesis: verum
end;
hence 0 <= f . x by FUNCT_1:def_2; ::_thesis: verum
end;
end;
assume A3: for x being set holds 0 <= f . x ; ::_thesis: f is nonnegative
let y be R_eal; :: according to SUPINF_2:def_9,SUPINF_2:def_16 ::_thesis: ( not y in rng f or 0. <= y )
assume y in rng f ; ::_thesis: 0. <= y
then ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def_3;
hence 0. <= y by A3; ::_thesis: verum
end;
theorem Th52: :: MESFUNC6:52
for X being set
for f being PartFunc of X,REAL st ( for x being set st x in dom f holds
0 <= f . x ) holds
f is nonnegative
proof
let X be set ; ::_thesis: for f being PartFunc of X,REAL st ( for x being set st x in dom f holds
0 <= f . x ) holds
f is nonnegative
let f be PartFunc of X,REAL; ::_thesis: ( ( for x being set st x in dom f holds
0 <= f . x ) implies f is nonnegative )
assume A1: for x being set st x in dom f holds
0 <= f . x ; ::_thesis: f is nonnegative
let y be R_eal; :: according to SUPINF_2:def_9,SUPINF_2:def_16 ::_thesis: ( not y in rng f or 0. <= y )
assume y in rng f ; ::_thesis: 0. <= y
then ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def_3;
hence 0. <= y by A1; ::_thesis: verum
end;
theorem :: MESFUNC6:53
for X being set
for f being PartFunc of X,REAL holds
( f is nonpositive iff for x being set holds f . x <= 0 )
proof
let X be set ; ::_thesis: for f being PartFunc of X,REAL holds
( f is nonpositive iff for x being set holds f . x <= 0 )
let f be PartFunc of X,REAL; ::_thesis: ( f is nonpositive iff for x being set holds f . x <= 0 )
hereby ::_thesis: ( ( for x being set holds f . x <= 0 ) implies f is nonpositive )
assume f is nonpositive ; ::_thesis: for x being set holds f . x <= 0
then A1: rng f is nonpositive by MESFUNC5:def_2;
hereby ::_thesis: verum
let x be set ; ::_thesis: f . x <= 0
now__::_thesis:_(_x_in_dom_f_implies_f_._x_<=_0_)
assume x in dom f ; ::_thesis: f . x <= 0
then A2: f . x in rng f by FUNCT_1:def_3;
f . x in REAL ;
hence f . x <= 0 by A1, A2, MESFUNC5:def_1, NUMBERS:31; ::_thesis: verum
end;
hence f . x <= 0 by FUNCT_1:def_2; ::_thesis: verum
end;
end;
assume A3: for x being set holds f . x <= 0 ; ::_thesis: f is nonpositive
let y be R_eal; :: according to MESFUNC5:def_1,MESFUNC5:def_2 ::_thesis: ( not y in rng f or y <= 0 )
assume y in rng f ; ::_thesis: y <= 0
then ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def_3;
hence y <= 0 by A3; ::_thesis: verum
end;
theorem Th54: :: MESFUNC6:54
for X being non empty set
for f being PartFunc of X,REAL st ( for x being set st x in dom f holds
f . x <= 0 ) holds
f is nonpositive
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL st ( for x being set st x in dom f holds
f . x <= 0 ) holds
f is nonpositive
let f be PartFunc of X,REAL; ::_thesis: ( ( for x being set st x in dom f holds
f . x <= 0 ) implies f is nonpositive )
assume A1: for x being set st x in dom f holds
f . x <= 0 ; ::_thesis: f is nonpositive
let y be R_eal; :: according to MESFUNC5:def_1,MESFUNC5:def_2 ::_thesis: ( not y in rng f or y <= 0 )
assume y in rng f ; ::_thesis: y <= 0
then ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def_3;
hence y <= 0 by A1; ::_thesis: verum
end;
theorem :: MESFUNC6:55
for X being non empty set
for Y being set
for f being PartFunc of X,REAL st f is nonnegative holds
f | Y is nonnegative
proof
let X be non empty set ; ::_thesis: for Y being set
for f being PartFunc of X,REAL st f is nonnegative holds
f | Y is nonnegative
let Y be set ; ::_thesis: for f being PartFunc of X,REAL st f is nonnegative holds
f | Y is nonnegative
let f be PartFunc of X,REAL; ::_thesis: ( f is nonnegative implies f | Y is nonnegative )
assume f is nonnegative ; ::_thesis: f | Y is nonnegative
then A1: rng f is nonnegative by SUPINF_2:def_16;
now__::_thesis:_for_y_being_R_eal_st_y_in_rng_(f_|_Y)_holds_
0._<=_y
let y be R_eal; ::_thesis: ( y in rng (f | Y) implies 0. <= y )
assume y in rng (f | Y) ; ::_thesis: 0. <= y
then consider x being set such that
A2: x in dom (f | Y) and
A3: (f | Y) . x = y by FUNCT_1:def_3;
x in (dom f) /\ Y by A2, RELAT_1:61;
then A4: x in dom f by XBOOLE_0:def_4;
(f | Y) . x = f . x by A2, FUNCT_1:47;
then (f | Y) . x in rng f by A4, FUNCT_1:3;
hence 0. <= y by A1, A3, SUPINF_2:def_9; ::_thesis: verum
end;
then rng (f | Y) is nonnegative by SUPINF_2:def_9;
hence f | Y is nonnegative by SUPINF_2:def_16; ::_thesis: verum
end;
theorem Th56: :: MESFUNC6:56
for X being non empty set
for f, g being PartFunc of X,REAL st f is nonnegative & g is nonnegative holds
f + g is nonnegative
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL st f is nonnegative & g is nonnegative holds
f + g is nonnegative
let f, g be PartFunc of X,REAL; ::_thesis: ( f is nonnegative & g is nonnegative implies f + g is nonnegative )
assume that
A1: f is nonnegative and
A2: g is nonnegative ; ::_thesis: f + g is nonnegative
for x being set st x in dom (f + g) holds
0 <= (f + g) . x
proof
let x be set ; ::_thesis: ( x in dom (f + g) implies 0 <= (f + g) . x )
assume A3: x in dom (f + g) ; ::_thesis: 0 <= (f + g) . x
0 <= f . x by A1, Th51;
then A4: g . x <= (f . x) + (g . x) by XREAL_1:31;
0 <= g . x by A2, Th51;
hence 0 <= (f + g) . x by A3, A4, VALUED_1:def_1; ::_thesis: verum
end;
hence f + g is nonnegative by Th52; ::_thesis: verum
end;
theorem :: MESFUNC6:57
for X being non empty set
for f being PartFunc of X,REAL
for r being Real st f is nonnegative holds
( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for r being Real st f is nonnegative holds
( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) )
let f be PartFunc of X,REAL; ::_thesis: for r being Real st f is nonnegative holds
( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) )
let r be Real; ::_thesis: ( f is nonnegative implies ( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) ) )
assume A1: f is nonnegative ; ::_thesis: ( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) )
hereby ::_thesis: ( r <= 0 implies r (#) f is nonpositive )
assume A2: 0 <= r ; ::_thesis: r (#) f is nonnegative
now__::_thesis:_for_x_being_set_st_x_in_dom_(r_(#)_f)_holds_
0_<=_(r_(#)_f)_._x
let x be set ; ::_thesis: ( x in dom (r (#) f) implies 0 <= (r (#) f) . x )
assume A3: x in dom (r (#) f) ; ::_thesis: 0 <= (r (#) f) . x
0 <= f . x by A1, Th51;
then 0 * r <= r * (f . x) by A2;
hence 0 <= (r (#) f) . x by A3, VALUED_1:def_5; ::_thesis: verum
end;
hence r (#) f is nonnegative by Th52; ::_thesis: verum
end;
assume A4: r <= 0 ; ::_thesis: r (#) f is nonpositive
now__::_thesis:_for_x_being_set_st_x_in_dom_(r_(#)_f)_holds_
(r_(#)_f)_._x_<=_0
let x be set ; ::_thesis: ( x in dom (r (#) f) implies (r (#) f) . x <= 0 )
assume A5: x in dom (r (#) f) ; ::_thesis: (r (#) f) . x <= 0
0 <= f . x by A1, Th51;
then r * (f . x) <= r * 0 by A4;
hence (r (#) f) . x <= 0 by A5, VALUED_1:def_5; ::_thesis: verum
end;
hence r (#) f is nonpositive by Th54; ::_thesis: verum
end;
theorem Th58: :: MESFUNC6:58
for X being non empty set
for f, g being PartFunc of X,REAL st ( for x being set st x in (dom f) /\ (dom g) holds
g . x <= f . x ) holds
f - g is nonnegative
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL st ( for x being set st x in (dom f) /\ (dom g) holds
g . x <= f . x ) holds
f - g is nonnegative
let f, g be PartFunc of X,REAL; ::_thesis: ( ( for x being set st x in (dom f) /\ (dom g) holds
g . x <= f . x ) implies f - g is nonnegative )
assume A1: for x being set st x in (dom f) /\ (dom g) holds
g . x <= f . x ; ::_thesis: f - g is nonnegative
now__::_thesis:_for_x_being_set_st_x_in_dom_(f_-_g)_holds_
0_<=_(f_-_g)_._x
let x be set ; ::_thesis: ( x in dom (f - g) implies 0 <= (f - g) . x )
assume A2: x in dom (f - g) ; ::_thesis: 0 <= (f - g) . x
dom (f - g) = (dom f) /\ (dom g) by VALUED_1:12;
then 0 <= (f . x) - (g . x) by A1, A2, XREAL_1:48;
hence 0 <= (f - g) . x by A2, VALUED_1:13; ::_thesis: verum
end;
hence f - g is nonnegative by Th52; ::_thesis: verum
end;
theorem :: MESFUNC6:59
for X being non empty set
for f, g, h being PartFunc of X,REAL st f is nonnegative & g is nonnegative & h is nonnegative holds
(f + g) + h is nonnegative
proof
let X be non empty set ; ::_thesis: for f, g, h being PartFunc of X,REAL st f is nonnegative & g is nonnegative & h is nonnegative holds
(f + g) + h is nonnegative
let f, g, h be PartFunc of X,REAL; ::_thesis: ( f is nonnegative & g is nonnegative & h is nonnegative implies (f + g) + h is nonnegative )
assume that
A1: ( f is nonnegative & g is nonnegative ) and
A2: h is nonnegative ; ::_thesis: (f + g) + h is nonnegative
f + g is nonnegative by A1, Th56;
hence (f + g) + h is nonnegative by A2, Th56; ::_thesis: verum
end;
theorem Th60: :: MESFUNC6:60
for X being non empty set
for f, g, h being PartFunc of X,REAL
for x being set st x in dom ((f + g) + h) holds
((f + g) + h) . x = ((f . x) + (g . x)) + (h . x)
proof
let X be non empty set ; ::_thesis: for f, g, h being PartFunc of X,REAL
for x being set st x in dom ((f + g) + h) holds
((f + g) + h) . x = ((f . x) + (g . x)) + (h . x)
let f, g, h be PartFunc of X,REAL; ::_thesis: for x being set st x in dom ((f + g) + h) holds
((f + g) + h) . x = ((f . x) + (g . x)) + (h . x)
let x be set ; ::_thesis: ( x in dom ((f + g) + h) implies ((f + g) + h) . x = ((f . x) + (g . x)) + (h . x) )
assume A1: x in dom ((f + g) + h) ; ::_thesis: ((f + g) + h) . x = ((f . x) + (g . x)) + (h . x)
dom ((f + g) + h) = (dom (f + g)) /\ (dom h) by VALUED_1:def_1;
then x in dom (f + g) by A1, XBOOLE_0:def_4;
then ((f . x) + (g . x)) + (h . x) = ((f + g) . x) + (h . x) by VALUED_1:def_1;
hence ((f + g) + h) . x = ((f . x) + (g . x)) + (h . x) by A1, VALUED_1:def_1; ::_thesis: verum
end;
theorem :: MESFUNC6:61
for X being non empty set
for f being PartFunc of X,REAL holds
( max+ f is nonnegative & max- f is nonnegative )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds
( max+ f is nonnegative & max- f is nonnegative )
let f be PartFunc of X,REAL; ::_thesis: ( max+ f is nonnegative & max- f is nonnegative )
for x being set st x in dom (max+ f) holds
0 <= (max+ f) . x by RFUNCT_3:37;
hence max+ f is nonnegative by Th52; ::_thesis: max- f is nonnegative
for x being set st x in dom (max- f) holds
0 <= (max- f) . x by RFUNCT_3:40;
hence max- f is nonnegative by Th52; ::_thesis: verum
end;
theorem Th62: :: MESFUNC6:62
for X being non empty set
for f, g being PartFunc of X,REAL holds
( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) & dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL holds
( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) & dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )
let f, g be PartFunc of X,REAL; ::_thesis: ( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) & dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )
A1: ( dom (max- f) = dom f & dom ((max+ (f + g)) + (max- f)) = (dom (max+ (f + g))) /\ (dom (max- f)) ) by RFUNCT_3:def_11, VALUED_1:def_1;
A2: ( dom (max+ f) = dom f & dom ((max- (f + g)) + (max+ f)) = (dom (max- (f + g))) /\ (dom (max+ f)) ) by RFUNCT_3:def_10, VALUED_1:def_1;
A3: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1;
then A4: dom (max- (f + g)) = (dom f) /\ (dom g) by RFUNCT_3:def_11;
dom (max+ (f + g)) = (dom f) /\ (dom g) by A3, RFUNCT_3:def_10;
then A5: dom ((max+ (f + g)) + (max- f)) = (dom g) /\ ((dom f) /\ (dom f)) by A1, XBOOLE_1:16;
hence ( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) ) by A4, A2, XBOOLE_1:16; ::_thesis: ( dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )
dom (max- g) = dom g by RFUNCT_3:def_11;
then dom (((max+ (f + g)) + (max- f)) + (max- g)) = ((dom f) /\ (dom g)) /\ (dom g) by A5, VALUED_1:def_1
.= (dom f) /\ ((dom g) /\ (dom g)) by XBOOLE_1:16 ;
hence dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) ; ::_thesis: ( dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )
( dom (max+ g) = dom g & dom ((max- (f + g)) + (max+ f)) = (dom g) /\ ((dom f) /\ (dom f)) ) by A4, A2, RFUNCT_3:def_10, XBOOLE_1:16;
then dom (((max- (f + g)) + (max+ f)) + (max+ g)) = ((dom f) /\ (dom g)) /\ (dom g) by VALUED_1:def_1;
then dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ ((dom g) /\ (dom g)) by XBOOLE_1:16;
hence dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) ; ::_thesis: ( (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )
now__::_thesis:_for_x_being_set_st_x_in_dom_((max+_(f_+_g))_+_(max-_f))_holds_
0_<=_((max+_(f_+_g))_+_(max-_f))_._x
let x be set ; ::_thesis: ( x in dom ((max+ (f + g)) + (max- f)) implies 0 <= ((max+ (f + g)) + (max- f)) . x )
assume A6: x in dom ((max+ (f + g)) + (max- f)) ; ::_thesis: 0 <= ((max+ (f + g)) + (max- f)) . x
then ( 0 <= (max+ (f + g)) . x & 0 <= (max- f) . x ) by RFUNCT_3:37, RFUNCT_3:40;
then 0 + 0 <= ((max+ (f + g)) . x) + ((max- f) . x) ;
hence 0 <= ((max+ (f + g)) + (max- f)) . x by A6, VALUED_1:def_1; ::_thesis: verum
end;
hence (max+ (f + g)) + (max- f) is nonnegative by Th52; ::_thesis: (max- (f + g)) + (max+ f) is nonnegative
now__::_thesis:_for_x_being_set_st_x_in_dom_((max-_(f_+_g))_+_(max+_f))_holds_
0_<=_((max-_(f_+_g))_+_(max+_f))_._x
let x be set ; ::_thesis: ( x in dom ((max- (f + g)) + (max+ f)) implies 0 <= ((max- (f + g)) + (max+ f)) . x )
assume A7: x in dom ((max- (f + g)) + (max+ f)) ; ::_thesis: 0 <= ((max- (f + g)) + (max+ f)) . x
then ( 0 <= (max- (f + g)) . x & 0 <= (max+ f) . x ) by RFUNCT_3:37, RFUNCT_3:40;
then 0 + 0 <= ((max- (f + g)) . x) + ((max+ f) . x) ;
hence 0 <= ((max- (f + g)) + (max+ f)) . x by A7, VALUED_1:def_1; ::_thesis: verum
end;
hence (max- (f + g)) + (max+ f) is nonnegative by Th52; ::_thesis: verum
end;
theorem :: MESFUNC6:63
for X being non empty set
for f, g being PartFunc of X,REAL holds ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL holds ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)
let f, g be PartFunc of X,REAL; ::_thesis: ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)
A1: dom (max+ (f + g)) = dom (f + g) by RFUNCT_3:def_10;
A2: dom (max+ g) = dom g by RFUNCT_3:def_10;
A3: dom (max+ f) = dom f by RFUNCT_3:def_10;
A4: dom (max- f) = dom f by RFUNCT_3:def_11;
A5: dom (max- g) = dom g by RFUNCT_3:def_11;
A6: dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom ((max+ (f + g)) + (max- f))) /\ (dom (max- g)) by VALUED_1:def_1
.= ((dom (f + g)) /\ (dom f)) /\ (dom g) by A1, A4, A5, VALUED_1:def_1 ;
then A7: dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom (f + g)) /\ ((dom f) /\ (dom g)) by XBOOLE_1:16;
A8: dom (max- (f + g)) = dom (f + g) by RFUNCT_3:def_11;
A9: for x being set st x in dom (((max+ (f + g)) + (max- f)) + (max- g)) holds
(((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x
proof
let x be set ; ::_thesis: ( x in dom (((max+ (f + g)) + (max- f)) + (max- g)) implies (((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x )
assume A10: x in dom (((max+ (f + g)) + (max- f)) + (max- g)) ; ::_thesis: (((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x
then A11: x in dom g by A6, XBOOLE_0:def_4;
then A12: (max+ g) . x = max+ (g . x) by A2, RFUNCT_3:def_10;
A13: (max- g) . x = max- (g . x) by A5, A11, RFUNCT_3:def_11;
A14: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1;
then A15: (max+ (f + g)) . x = max+ ((f + g) . x) by A1, A7, A10, RFUNCT_3:def_10
.= max (((f . x) + (g . x)),0) by A7, A10, A14, VALUED_1:def_1 ;
A16: x in dom f by A7, A10, A14, XBOOLE_0:def_4;
then A17: (max+ f) . x = max+ (f . x) by A3, RFUNCT_3:def_10;
A18: (max- (f + g)) . x = max- ((f + g) . x) by A8, A7, A10, A14, RFUNCT_3:def_11
.= max ((- ((f . x) + (g . x))),0) by A7, A10, A14, VALUED_1:def_1 ;
A19: (max- f) . x = max- (f . x) by A4, A16, RFUNCT_3:def_11;
A20: now__::_thesis:_(_0_<=_f_._x_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_)
assume A21: 0 <= f . x ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then A22: (max- f) . x = 0 by A19, XXREAL_0:def_10;
A23: now__::_thesis:_(_g_._x_<_0_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_)
assume A24: g . x < 0 ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then A25: (max- g) . x = - (g . x) by A13, XXREAL_0:def_10;
A26: (max+ g) . x = 0 by A12, A24, XXREAL_0:def_10;
A27: now__::_thesis:_(_(f_._x)_+_(g_._x)_<_0_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_)
assume A28: (f . x) + (g . x) < 0 ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then (max- (f + g)) . x = - ((f . x) + (g . x)) by A18, XXREAL_0:def_10;
then (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + (f . x)) + 0 by A17, A21, A26, XXREAL_0:def_10;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A15, A22, A25, A28, XXREAL_0:def_10; ::_thesis: verum
end;
now__::_thesis:_(_0_<=_(f_._x)_+_(g_._x)_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_)
assume 0 <= (f . x) + (g . x) ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then ( (max- (f + g)) . x = 0 & (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((f . x) + (g . x)) + 0) + (- (g . x)) ) by A15, A18, A22, A25, XXREAL_0:def_10;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A17, A21, A26, XXREAL_0:def_10; ::_thesis: verum
end;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A27; ::_thesis: verum
end;
now__::_thesis:_(_0_<=_g_._x_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_)
assume A29: 0 <= g . x ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then (max- g) . x = 0 by A13, XXREAL_0:def_10;
then A30: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (f . x) + (g . x) by A15, A21, A22, A29, XXREAL_0:def_10;
( (max- (f + g)) . x = 0 & (max+ g) . x = g . x ) by A18, A12, A21, A29, XXREAL_0:def_10;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A17, A21, A30, XXREAL_0:def_10; ::_thesis: verum
end;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A23; ::_thesis: verum
end;
A31: now__::_thesis:_(_f_._x_<_0_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_)
assume A32: f . x < 0 ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then A33: (max- f) . x = - (f . x) by A19, XXREAL_0:def_10;
A34: now__::_thesis:_(_0_<=_g_._x_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_)
assume A35: 0 <= g . x ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then A36: (max- g) . x = 0 by A13, XXREAL_0:def_10;
A37: (max+ g) . x = g . x by A12, A35, XXREAL_0:def_10;
A38: now__::_thesis:_(_(f_._x)_+_(g_._x)_<_0_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_)
assume A39: (f . x) + (g . x) < 0 ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then (max- (f + g)) . x = - ((f . x) + (g . x)) by A18, XXREAL_0:def_10;
then (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + 0) + (g . x) by A17, A32, A37, XXREAL_0:def_10
.= (- (f . x)) + ((- (g . x)) + (g . x)) ;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A15, A33, A36, A39, XXREAL_0:def_10; ::_thesis: verum
end;
now__::_thesis:_(_0_<=_(f_._x)_+_(g_._x)_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_)
assume 0 <= (f . x) + (g . x) ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then ( (max- (f + g)) . x = 0 & (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((f . x) + (g . x)) + (- (f . x))) + 0 ) by A15, A18, A33, A36, XXREAL_0:def_10;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A17, A32, A37, XXREAL_0:def_10; ::_thesis: verum
end;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A38; ::_thesis: verum
end;
now__::_thesis:_(_g_._x_<_0_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_)
assume A40: g . x < 0 ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then ( (max- (f + g)) . x = - ((f . x) + (g . x)) & (max+ g) . x = 0 ) by A18, A12, A32, XXREAL_0:def_10;
then A41: (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + 0) + 0 by A17, A32, XXREAL_0:def_10;
(max- g) . x = - (g . x) by A13, A40, XXREAL_0:def_10;
then (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (0 + (- (f . x))) + (- (g . x)) by A15, A32, A33, A40, XXREAL_0:def_10;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A41; ::_thesis: verum
end;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A34; ::_thesis: verum
end;
x in (dom f) /\ (dom g) by A10, Th62;
then x in dom (((max- (f + g)) + (max+ f)) + (max+ g)) by Th62;
then (((max- (f + g)) + (max+ f)) + (max+ g)) . x = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by Th60;
hence (((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x by A10, A20, A31, Th60; ::_thesis: verum
end;
dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) by Th62;
then dom (((max+ (f + g)) + (max- f)) + (max- g)) = dom (((max- (f + g)) + (max+ f)) + (max+ g)) by Th62;
hence ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g) by A9, FUNCT_1:2; ::_thesis: verum
end;
theorem :: MESFUNC6:64
for X being non empty set
for f being PartFunc of X,REAL
for r being Real st 0 <= r holds
( max+ (r (#) f) = r (#) (max+ f) & max- (r (#) f) = r (#) (max- f) )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for r being Real st 0 <= r holds
( max+ (r (#) f) = r (#) (max+ f) & max- (r (#) f) = r (#) (max- f) )
let f be PartFunc of X,REAL; ::_thesis: for r being Real st 0 <= r holds
( max+ (r (#) f) = r (#) (max+ f) & max- (r (#) f) = r (#) (max- f) )
let r be Real; ::_thesis: ( 0 <= r implies ( max+ (r (#) f) = r (#) (max+ f) & max- (r (#) f) = r (#) (max- f) ) )
assume A1: 0 <= r ; ::_thesis: ( max+ (r (#) f) = r (#) (max+ f) & max- (r (#) f) = r (#) (max- f) )
A2: dom (max+ (r (#) f)) = dom (r (#) f) by RFUNCT_3:def_10
.= dom f by VALUED_1:def_5
.= dom (max+ f) by RFUNCT_3:def_10
.= dom (r (#) (max+ f)) by VALUED_1:def_5 ;
for x being Element of X st x in dom (max+ (r (#) f)) holds
(max+ (r (#) f)) . x = (r (#) (max+ f)) . x
proof
let x be Element of X; ::_thesis: ( x in dom (max+ (r (#) f)) implies (max+ (r (#) f)) . x = (r (#) (max+ f)) . x )
assume A3: x in dom (max+ (r (#) f)) ; ::_thesis: (max+ (r (#) f)) . x = (r (#) (max+ f)) . x
then A4: x in dom (r (#) f) by RFUNCT_3:def_10;
then x in dom f by VALUED_1:def_5;
then A5: x in dom (max+ f) by RFUNCT_3:def_10;
A6: (max+ (r (#) f)) . x = max+ ((r (#) f) . x) by A3, RFUNCT_3:def_10
.= max ((r * (f . x)),0) by A4, VALUED_1:def_5 ;
(r (#) (max+ f)) . x = r * ((max+ f) . x) by A2, A3, VALUED_1:def_5
.= r * (max+ (f . x)) by A5, RFUNCT_3:def_10
.= max ((r * (f . x)),(r * 0)) by A1, FUZZY_2:41 ;
hence (max+ (r (#) f)) . x = (r (#) (max+ f)) . x by A6; ::_thesis: verum
end;
hence max+ (r (#) f) = r (#) (max+ f) by A2, PARTFUN1:5; ::_thesis: max- (r (#) f) = r (#) (max- f)
A7: dom (max- (r (#) f)) = dom (r (#) f) by RFUNCT_3:def_11
.= dom f by VALUED_1:def_5
.= dom (max- f) by RFUNCT_3:def_11
.= dom (r (#) (max- f)) by VALUED_1:def_5 ;
for x being Element of X st x in dom (max- (r (#) f)) holds
(max- (r (#) f)) . x = (r (#) (max- f)) . x
proof
let x be Element of X; ::_thesis: ( x in dom (max- (r (#) f)) implies (max- (r (#) f)) . x = (r (#) (max- f)) . x )
assume A8: x in dom (max- (r (#) f)) ; ::_thesis: (max- (r (#) f)) . x = (r (#) (max- f)) . x
then A9: x in dom (r (#) f) by RFUNCT_3:def_11;
then x in dom f by VALUED_1:def_5;
then A10: x in dom (max- f) by RFUNCT_3:def_11;
A11: (max- (r (#) f)) . x = max- ((r (#) f) . x) by A8, RFUNCT_3:def_11
.= max ((- (r * (f . x))),0) by A9, VALUED_1:def_5 ;
(r (#) (max- f)) . x = r * ((max- f) . x) by A7, A8, VALUED_1:def_5
.= r * (max- (f . x)) by A10, RFUNCT_3:def_11
.= max ((r * (- (f . x))),(r * 0)) by A1, FUZZY_2:41
.= max ((- (r * (f . x))),(r * 0)) ;
hence (max- (r (#) f)) . x = (r (#) (max- f)) . x by A11; ::_thesis: verum
end;
hence max- (r (#) f) = r (#) (max- f) by A7, PARTFUN1:5; ::_thesis: verum
end;
theorem :: MESFUNC6:65
for X being non empty set
for f being PartFunc of X,REAL
for r being Real st 0 <= r holds
( max+ ((- r) (#) f) = r (#) (max- f) & max- ((- r) (#) f) = r (#) (max+ f) )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for r being Real st 0 <= r holds
( max+ ((- r) (#) f) = r (#) (max- f) & max- ((- r) (#) f) = r (#) (max+ f) )
let f be PartFunc of X,REAL; ::_thesis: for r being Real st 0 <= r holds
( max+ ((- r) (#) f) = r (#) (max- f) & max- ((- r) (#) f) = r (#) (max+ f) )
let r be Real; ::_thesis: ( 0 <= r implies ( max+ ((- r) (#) f) = r (#) (max- f) & max- ((- r) (#) f) = r (#) (max+ f) ) )
assume A1: 0 <= r ; ::_thesis: ( max+ ((- r) (#) f) = r (#) (max- f) & max- ((- r) (#) f) = r (#) (max+ f) )
A2: dom (max+ ((- r) (#) f)) = dom ((- r) (#) f) by RFUNCT_3:def_10;
then dom (max+ ((- r) (#) f)) = dom f by VALUED_1:def_5;
then A3: dom (max+ ((- r) (#) f)) = dom (max- f) by RFUNCT_3:def_11;
then A4: dom (max+ ((- r) (#) f)) = dom (r (#) (max- f)) by VALUED_1:def_5;
for x being Element of X st x in dom (max+ ((- r) (#) f)) holds
(max+ ((- r) (#) f)) . x = (r (#) (max- f)) . x
proof
let x be Element of X; ::_thesis: ( x in dom (max+ ((- r) (#) f)) implies (max+ ((- r) (#) f)) . x = (r (#) (max- f)) . x )
assume A5: x in dom (max+ ((- r) (#) f)) ; ::_thesis: (max+ ((- r) (#) f)) . x = (r (#) (max- f)) . x
then A6: (max+ ((- r) (#) f)) . x = max+ (((- r) (#) f) . x) by RFUNCT_3:def_10
.= max (((- r) * (f . x)),0) by A2, A5, VALUED_1:def_5 ;
(r (#) (max- f)) . x = r * ((max- f) . x) by A4, A5, VALUED_1:def_5
.= r * (max- (f . x)) by A3, A5, RFUNCT_3:def_11
.= max ((r * (- (f . x))),(r * 0)) by A1, FUZZY_2:41 ;
hence (max+ ((- r) (#) f)) . x = (r (#) (max- f)) . x by A6; ::_thesis: verum
end;
hence max+ ((- r) (#) f) = r (#) (max- f) by A4, PARTFUN1:5; ::_thesis: max- ((- r) (#) f) = r (#) (max+ f)
A7: dom (max- ((- r) (#) f)) = dom ((- r) (#) f) by RFUNCT_3:def_11;
then dom (max- ((- r) (#) f)) = dom f by VALUED_1:def_5;
then A8: dom (max- ((- r) (#) f)) = dom (max+ f) by RFUNCT_3:def_10;
then A9: dom (max- ((- r) (#) f)) = dom (r (#) (max+ f)) by VALUED_1:def_5;
for x being Element of X st x in dom (max- ((- r) (#) f)) holds
(max- ((- r) (#) f)) . x = (r (#) (max+ f)) . x
proof
let x be Element of X; ::_thesis: ( x in dom (max- ((- r) (#) f)) implies (max- ((- r) (#) f)) . x = (r (#) (max+ f)) . x )
assume A10: x in dom (max- ((- r) (#) f)) ; ::_thesis: (max- ((- r) (#) f)) . x = (r (#) (max+ f)) . x
then A11: (max- ((- r) (#) f)) . x = max- (((- r) (#) f) . x) by RFUNCT_3:def_11
.= max ((- ((- r) * (f . x))),0) by A7, A10, VALUED_1:def_5 ;
(r (#) (max+ f)) . x = r * ((max+ f) . x) by A9, A10, VALUED_1:def_5
.= r * (max+ (f . x)) by A8, A10, RFUNCT_3:def_10
.= max ((r * (f . x)),(r * 0)) by A1, FUZZY_2:41 ;
hence (max- ((- r) (#) f)) . x = (r (#) (max+ f)) . x by A11; ::_thesis: verum
end;
hence max- ((- r) (#) f) = r (#) (max+ f) by A9, PARTFUN1:5; ::_thesis: verum
end;
theorem :: MESFUNC6:66
for X being non empty set
for Y being set
for f being PartFunc of X,REAL holds
( max+ (f | Y) = (max+ f) | Y & max- (f | Y) = (max- f) | Y )
proof
let X be non empty set ; ::_thesis: for Y being set
for f being PartFunc of X,REAL holds
( max+ (f | Y) = (max+ f) | Y & max- (f | Y) = (max- f) | Y )
let Y be set ; ::_thesis: for f being PartFunc of X,REAL holds
( max+ (f | Y) = (max+ f) | Y & max- (f | Y) = (max- f) | Y )
let f be PartFunc of X,REAL; ::_thesis: ( max+ (f | Y) = (max+ f) | Y & max- (f | Y) = (max- f) | Y )
A1: dom (max+ (f | Y)) = dom (f | Y) by RFUNCT_3:def_10
.= (dom f) /\ Y by RELAT_1:61
.= (dom (max+ f)) /\ Y by RFUNCT_3:def_10
.= dom ((max+ f) | Y) by RELAT_1:61 ;
for x being Element of X st x in dom (max+ (f | Y)) holds
(max+ (f | Y)) . x = ((max+ f) | Y) . x
proof
let x be Element of X; ::_thesis: ( x in dom (max+ (f | Y)) implies (max+ (f | Y)) . x = ((max+ f) | Y) . x )
assume A2: x in dom (max+ (f | Y)) ; ::_thesis: (max+ (f | Y)) . x = ((max+ f) | Y) . x
then A3: x in (dom (max+ f)) /\ Y by A1, RELAT_1:61;
then A4: x in Y by XBOOLE_0:def_4;
A5: x in dom (max+ f) by A3, XBOOLE_0:def_4;
A6: (max+ (f | Y)) . x = max+ ((f | Y) . x) by A2, RFUNCT_3:def_10
.= max ((f . x),0) by A4, FUNCT_1:49 ;
((max+ f) | Y) . x = (max+ f) . x by A1, A2, FUNCT_1:47
.= max+ (f . x) by A5, RFUNCT_3:def_10 ;
hence (max+ (f | Y)) . x = ((max+ f) | Y) . x by A6; ::_thesis: verum
end;
hence max+ (f | Y) = (max+ f) | Y by A1, PARTFUN1:5; ::_thesis: max- (f | Y) = (max- f) | Y
A7: dom (max- (f | Y)) = dom (f | Y) by RFUNCT_3:def_11
.= (dom f) /\ Y by RELAT_1:61
.= (dom (max- f)) /\ Y by RFUNCT_3:def_11
.= dom ((max- f) | Y) by RELAT_1:61 ;
for x being Element of X st x in dom (max- (f | Y)) holds
(max- (f | Y)) . x = ((max- f) | Y) . x
proof
let x be Element of X; ::_thesis: ( x in dom (max- (f | Y)) implies (max- (f | Y)) . x = ((max- f) | Y) . x )
assume A8: x in dom (max- (f | Y)) ; ::_thesis: (max- (f | Y)) . x = ((max- f) | Y) . x
then A9: x in (dom (max- f)) /\ Y by A7, RELAT_1:61;
then A10: x in Y by XBOOLE_0:def_4;
A11: x in dom (max- f) by A9, XBOOLE_0:def_4;
A12: (max- (f | Y)) . x = max- ((f | Y) . x) by A8, RFUNCT_3:def_11
.= max ((- (f . x)),0) by A10, FUNCT_1:49 ;
((max- f) | Y) . x = (max- f) . x by A7, A8, FUNCT_1:47
.= max- (f . x) by A11, RFUNCT_3:def_11 ;
hence (max- (f | Y)) . x = ((max- f) | Y) . x by A12; ::_thesis: verum
end;
hence max- (f | Y) = (max- f) | Y by A7, PARTFUN1:5; ::_thesis: verum
end;
theorem :: MESFUNC6:67
for X being non empty set
for Y being set
for f, g being PartFunc of X,REAL st Y c= dom (f + g) holds
( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )
proof
let X be non empty set ; ::_thesis: for Y being set
for f, g being PartFunc of X,REAL st Y c= dom (f + g) holds
( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )
let Y be set ; ::_thesis: for f, g being PartFunc of X,REAL st Y c= dom (f + g) holds
( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )
let f, g be PartFunc of X,REAL; ::_thesis: ( Y c= dom (f + g) implies ( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) )
assume A1: Y c= dom (f + g) ; ::_thesis: ( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )
(dom (f | Y)) /\ (dom (g | Y)) = ((dom f) /\ Y) /\ (dom (g | Y)) by RELAT_1:61
.= ((dom f) /\ Y) /\ ((dom g) /\ Y) by RELAT_1:61
.= (((dom f) /\ Y) /\ (dom g)) /\ Y by XBOOLE_1:16
.= (((dom f) /\ (dom g)) /\ Y) /\ Y by XBOOLE_1:16
.= ((dom f) /\ (dom g)) /\ (Y /\ Y) by XBOOLE_1:16 ;
then A2: dom ((f | Y) + (g | Y)) = ((dom f) /\ (dom g)) /\ Y by VALUED_1:def_1
.= (dom (f + g)) /\ Y by VALUED_1:def_1
.= Y by A1, XBOOLE_1:28 ;
A3: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1;
dom (g | Y) = (dom g) /\ Y by RELAT_1:61;
then A4: dom (g | Y) = Y by A1, A3, XBOOLE_1:18, XBOOLE_1:28;
A5: dom ((f + g) | Y) = (dom (f + g)) /\ Y by RELAT_1:61;
then A6: dom ((f + g) | Y) = Y by A1, XBOOLE_1:28;
dom (f | Y) = (dom f) /\ Y by RELAT_1:61;
then A7: dom (f | Y) = Y by A1, A3, XBOOLE_1:18, XBOOLE_1:28;
now__::_thesis:_for_x_being_set_st_x_in_dom_((f_+_g)_|_Y)_holds_
((f_+_g)_|_Y)_._x_=_((f_|_Y)_+_(g_|_Y))_._x
let x be set ; ::_thesis: ( x in dom ((f + g) | Y) implies ((f + g) | Y) . x = ((f | Y) + (g | Y)) . x )
assume A8: x in dom ((f + g) | Y) ; ::_thesis: ((f + g) | Y) . x = ((f | Y) + (g | Y)) . x
hence ((f + g) | Y) . x = (f + g) . x by FUNCT_1:47
.= (f . x) + (g . x) by A1, A6, A8, VALUED_1:def_1
.= ((f | Y) . x) + (g . x) by A6, A7, A8, FUNCT_1:47
.= ((f | Y) . x) + ((g | Y) . x) by A6, A4, A8, FUNCT_1:47
.= ((f | Y) + (g | Y)) . x by A6, A2, A8, VALUED_1:def_1 ;
::_thesis: verum
end;
hence ( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) by A1, A5, A2, FUNCT_1:2, XBOOLE_1:28; ::_thesis: verum
end;
theorem :: MESFUNC6:68
for X being non empty set
for f being PartFunc of X,REAL
for r being Real holds eq_dom (f,r) = f " {r}
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for r being Real holds eq_dom (f,r) = f " {r}
let f be PartFunc of X,REAL; ::_thesis: for r being Real holds eq_dom (f,r) = f " {r}
let r be Real; ::_thesis: eq_dom (f,r) = f " {r}
now__::_thesis:_for_x_being_set_st_x_in_f_"_{r}_holds_
x_in_eq_dom_(f,r)
let x be set ; ::_thesis: ( x in f " {r} implies x in eq_dom (f,r) )
assume A1: x in f " {r} ; ::_thesis: x in eq_dom (f,r)
then f . x in {r} by FUNCT_1:def_7;
then A2: (R_EAL f) . x = R_EAL r by TARSKI:def_1;
x in dom f by A1, FUNCT_1:def_7;
hence x in eq_dom (f,r) by A2, MESFUNC1:def_15; ::_thesis: verum
end;
then A3: f " {r} c= eq_dom (f,r) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_eq_dom_(f,r)_holds_
x_in_f_"_{r}
let x be set ; ::_thesis: ( x in eq_dom (f,r) implies x in f " {r} )
assume A4: x in eq_dom (f,r) ; ::_thesis: x in f " {r}
then r = f . x by MESFUNC1:def_15;
then A5: f . x in {r} by TARSKI:def_1;
x in dom f by A4, MESFUNC1:def_15;
hence x in f " {r} by A5, FUNCT_1:def_7; ::_thesis: verum
end;
then eq_dom (f,r) c= f " {r} by TARSKI:def_3;
hence eq_dom (f,r) = f " {r} by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
theorem :: MESFUNC6:69
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S
for r, s being Real st f is_measurable_on A & A c= dom f holds
(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S
for r, s being Real st f is_measurable_on A & A c= dom f holds
(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for A being Element of S
for r, s being Real st f is_measurable_on A & A c= dom f holds
(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S
let f be PartFunc of X,REAL; ::_thesis: for A being Element of S
for r, s being Real st f is_measurable_on A & A c= dom f holds
(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S
let A be Element of S; ::_thesis: for r, s being Real st f is_measurable_on A & A c= dom f holds
(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S
let r, s be Real; ::_thesis: ( f is_measurable_on A & A c= dom f implies (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S )
assume that
A1: f is_measurable_on A and
A2: A c= dom f ; ::_thesis: (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S
R_EAL f is_measurable_on A by A1, Def1;
then A3: A /\ (less_dom ((R_EAL f),(R_EAL s))) in S by MESFUNC1:def_16;
A4: (A /\ (great_eq_dom (f,r))) /\ (A /\ (less_dom (f,s))) = ((A /\ (great_eq_dom (f,r))) /\ A) /\ (less_dom (f,s)) by XBOOLE_1:16
.= ((great_eq_dom (f,r)) /\ (A /\ A)) /\ (less_dom (f,s)) by XBOOLE_1:16 ;
A /\ (great_eq_dom (f,r)) in S by A1, A2, Th13;
hence (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S by A3, A4, FINSUB_1:def_2; ::_thesis: verum
end;
theorem Th70: :: MESFUNC6:70
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_simple_func_in S holds
f | A is_simple_func_in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_simple_func_in S holds
f | A is_simple_func_in S
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for A being Element of S st f is_simple_func_in S holds
f | A is_simple_func_in S
let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st f is_simple_func_in S holds
f | A is_simple_func_in S
let A be Element of S; ::_thesis: ( f is_simple_func_in S implies f | A is_simple_func_in S )
assume f is_simple_func_in S ; ::_thesis: f | A is_simple_func_in S
then consider F being Finite_Sep_Sequence of S such that
A1: dom f = union (rng F) and
A2: 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 Def2;
deffunc H1( Nat) -> Element of bool X = (F . $1) /\ A;
consider G being FinSequence such that
A3: ( len G = len F & ( for n being Nat st n in dom G holds
G . n = H1(n) ) ) from FINSEQ_1:sch_2();
A4: rng G c= S
proof
let P be set ; :: according to TARSKI:def_3 ::_thesis: ( not P in rng G or P in S )
assume P in rng G ; ::_thesis: P in S
then consider k being set such that
A5: k in dom G and
A6: P = G . k by FUNCT_1:def_3;
reconsider k = k as Element of NAT by A5;
k in Seg (len F) by A3, A5, FINSEQ_1:def_3;
then k in dom F by FINSEQ_1:def_3;
then A7: F . k in rng F by FUNCT_1:3;
G . k = (F . k) /\ A by A3, A5;
hence P in S by A6, A7, FINSUB_1:def_2; ::_thesis: verum
end;
A8: dom G = Seg (len F) by A3, FINSEQ_1:def_3;
reconsider G = G as FinSequence of S by A4, FINSEQ_1:def_4;
for i, j being Nat st i in dom G & j in dom G & i <> j holds
G . i misses G . j
proof
let i, j be Nat; ::_thesis: ( i in dom G & j in dom G & i <> j implies G . i misses G . j )
assume that
A9: i in dom G and
A10: j in dom G and
A11: i <> j ; ::_thesis: G . i misses G . j
j in Seg (len F) by A3, A10, FINSEQ_1:def_3;
then A12: j in dom F by FINSEQ_1:def_3;
i in Seg (len F) by A3, A9, FINSEQ_1:def_3;
then i in dom F by FINSEQ_1:def_3;
then A13: F . i misses F . j by A11, A12, MESFUNC3:4;
( G . i = (F . i) /\ A & G . j = (F . j) /\ A ) by A3, A9, A10;
then (G . i) /\ (G . j) = (((F . i) /\ A) /\ (F . j)) /\ A by XBOOLE_1:16
.= (((F . i) /\ (F . j)) /\ A) /\ A by XBOOLE_1:16
.= ({} /\ A) /\ A by A13, XBOOLE_0:def_7 ;
hence G . i misses G . j by XBOOLE_0:def_7; ::_thesis: verum
end;
then reconsider G = G as Finite_Sep_Sequence of S by MESFUNC3:4;
for v being set st v in union (rng G) holds
v in dom (f | A)
proof
let v be set ; ::_thesis: ( v in union (rng G) implies v in dom (f | A) )
assume v in union (rng G) ; ::_thesis: v in dom (f | A)
then consider W being set such that
A14: v in W and
A15: W in rng G by TARSKI:def_4;
consider k being set such that
A16: k in dom G and
A17: W = G . k by A15, FUNCT_1:def_3;
reconsider k = k as Element of NAT by A16;
k in Seg (len F) by A3, A16, FINSEQ_1:def_3;
then k in dom F by FINSEQ_1:def_3;
then A18: F . k in rng F by FUNCT_1:3;
A19: G . k = (F . k) /\ A by A3, A16;
then v in F . k by A14, A17, XBOOLE_0:def_4;
then A20: v in union (rng F) by A18, TARSKI:def_4;
v in A by A14, A17, A19, XBOOLE_0:def_4;
then v in (dom f) /\ A by A1, A20, XBOOLE_0:def_4;
hence v in dom (f | A) by RELAT_1:61; ::_thesis: verum
end;
then A21: union (rng G) c= dom (f | A) by TARSKI:def_3;
for v being set st v in dom (f | A) holds
v in union (rng G)
proof
let v be set ; ::_thesis: ( v in dom (f | A) implies v in union (rng G) )
assume v in dom (f | A) ; ::_thesis: v in union (rng G)
then A22: v in (dom f) /\ A by RELAT_1:61;
then A23: v in A by XBOOLE_0:def_4;
v in dom f by A22, XBOOLE_0:def_4;
then consider W being set such that
A24: v in W and
A25: W in rng F by A1, TARSKI:def_4;
consider k being set such that
A26: k in dom F and
A27: W = F . k by A25, FUNCT_1:def_3;
reconsider k = k as Element of NAT by A26;
A28: k in Seg (len F) by A26, FINSEQ_1:def_3;
then k in dom G by A3, FINSEQ_1:def_3;
then A29: G . k in rng G by FUNCT_1:3;
G . k = (F . k) /\ A by A3, A8, A28;
then v in G . k by A23, A24, A27, XBOOLE_0:def_4;
hence v in union (rng G) by A29, TARSKI:def_4; ::_thesis: verum
end;
then dom (f | A) c= union (rng G) by TARSKI:def_3;
then A30: dom (f | A) = union (rng G) by A21, XBOOLE_0:def_10;
for n being Nat
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
(f | A) . x = (f | A) . y
proof
let n be Nat; ::_thesis: for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
(f | A) . x = (f | A) . y
let x, y be Element of X; ::_thesis: ( n in dom G & x in G . n & y in G . n implies (f | A) . x = (f | A) . y )
assume that
A31: n in dom G and
A32: x in G . n and
A33: y in G . n ; ::_thesis: (f | A) . x = (f | A) . y
n in Seg (len F) by A3, A31, FINSEQ_1:def_3;
then A34: n in dom F by FINSEQ_1:def_3;
G . n = (F . n) /\ A by A3, A31;
then ( x in F . n & y in F . n ) by A32, A33, XBOOLE_0:def_4;
then A35: f . x = f . y by A2, A34;
A36: G . n in rng G by A31, FUNCT_1:3;
then x in dom (f | A) by A30, A32, TARSKI:def_4;
then A37: (f | A) . x = f . y by A35, FUNCT_1:47;
y in dom (f | A) by A30, A33, A36, TARSKI:def_4;
hence (f | A) . x = (f | A) . y by A37, FUNCT_1:47; ::_thesis: verum
end;
hence f | A is_simple_func_in S by A30, Def2; ::_thesis: verum
end;
theorem Th71: :: MESFUNC6:71
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL st f is_simple_func_in S holds
dom f is Element of S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL st f is_simple_func_in S holds
dom f is Element of S
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL st f is_simple_func_in S holds
dom f is Element of S
let f be PartFunc of X,REAL; ::_thesis: ( f is_simple_func_in S implies dom f is Element of S )
assume f is_simple_func_in S ; ::_thesis: dom f is Element of S
then ex F being Finite_Sep_Sequence of S st
( dom f = union (rng F) & ( 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 Def2;
hence dom f is Element of S by MESFUNC2:31; ::_thesis: verum
end;
Lm1: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds
( f + g is_simple_func_in S & dom (f + g) <> {} )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds
( f + g is_simple_func_in S & dom (f + g) <> {} )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds
( f + g is_simple_func_in S & dom (f + g) <> {} )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds
( f + g is_simple_func_in S & dom (f + g) <> {} )
let f, g be PartFunc of X,REAL; ::_thesis: ( f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f implies ( f + g is_simple_func_in S & dom (f + g) <> {} ) )
assume that
A1: f is_simple_func_in S and
A2: dom f <> {} and
A3: g is_simple_func_in S and
A4: dom g = dom f ; ::_thesis: ( f + g is_simple_func_in S & dom (f + g) <> {} )
R_EAL f is_simple_func_in S by A1, Th49;
then consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that
A5: F,a are_Re-presentation_of R_EAL f by MESFUNC3:12;
set la = len F;
A6: dom f = union (rng F) by A5, MESFUNC3:def_1;
R_EAL g is_simple_func_in S by A3, Th49;
then consider G being Finite_Sep_Sequence of S, b being FinSequence of ExtREAL such that
A7: G,b are_Re-presentation_of R_EAL g by MESFUNC3:12;
set lb = len G;
A8: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1;
deffunc H1( Nat) -> set = (F . ((($1 -' 1) div (len G)) + 1)) /\ (G . ((($1 -' 1) mod (len G)) + 1));
consider FG being FinSequence such that
A9: len FG = (len F) * (len G) and
A10: for k being Nat st k in dom FG holds
FG . k = H1(k) from FINSEQ_1:sch_2();
A11: dom FG = Seg ((len F) * (len G)) by A9, FINSEQ_1:def_3;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_FG_holds_
FG_._k_in_S
reconsider la9 = len F, lb9 = len G as Nat ;
let k be Nat; ::_thesis: ( k in dom FG implies FG . k in S )
set i = ((k -' 1) div (len G)) + 1;
set j = ((k -' 1) mod (len G)) + 1;
assume A12: k in dom FG ; ::_thesis: FG . k in S
then A13: k in Seg ((len F) * (len G)) by A9, FINSEQ_1:def_3;
then A14: k <= (len F) * (len G) by FINSEQ_1:1;
then k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;
then A15: (k -' 1) div (len G) <= (((len F) * (len G)) -' 1) div (len G) by NAT_2:24;
1 <= k by A13, FINSEQ_1:1;
then A16: ( lb9 divides la9 * lb9 & 1 <= (len F) * (len G) ) by A14, NAT_D:def_3, XXREAL_0:2;
A17: len G <> 0 by A13, A14, FINSEQ_1:1;
then len G >= 0 + 1 by NAT_1:13;
then ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A16, NAT_2:15;
then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by A15, XREAL_1:19;
then ( ((k -' 1) div (len G)) + 1 >= 0 + 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A17, NAT_D:18, XREAL_1:6;
then ((k -' 1) div (len G)) + 1 in Seg (len F) ;
then ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def_3;
then A18: F . (((k -' 1) div (len G)) + 1) in rng F by FUNCT_1:3;
(k -' 1) mod (len G) < len G by A17, NAT_D:1;
then ( ((k -' 1) mod (len G)) + 1 >= 0 + 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13;
then ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_3:25;
then G . (((k -' 1) mod (len G)) + 1) in rng G by FUNCT_1:3;
then (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) in S by A18, MEASURE1:34;
hence FG . k in S by A10, A12; ::_thesis: verum
end;
then reconsider FG = FG as FinSequence of S by FINSEQ_2:12;
for k, l being Nat st k in dom FG & l in dom FG & k <> l holds
FG . k misses FG . l
proof
reconsider la9 = len F, lb9 = len G as Nat ;
let k, l be Nat; ::_thesis: ( k in dom FG & l in dom FG & k <> l implies FG . k misses FG . l )
assume that
A19: k in dom FG and
A20: l in dom FG and
A21: k <> l ; ::_thesis: FG . k misses FG . l
set j = ((k -' 1) mod (len G)) + 1;
set i = ((k -' 1) div (len G)) + 1;
A22: FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A10, A19;
set m = ((l -' 1) mod (len G)) + 1;
set n = ((l -' 1) div (len G)) + 1;
A23: k in Seg ((len F) * (len G)) by A9, A19, FINSEQ_1:def_3;
then A24: 1 <= k by FINSEQ_1:1;
then A25: len G <> 0 by A23, FINSEQ_1:1;
then (k -' 1) mod (len G) < len G by NAT_D:1;
then ( ((k -' 1) mod (len G)) + 1 >= 0 + 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13;
then A26: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_3:25;
A27: k <= (len F) * (len G) by A23, FINSEQ_1:1;
then A28: ( lb9 divides la9 * lb9 & 1 <= (len F) * (len G) ) by A24, NAT_D:def_3, XXREAL_0:2;
len G >= 0 + 1 by A25, NAT_1:13;
then A29: ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A28, NAT_2:15;
A30: l in Seg ((len F) * (len G)) by A9, A20, FINSEQ_1:def_3;
then A31: 1 <= l by FINSEQ_1:1;
A32: now__::_thesis:_(_((k_-'_1)_div_(len_G))_+_1_=_((l_-'_1)_div_(len_G))_+_1_implies_not_((k_-'_1)_mod_(len_G))_+_1_=_((l_-'_1)_mod_(len_G))_+_1_)
(l -' 1) + 1 = ((((((l -' 1) div (len G)) + 1) - 1) * (len G)) + ((((l -' 1) mod (len G)) + 1) - 1)) + 1 by A25, NAT_D:2;
then A33: (l - 1) + 1 = (((((l -' 1) div (len G)) + 1) - 1) * (len G)) + (((l -' 1) mod (len G)) + 1) by A31, XREAL_1:233;
(k -' 1) + 1 = ((((((k -' 1) div (len G)) + 1) - 1) * (len G)) + ((((k -' 1) mod (len G)) + 1) - 1)) + 1 by A25, NAT_D:2;
then A34: (k - 1) + 1 = (((((k -' 1) div (len G)) + 1) - 1) * (len G)) + (((k -' 1) mod (len G)) + 1) by A24, XREAL_1:233;
assume ( ((k -' 1) div (len G)) + 1 = ((l -' 1) div (len G)) + 1 & ((k -' 1) mod (len G)) + 1 = ((l -' 1) mod (len G)) + 1 ) ; ::_thesis: contradiction
hence contradiction by A21, A34, A33; ::_thesis: verum
end;
k -' 1 <= ((len F) * (len G)) -' 1 by A27, NAT_D:42;
then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A29, NAT_2:24;
then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;
then ( ((k -' 1) div (len G)) + 1 >= 0 + 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A25, NAT_D:18, XREAL_1:6;
then ((k -' 1) div (len G)) + 1 in Seg (len F) ;
then A35: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def_3;
(l -' 1) mod (len G) < len G by A25, NAT_D:1;
then ( ((l -' 1) mod (len G)) + 1 >= 0 + 1 & ((l -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13;
then A36: ((l -' 1) mod (len G)) + 1 in dom G by FINSEQ_3:25;
l <= (len F) * (len G) by A30, FINSEQ_1:1;
then l -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;
then (l -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A29, NAT_2:24;
then ((l -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;
then ( ((l -' 1) div (len G)) + 1 >= 0 + 1 & ((l -' 1) div (len G)) + 1 <= len F ) by A25, NAT_D:18, XREAL_1:6;
then ((l -' 1) div (len G)) + 1 in Seg (len F) ;
then A37: ((l -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def_3;
percases ( ((k -' 1) div (len G)) + 1 <> ((l -' 1) div (len G)) + 1 or ((k -' 1) mod (len G)) + 1 <> ((l -' 1) mod (len G)) + 1 ) by A32;
supposeA38: ((k -' 1) div (len G)) + 1 <> ((l -' 1) div (len G)) + 1 ; ::_thesis: FG . k misses FG . l
(FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A10, A20, A22;
then (FG . k) /\ (FG . l) = (F . (((k -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16;
then (FG . k) /\ (FG . l) = (F . (((k -' 1) div (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16;
then A39: (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by XBOOLE_1:16;
F . (((k -' 1) div (len G)) + 1) misses F . (((l -' 1) div (len G)) + 1) by A35, A37, A38, MESFUNC3:4;
then (FG . k) /\ (FG . l) = {} /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A39, XBOOLE_0:def_7;
hence FG . k misses FG . l by XBOOLE_0:def_7; ::_thesis: verum
end;
supposeA40: ((k -' 1) mod (len G)) + 1 <> ((l -' 1) mod (len G)) + 1 ; ::_thesis: FG . k misses FG . l
(FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A10, A20, A22;
then (FG . k) /\ (FG . l) = (F . (((k -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16;
then (FG . k) /\ (FG . l) = (F . (((k -' 1) div (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16;
then A41: (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by XBOOLE_1:16;
G . (((k -' 1) mod (len G)) + 1) misses G . (((l -' 1) mod (len G)) + 1) by A26, A36, A40, MESFUNC3:4;
then (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ {} by A41, XBOOLE_0:def_7;
hence FG . k misses FG . l by XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4;
A42: dom g = union (rng G) by A7, MESFUNC3:def_1;
A43: dom f = union (rng FG)
proof
now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_
z_in_union_(rng_FG)
let z be set ; ::_thesis: ( z in dom f implies z in union (rng FG) )
assume A44: z in dom f ; ::_thesis: z in union (rng FG)
then consider Y being set such that
A45: z in Y and
A46: Y in rng F by A6, TARSKI:def_4;
consider i being Nat such that
A47: i in dom F and
A48: Y = F . i by A46, FINSEQ_2:10;
A49: i in Seg (len F) by A47, FINSEQ_1:def_3;
then 1 <= i by FINSEQ_1:1;
then consider i9 being Nat such that
A50: i = 1 + i9 by NAT_1:10;
consider Z being set such that
A51: z in Z and
A52: Z in rng G by A4, A42, A44, TARSKI:def_4;
consider j being Nat such that
A53: j in dom G and
A54: Z = G . j by A52, FINSEQ_2:10;
A55: j in Seg (len G) by A53, FINSEQ_1:def_3;
then A56: 1 <= j by FINSEQ_1:1;
then consider j9 being Nat such that
A57: j = 1 + j9 by NAT_1:10;
A58: j <= len G by A55, FINSEQ_1:1;
then A59: j9 < len G by A57, NAT_1:13;
reconsider k = ((i - 1) * (len G)) + j as Nat by A50;
A60: k >= 0 + j by A50, XREAL_1:6;
then A61: k -' 1 = k - 1 by A56, XREAL_1:233, XXREAL_0:2
.= (i9 * (len G)) + j9 by A50, A57 ;
then A62: i = ((k -' 1) div (len G)) + 1 by A50, A59, NAT_D:def_1;
i <= len F by A49, FINSEQ_1:1;
then i - 1 <= (len F) - 1 by XREAL_1:9;
then (i - 1) * (len G) <= ((len F) - 1) * (len G) by XREAL_1:64;
then A63: k <= (((len F) - 1) * (len G)) + j by XREAL_1:6;
(((len F) - 1) * (len G)) + j <= (((len F) - 1) * (len G)) + (len G) by A58, XREAL_1:6;
then A64: k <= (len F) * (len G) by A63, XXREAL_0:2;
k >= 1 by A56, A60, XXREAL_0:2;
then A65: k in Seg ((len F) * (len G)) by A64, FINSEQ_1:1;
then k in dom FG by A9, FINSEQ_1:def_3;
then A66: FG . k in rng FG by FUNCT_1:def_3;
A67: j = ((k -' 1) mod (len G)) + 1 by A57, A61, A59, NAT_D:def_2;
z in (F . i) /\ (G . j) by A45, A48, A51, A54, XBOOLE_0:def_4;
then z in FG . k by A10, A11, A62, A67, A65;
hence z in union (rng FG) by A66, TARSKI:def_4; ::_thesis: verum
end;
hence dom f c= union (rng FG) by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: union (rng FG) c= dom f
reconsider la9 = len F, lb9 = len G as Nat ;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union (rng FG) or z in dom f )
assume z in union (rng FG) ; ::_thesis: z in dom f
then consider Y being set such that
A68: z in Y and
A69: Y in rng FG by TARSKI:def_4;
consider k being Nat such that
A70: k in dom FG and
A71: Y = FG . k by A69, FINSEQ_2:10;
set j = ((k -' 1) mod (len G)) + 1;
set i = ((k -' 1) div (len G)) + 1;
A72: k in Seg (len FG) by A70, FINSEQ_1:def_3;
then A73: k <= (len F) * (len G) by A9, FINSEQ_1:1;
then A74: len G <> 0 by A72, FINSEQ_1:1;
then A75: len G >= 0 + 1 by NAT_1:13;
1 <= k by A72, FINSEQ_1:1;
then ( lb9 divides la9 * lb9 & 1 <= (len F) * (len G) ) by A73, NAT_D:def_3, XXREAL_0:2;
then A76: ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A75, NAT_2:15;
k -' 1 <= ((len F) * (len G)) -' 1 by A73, NAT_D:42;
then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A76, NAT_2:24;
then A77: ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;
( ((k -' 1) div (len G)) + 1 >= 0 + 1 & ((len F) * (len G)) div (len G) = len F ) by A74, NAT_D:18, XREAL_1:6;
then ((k -' 1) div (len G)) + 1 in Seg (len F) by A77;
then ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def_3;
then A78: F . (((k -' 1) div (len G)) + 1) in rng F by FUNCT_1:def_3;
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A10, A70;
then z in F . (((k -' 1) div (len G)) + 1) by A68, A71, XBOOLE_0:def_4;
hence z in dom f by A6, A78, TARSKI:def_4; ::_thesis: verum
end;
for k being Nat
for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds
(f + g) . x = (f + g) . y
proof
reconsider la9 = len F, lb9 = len G as Nat ;
let k be Nat; ::_thesis: for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds
(f + g) . x = (f + g) . y
let x, y be Element of X; ::_thesis: ( k in dom FG & x in FG . k & y in FG . k implies (f + g) . x = (f + g) . y )
assume that
A79: k in dom FG and
A80: x in FG . k and
A81: y in FG . k ; ::_thesis: (f + g) . x = (f + g) . y
set i = ((k -' 1) div (len G)) + 1;
set j = ((k -' 1) mod (len G)) + 1;
A82: k in Seg (len FG) by A79, FINSEQ_1:def_3;
then A83: k <= (len F) * (len G) by A9, FINSEQ_1:1;
then A84: k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;
A85: len G <> 0 by A82, A83, FINSEQ_1:1;
then (k -' 1) mod (len G) < len G by NAT_D:1;
then ( ((k -' 1) mod (len G)) + 1 >= 0 + 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13;
then ((k -' 1) mod (len G)) + 1 in Seg (len G) ;
then A86: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_1:def_3;
1 <= k by A82, FINSEQ_1:1;
then A87: ( lb9 divides la9 * lb9 & 1 <= (len F) * (len G) ) by A83, NAT_D:def_3, XXREAL_0:2;
len G >= 0 + 1 by A85, NAT_1:13;
then ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A87, NAT_2:15;
then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A84, NAT_2:24;
then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;
then ( ((k -' 1) div (len G)) + 1 >= 0 + 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A85, NAT_D:18, XREAL_1:6;
then ((k -' 1) div (len G)) + 1 in Seg (len F) ;
then A88: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def_3;
A89: FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A10, A79;
then x in G . (((k -' 1) mod (len G)) + 1) by A80, XBOOLE_0:def_4;
then A90: g . x = b . (((k -' 1) mod (len G)) + 1) by A7, A86, MESFUNC3:def_1;
y in G . (((k -' 1) mod (len G)) + 1) by A81, A89, XBOOLE_0:def_4;
then A91: g . y = b . (((k -' 1) mod (len G)) + 1) by A7, A86, MESFUNC3:def_1;
x in F . (((k -' 1) div (len G)) + 1) by A80, A89, XBOOLE_0:def_4;
then f . x = a . (((k -' 1) div (len G)) + 1) by A5, A88, MESFUNC3:def_1;
then A92: (f . x) + (g . x) = (a . (((k -' 1) div (len G)) + 1)) + (b . (((k -' 1) mod (len G)) + 1)) by A90, SUPINF_2:1;
y in F . (((k -' 1) div (len G)) + 1) by A81, A89, XBOOLE_0:def_4;
then A93: f . y = a . (((k -' 1) div (len G)) + 1) by A5, A88, MESFUNC3:def_1;
A94: FG . k in rng FG by A79, FUNCT_1:def_3;
then x in dom (f + g) by A4, A43, A8, A80, TARSKI:def_4;
then (f + g) . x = (a . (((k -' 1) div (len G)) + 1)) + (b . (((k -' 1) mod (len G)) + 1)) by A92, VALUED_1:def_1;
then A95: (f + g) . x = (f . y) + (g . y) by A93, A91, SUPINF_2:1;
y in dom (f + g) by A4, A43, A8, A81, A94, TARSKI:def_4;
hence (f + g) . x = (f + g) . y by A95, VALUED_1:def_1; ::_thesis: verum
end;
hence f + g is_simple_func_in S by A4, A43, A8, Def2; ::_thesis: dom (f + g) <> {}
thus dom (f + g) <> {} by A2, A4, A8; ::_thesis: verum
end;
theorem :: MESFUNC6:72
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL st f is_simple_func_in S & g is_simple_func_in S holds
f + g is_simple_func_in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f, g being PartFunc of X,REAL st f is_simple_func_in S & g is_simple_func_in S holds
f + g is_simple_func_in S
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL st f is_simple_func_in S & g is_simple_func_in S holds
f + g is_simple_func_in S
let f, g be PartFunc of X,REAL; ::_thesis: ( f is_simple_func_in S & g is_simple_func_in S implies f + g is_simple_func_in S )
assume A1: ( f is_simple_func_in S & g is_simple_func_in S ) ; ::_thesis: f + g is_simple_func_in S
percases ( dom (f + g) = {} or dom (f + g) <> {} ) ;
supposeA2: dom (f + g) = {} ; ::_thesis: f + g is_simple_func_in S
ex F being Finite_Sep_Sequence of S st
( dom (f + g) = union (rng F) & ( 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 + g) . x = (f + g) . y ) )
proof
reconsider EMPTY = {} as Element of S by PROB_1:4;
set F = <*EMPTY*>;
A3: dom <*EMPTY*> = Seg 1 by FINSEQ_1:38;
A4: now__::_thesis:_for_i,_j_being_Nat_st_i_in_dom_<*EMPTY*>_&_j_in_dom_<*EMPTY*>_&_i_<>_j_holds_
<*EMPTY*>_._i_misses_<*EMPTY*>_._j
let i, j be Nat; ::_thesis: ( i in dom <*EMPTY*> & j in dom <*EMPTY*> & i <> j implies <*EMPTY*> . i misses <*EMPTY*> . j )
assume that
A5: i in dom <*EMPTY*> and
A6: ( j in dom <*EMPTY*> & i <> j ) ; ::_thesis: <*EMPTY*> . i misses <*EMPTY*> . j
i = 1 by A3, A5, FINSEQ_1:2, TARSKI:def_1;
hence <*EMPTY*> . i misses <*EMPTY*> . j by A3, A6, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum
end;
A7: for n being Nat st n in dom <*EMPTY*> holds
<*EMPTY*> . n = EMPTY
proof
let n be Nat; ::_thesis: ( n in dom <*EMPTY*> implies <*EMPTY*> . n = EMPTY )
assume n in dom <*EMPTY*> ; ::_thesis: <*EMPTY*> . n = EMPTY
then n = 1 by A3, FINSEQ_1:2, TARSKI:def_1;
hence <*EMPTY*> . n = EMPTY by FINSEQ_1:40; ::_thesis: verum
end;
reconsider F = <*EMPTY*> as Finite_Sep_Sequence of S by A4, MESFUNC3:4;
take F ; ::_thesis: ( dom (f + g) = union (rng F) & ( 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 + g) . x = (f + g) . y ) )
union (rng F) = union (bool {}) by FINSEQ_1:39, ZFMISC_1:1;
hence dom (f + g) = union (rng F) by A2; ::_thesis: 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 + g) . x = (f + g) . y
thus 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 + g) . x = (f + g) . y by A7; ::_thesis: verum
end;
hence f + g is_simple_func_in S by Def2; ::_thesis: verum
end;
supposeA8: dom (f + g) <> {} ; ::_thesis: f + g is_simple_func_in S
A9: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1;
( dom f is Element of S & dom g is Element of S ) by A1, Th71;
then dom (f + g) in S by A9, FINSUB_1:def_2;
then A10: ( f | (dom (f + g)) is_simple_func_in S & g | (dom (f + g)) is_simple_func_in S ) by A1, Th70;
dom (f | (dom (f + g))) = (dom f) /\ (dom (f + g)) by RELAT_1:61;
then A11: dom (f | (dom (f + g))) = ((dom f) /\ (dom f)) /\ (dom g) by A9, XBOOLE_1:16;
dom (g | (dom (f + g))) = (dom g) /\ (dom (f + g)) by RELAT_1:61;
then A12: dom (g | (dom (f + g))) = ((dom g) /\ (dom g)) /\ (dom f) by A9, XBOOLE_1:16;
then A13: dom (g | (dom (f + g))) = dom (f + g) by VALUED_1:def_1;
A14: dom ((f | (dom (f + g))) + (g | (dom (f + g)))) = (dom (f | (dom (f + g)))) /\ (dom (g | (dom (f + g)))) by VALUED_1:def_1
.= dom (f + g) by A11, A12, VALUED_1:def_1 ;
A15: for x being Element of X st x in dom ((f | (dom (f + g))) + (g | (dom (f + g)))) holds
((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x
proof
let x be Element of X; ::_thesis: ( x in dom ((f | (dom (f + g))) + (g | (dom (f + g)))) implies ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x )
assume A16: x in dom ((f | (dom (f + g))) + (g | (dom (f + g)))) ; ::_thesis: ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x
then ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = ((f | (dom (f + g))) . x) + ((g | (dom (f + g))) . x) by VALUED_1:def_1
.= (f . x) + ((g | (dom (f + g))) . x) by A14, A16, FUNCT_1:49
.= (f . x) + (g . x) by A14, A16, FUNCT_1:49 ;
hence ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x by A14, A16, VALUED_1:def_1; ::_thesis: verum
end;
dom (f | (dom (f + g))) = dom (f + g) by A11, VALUED_1:def_1;
then (f | (dom (f + g))) + (g | (dom (f + g))) is_simple_func_in S by A8, A10, A13, Lm1;
hence f + g is_simple_func_in S by A14, A15, PARTFUN1:5; ::_thesis: verum
end;
end;
end;
theorem :: MESFUNC6:73
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for r being Real st f is_simple_func_in S holds
r (#) f is_simple_func_in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for r being Real st f is_simple_func_in S holds
r (#) f is_simple_func_in S
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for r being Real st f is_simple_func_in S holds
r (#) f is_simple_func_in S
let f be PartFunc of X,REAL; ::_thesis: for r being Real st f is_simple_func_in S holds
r (#) f is_simple_func_in S
let r be Real; ::_thesis: ( f is_simple_func_in S implies r (#) f is_simple_func_in S )
set g = r (#) f;
assume f is_simple_func_in S ; ::_thesis: r (#) f is_simple_func_in S
then consider G being Finite_Sep_Sequence of S such that
A1: dom f = union (rng G) and
A2: for n being Nat
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
f . x = f . y by Def2;
A3: dom (r (#) f) = dom f by VALUED_1:def_5;
now__::_thesis:_for_n_being_Nat
for_x,_y_being_Element_of_X_st_n_in_dom_G_&_x_in_G_._n_&_y_in_G_._n_holds_
(r_(#)_f)_._x_=_(r_(#)_f)_._y
let n be Nat; ::_thesis: for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
(r (#) f) . x = (r (#) f) . y
let x, y be Element of X; ::_thesis: ( n in dom G & x in G . n & y in G . n implies (r (#) f) . x = (r (#) f) . y )
assume that
A4: n in dom G and
A5: x in G . n and
A6: y in G . n ; ::_thesis: (r (#) f) . x = (r (#) f) . y
A7: G . n in rng G by A4, FUNCT_1:3;
then y in dom (r (#) f) by A3, A1, A6, TARSKI:def_4;
then A8: (r (#) f) . y = r * (f . y) by VALUED_1:def_5;
x in dom (r (#) f) by A3, A1, A5, A7, TARSKI:def_4;
then (r (#) f) . x = r * (f . x) by VALUED_1:def_5;
hence (r (#) f) . x = (r (#) f) . y by A2, A4, A5, A6, A8; ::_thesis: verum
end;
hence r (#) f is_simple_func_in S by A3, A1, Def2; ::_thesis: verum
end;
theorem :: MESFUNC6:74
for X being non empty set
for f, g being PartFunc of X,REAL st ( for x being set st x in dom (f - g) holds
g . x <= f . x ) holds
f - g is nonnegative
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL st ( for x being set st x in dom (f - g) holds
g . x <= f . x ) holds
f - g is nonnegative
let f, g be PartFunc of X,REAL; ::_thesis: ( ( for x being set st x in dom (f - g) holds
g . x <= f . x ) implies f - g is nonnegative )
A1: dom (f - g) = (dom f) /\ (dom g) by VALUED_1:12;
assume for x being set st x in dom (f - g) holds
g . x <= f . x ; ::_thesis: f - g is nonnegative
hence f - g is nonnegative by A1, Th58; ::_thesis: verum
end;
theorem :: MESFUNC6:75
for X being non empty set
for S being SigmaField of X
for A being Element of S
for r being Real ex f being PartFunc of X,REAL st
( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds
f . x = r ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for A being Element of S
for r being Real ex f being PartFunc of X,REAL st
( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds
f . x = r ) )
let S be SigmaField of X; ::_thesis: for A being Element of S
for r being Real ex f being PartFunc of X,REAL st
( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds
f . x = r ) )
let A be Element of S; ::_thesis: for r being Real ex f being PartFunc of X,REAL st
( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds
f . x = r ) )
let r be Real; ::_thesis: ex f being PartFunc of X,REAL st
( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds
f . x = r ) )
defpred S1[ set ] means $1 in A;
deffunc H1( set ) -> Real = r;
A1: for x being set st S1[x] holds
H1(x) in REAL ;
consider f being PartFunc of X,REAL such that
A2: ( ( for x being set holds
( x in dom f iff ( x in X & S1[x] ) ) ) & ( for x being set st x in dom f holds
f . x = H1(x) ) ) from PARTFUN1:sch_3(A1);
take f ; ::_thesis: ( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds
f . x = r ) )
A3: A c= dom f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in dom f )
assume x in A ; ::_thesis: x in dom f
hence x in dom f by A2; ::_thesis: verum
end;
A4: dom f c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in A )
assume x in dom f ; ::_thesis: x in A
hence x in A by A2; ::_thesis: verum
end;
ex F being Finite_Sep_Sequence of S st
( dom f = union (rng F) & ( 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 ) )
proof
set F = <*(dom f)*>;
A5: rng <*(dom f)*> = {(dom f)} by FINSEQ_1:38;
then rng <*(dom f)*> = {A} by A4, A3, XBOOLE_0:def_10;
then reconsider F = <*(dom f)*> as FinSequence of S by FINSEQ_1:def_4;
now__::_thesis:_for_i,_j_being_Nat_st_i_in_dom_F_&_j_in_dom_F_&_i_<>_j_holds_
F_._i_misses_F_._j
let i, j be Nat; ::_thesis: ( i in dom F & j in dom F & i <> j implies F . i misses F . j )
assume that
A6: i in dom F and
A7: ( j in dom F & i <> j ) ; ::_thesis: F . i misses F . j
A8: dom F = Seg 1 by FINSEQ_1:38;
then i = 1 by A6, FINSEQ_1:2, TARSKI:def_1;
hence F . i misses F . j by A7, A8, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum
end;
then reconsider F = F as Finite_Sep_Sequence of S by MESFUNC3:4;
take F ; ::_thesis: ( dom f = union (rng F) & ( 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 ) )
thus dom f = union (rng F) by A5, ZFMISC_1:25; ::_thesis: 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
hereby ::_thesis: verum
let n be Nat; ::_thesis: 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
let x, y be Element of X; ::_thesis: ( n in dom F & x in F . n & y in F . n implies f . x = f . y )
assume that
A9: n in dom F and
A10: x in F . n and
A11: y in F . n ; ::_thesis: f . x = f . y
dom F = Seg 1 by FINSEQ_1:38;
then A12: n = 1 by A9, FINSEQ_1:2, TARSKI:def_1;
then x in dom f by A10, FINSEQ_1:40;
then A13: f . x = r by A2;
y in dom f by A11, A12, FINSEQ_1:40;
hence f . x = f . y by A2, A13; ::_thesis: verum
end;
end;
hence f is_simple_func_in S by Def2; ::_thesis: ( dom f = A & ( for x being set st x in A holds
f . x = r ) )
thus dom f = A by A4, A3, XBOOLE_0:def_10; ::_thesis: for x being set st x in A holds
f . x = r
thus for x being set st x in A holds
f . x = r by A2; ::_thesis: verum
end;
theorem :: MESFUNC6:76
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for B, A being Element of S st f is_measurable_on B & A = (dom f) /\ B holds
f | B is_measurable_on A
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for B, A being Element of S st f is_measurable_on B & A = (dom f) /\ B holds
f | B is_measurable_on A
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for B, A being Element of S st f is_measurable_on B & A = (dom f) /\ B holds
f | B is_measurable_on A
let f be PartFunc of X,REAL; ::_thesis: for B, A being Element of S st f is_measurable_on B & A = (dom f) /\ B holds
f | B is_measurable_on A
let B, A be Element of S; ::_thesis: ( f is_measurable_on B & A = (dom f) /\ B implies f | B is_measurable_on A )
assume that
A1: f is_measurable_on B and
A2: A = (dom f) /\ B ; ::_thesis: f | B is_measurable_on A
A3: R_EAL f is_measurable_on B by A1, Def1;
now__::_thesis:_for_r_being_real_number_holds_A_/\_(less_dom_((f_|_B),r))_in_S
let r be real number ; ::_thesis: A /\ (less_dom ((f | B),r)) in S
now__::_thesis:_for_x_being_set_holds_
(_x_in_A_/\_(less_dom_((f_|_B),r))_iff_x_in_B_/\_(less_dom_(f,r))_)
let x be set ; ::_thesis: ( x in A /\ (less_dom ((f | B),r)) iff x in B /\ (less_dom (f,r)) )
( x in dom (f | B) & (f | B) . x < R_EAL r iff ( x in (dom f) /\ B & (f | B) . x < R_EAL r ) ) by RELAT_1:61;
then A4: ( x in A & x in less_dom ((f | B),r) iff ( x in B & x in dom f & (f | B) . x < R_EAL r ) ) by A2, MESFUNC1:def_11, XBOOLE_0:def_4;
( x in B & x in dom f implies ( f . x < R_EAL r iff (f | B) . x < R_EAL r ) ) by FUNCT_1:49;
then ( x in A /\ (less_dom ((f | B),r)) iff ( x in B & x in less_dom (f,r) ) ) by A4, MESFUNC1:def_11, XBOOLE_0:def_4;
hence ( x in A /\ (less_dom ((f | B),r)) iff x in B /\ (less_dom (f,r)) ) by XBOOLE_0:def_4; ::_thesis: verum
end;
then ( A /\ (less_dom ((f | B),r)) c= B /\ (less_dom (f,r)) & B /\ (less_dom (f,r)) c= A /\ (less_dom ((f | B),r)) ) by TARSKI:def_3;
then A /\ (less_dom ((f | B),r)) = B /\ (less_dom (f,r)) by XBOOLE_0:def_10;
then A /\ (less_dom ((f | B),(R_EAL r))) in S by A3, MESFUNC1:def_16;
hence A /\ (less_dom ((f | B),r)) in S ; ::_thesis: verum
end;
hence f | B is_measurable_on A by Th12; ::_thesis: verum
end;
theorem :: MESFUNC6:77
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S st A c= dom f & f is_measurable_on A & g is_measurable_on A holds
(max+ (f + g)) + (max- f) is_measurable_on A
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S st A c= dom f & f is_measurable_on A & g is_measurable_on A holds
(max+ (f + g)) + (max- f) is_measurable_on A
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL
for A being Element of S st A c= dom f & f is_measurable_on A & g is_measurable_on A holds
(max+ (f + g)) + (max- f) is_measurable_on A
let f, g be PartFunc of X,REAL; ::_thesis: for A being Element of S st A c= dom f & f is_measurable_on A & g is_measurable_on A holds
(max+ (f + g)) + (max- f) is_measurable_on A
let A be Element of S; ::_thesis: ( A c= dom f & f is_measurable_on A & g is_measurable_on A implies (max+ (f + g)) + (max- f) is_measurable_on A )
assume that
A1: A c= dom f and
A2: f is_measurable_on A and
A3: g is_measurable_on A ; ::_thesis: (max+ (f + g)) + (max- f) is_measurable_on A
f + g is_measurable_on A by A2, A3, Th26;
then A4: max+ (f + g) is_measurable_on A by Th46;
max- f is_measurable_on A by A1, A2, Th47;
hence (max+ (f + g)) + (max- f) is_measurable_on A by A4, Th26; ::_thesis: verum
end;
theorem :: MESFUNC6:78
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S st A c= (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A holds
(max- (f + g)) + (max+ f) is_measurable_on A
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S st A c= (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A holds
(max- (f + g)) + (max+ f) is_measurable_on A
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL
for A being Element of S st A c= (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A holds
(max- (f + g)) + (max+ f) is_measurable_on A
let f, g be PartFunc of X,REAL; ::_thesis: for A being Element of S st A c= (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A holds
(max- (f + g)) + (max+ f) is_measurable_on A
let A be Element of S; ::_thesis: ( A c= (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A implies (max- (f + g)) + (max+ f) is_measurable_on A )
assume that
A1: A c= (dom f) /\ (dom g) and
A2: f is_measurable_on A and
A3: g is_measurable_on A ; ::_thesis: (max- (f + g)) + (max+ f) is_measurable_on A
A4: max+ f is_measurable_on A by A2, Th46;
A5: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1;
f + g is_measurable_on A by A2, A3, Th26;
then max- (f + g) is_measurable_on A by A1, A5, Th47;
hence (max- (f + g)) + (max+ f) is_measurable_on A by A4, Th26; ::_thesis: verum
end;
theorem :: MESFUNC6:79
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL st dom f in S & dom g in S holds
dom (f + g) in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f, g being PartFunc of X,REAL st dom f in S & dom g in S holds
dom (f + g) in S
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL st dom f in S & dom g in S holds
dom (f + g) in S
let f, g be PartFunc of X,REAL; ::_thesis: ( dom f in S & dom g in S implies dom (f + g) in S )
assume ( dom f in S & dom g in S ) ; ::_thesis: dom (f + g) in S
then reconsider E1 = dom f, E2 = dom g as Element of S ;
dom (f + g) = E1 /\ E2 by VALUED_1:def_1;
hence dom (f + g) in S ; ::_thesis: verum
end;
theorem Th80: :: MESFUNC6:80
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A, B being Element of S st dom f = A holds
( f is_measurable_on B iff f is_measurable_on A /\ B )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A, B being Element of S st dom f = A holds
( f is_measurable_on B iff f is_measurable_on A /\ B )
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL
for A, B being Element of S st dom f = A holds
( f is_measurable_on B iff f is_measurable_on A /\ B )
let f be PartFunc of X,REAL; ::_thesis: for A, B being Element of S st dom f = A holds
( f is_measurable_on B iff f is_measurable_on A /\ B )
let A, B be Element of S; ::_thesis: ( dom f = A implies ( f is_measurable_on B iff f is_measurable_on A /\ B ) )
assume A1: dom f = A ; ::_thesis: ( f is_measurable_on B iff f is_measurable_on A /\ B )
A2: now__::_thesis:_for_r_being_real_number_holds_A_/\_(less_dom_(f,r))_=_less_dom_(f,r)
let r be real number ; ::_thesis: A /\ (less_dom (f,r)) = less_dom (f,r)
now__::_thesis:_for_x_being_set_holds_
(_x_in_A_/\_(less_dom_(f,r))_iff_x_in_less_dom_(f,r)_)
let x be set ; ::_thesis: ( x in A /\ (less_dom (f,r)) iff x in less_dom (f,r) )
( x in A /\ (less_dom (f,r)) iff ( x in A & x in less_dom (f,r) ) ) by XBOOLE_0:def_4;
hence ( x in A /\ (less_dom (f,r)) iff x in less_dom (f,r) ) by A1, MESFUNC1:def_11; ::_thesis: verum
end;
then ( A /\ (less_dom (f,r)) c= less_dom (f,r) & less_dom (f,r) c= A /\ (less_dom (f,r)) ) by TARSKI:def_3;
hence A /\ (less_dom (f,r)) = less_dom (f,r) by XBOOLE_0:def_10; ::_thesis: verum
end;
hereby ::_thesis: ( f is_measurable_on A /\ B implies f is_measurable_on B )
assume A3: f is_measurable_on B ; ::_thesis: f is_measurable_on A /\ B
now__::_thesis:_for_r_being_real_number_holds_(A_/\_B)_/\_(less_dom_(f,r))_in_S
let r be real number ; ::_thesis: (A /\ B) /\ (less_dom (f,r)) in S
(A /\ B) /\ (less_dom (f,r)) = B /\ (A /\ (less_dom (f,r))) by XBOOLE_1:16
.= B /\ (less_dom (f,r)) by A2 ;
hence (A /\ B) /\ (less_dom (f,r)) in S by A3, Th12; ::_thesis: verum
end;
hence f is_measurable_on A /\ B by Th12; ::_thesis: verum
end;
assume A4: f is_measurable_on A /\ B ; ::_thesis: f is_measurable_on B
now__::_thesis:_for_r_being_real_number_holds_B_/\_(less_dom_(f,r))_in_S
let r be real number ; ::_thesis: B /\ (less_dom (f,r)) in S
(A /\ B) /\ (less_dom (f,r)) = B /\ (A /\ (less_dom (f,r))) by XBOOLE_1:16
.= B /\ (less_dom (f,r)) by A2 ;
hence B /\ (less_dom (f,r)) in S by A4, Th12; ::_thesis: verum
end;
hence f is_measurable_on B by Th12; ::_thesis: verum
end;
theorem :: MESFUNC6:81
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL st ex A being Element of S st dom f = A holds
for c being Real
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,REAL st ex A being Element of S st dom f = A holds
for c being Real
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL st ex A being Element of S st dom f = A holds
for c being Real
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
let f be PartFunc of X,REAL; ::_thesis: ( ex A being Element of S st dom f = A implies for c being Real
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B )
assume ex A being Element of S st A = dom f ; ::_thesis: for c being Real
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
then consider A being Element of S such that
A1: A = dom f ;
let c be Real; ::_thesis: for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
let B be Element of S; ::_thesis: ( f is_measurable_on B implies c (#) f is_measurable_on B )
assume f is_measurable_on B ; ::_thesis: c (#) f is_measurable_on B
then f is_measurable_on A /\ B by A1, Th80;
then A2: c (#) f is_measurable_on A /\ B by A1, Th21, XBOOLE_1:17;
dom (c (#) f) = A by A1, VALUED_1:def_5;
hence c (#) f is_measurable_on B by A2, Th80; ::_thesis: verum
end;
begin
definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,REAL;
func Integral (M,f) -> Element of ExtREAL equals :: MESFUNC6:def 3
Integral (M,(R_EAL f));
coherence
Integral (M,(R_EAL f)) is Element of ExtREAL ;
end;
:: deftheorem defines Integral MESFUNC6:def_3_:_
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL holds Integral (M,f) = Integral (M,(R_EAL f));
theorem Th82: :: MESFUNC6:82
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative holds
Integral (M,f) = integral+ (M,(R_EAL f))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative holds
Integral (M,f) = integral+ (M,(R_EAL f))
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative holds
Integral (M,f) = integral+ (M,(R_EAL f))
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative holds
Integral (M,f) = integral+ (M,(R_EAL f))
let f be PartFunc of X,REAL; ::_thesis: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative implies Integral (M,f) = integral+ (M,(R_EAL f)) )
assume that
A1: ex A being Element of S st
( A = dom f & f is_measurable_on A ) and
A2: f is nonnegative ; ::_thesis: Integral (M,f) = integral+ (M,(R_EAL f))
consider A being Element of S such that
A3: A = dom f and
A4: f is_measurable_on A by A1;
R_EAL f is_measurable_on A by A4, Def1;
hence Integral (M,f) = integral+ (M,(R_EAL f)) by A2, A3, MESFUNC5:88; ::_thesis: verum
end;
theorem :: MESFUNC6:83
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f is_simple_func_in S & f is nonnegative holds
( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f is_simple_func_in S & f is nonnegative holds
( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st f is_simple_func_in S & f is nonnegative holds
( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st f is_simple_func_in S & f is nonnegative holds
( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) )
let f be PartFunc of X,REAL; ::_thesis: ( f is_simple_func_in S & f is nonnegative implies ( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) ) )
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative ; ::_thesis: ( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) )
A3: R_EAL f is_simple_func_in S by A1, Th49;
then reconsider A = dom (R_EAL f) as Element of S by MESFUNC5:37;
R_EAL f is_measurable_on A by A3, MESFUNC2:34;
then f is_measurable_on A by Def1;
hence Integral (M,f) = integral+ (M,(R_EAL f)) by A2, Th82; ::_thesis: Integral (M,f) = integral' (M,(R_EAL f))
hence Integral (M,f) = integral' (M,(R_EAL f)) by A2, A3, MESFUNC5:77; ::_thesis: verum
end;
theorem :: MESFUNC6:84
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative holds
0 <= Integral (M,f)
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative holds
0 <= Integral (M,f)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative holds
0 <= Integral (M,f)
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative holds
0 <= Integral (M,f)
let f be PartFunc of X,REAL; ::_thesis: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative implies 0 <= Integral (M,f) )
assume that
A1: ex A being Element of S st
( A = dom f & f is_measurable_on A ) and
A2: f is nonnegative ; ::_thesis: 0 <= Integral (M,f)
consider A being Element of S such that
A3: A = dom f and
A4: f is_measurable_on A by A1;
R_EAL f is_measurable_on A by A4, Def1;
hence 0 <= Integral (M,f) by A2, A3, MESFUNC5:90; ::_thesis: verum
end;
theorem :: MESFUNC6:85
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let f be PartFunc of X,REAL; ::_thesis: for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let A, B be Element of S; ::_thesis: ( ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B implies Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
assume that
A1: ex E being Element of S st
( E = dom f & f is_measurable_on E ) and
A2: ( f is nonnegative & A misses B ) ; ::_thesis: Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
consider E being Element of S such that
A3: E = dom f and
A4: f is_measurable_on E by A1;
R_EAL f is_measurable_on E by A4, Def1;
hence Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A2, A3, MESFUNC5:91; ::_thesis: verum
end;
theorem :: MESFUNC6:86
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative holds
0 <= Integral (M,(f | A))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative holds
0 <= Integral (M,(f | A))
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative holds
0 <= Integral (M,(f | A))
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative holds
0 <= Integral (M,(f | A))
let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative holds
0 <= Integral (M,(f | A))
let A be Element of S; ::_thesis: ( ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative implies 0 <= Integral (M,(f | A)) )
assume that
A1: ex E being Element of S st
( E = dom f & f is_measurable_on E ) and
A2: f is nonnegative ; ::_thesis: 0 <= Integral (M,(f | A))
consider E being Element of S such that
A3: E = dom f and
A4: f is_measurable_on E by A1;
R_EAL f is_measurable_on E by A4, Def1;
hence 0 <= Integral (M,(f | A)) by A2, A3, MESFUNC5:92; ::_thesis: verum
end;
theorem :: MESFUNC6:87
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A c= B holds
Integral (M,(f | A)) <= Integral (M,(f | B))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A c= B holds
Integral (M,(f | A)) <= Integral (M,(f | B))
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A c= B holds
Integral (M,(f | A)) <= Integral (M,(f | B))
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A c= B holds
Integral (M,(f | A)) <= Integral (M,(f | B))
let f be PartFunc of X,REAL; ::_thesis: for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A c= B holds
Integral (M,(f | A)) <= Integral (M,(f | B))
let A, B be Element of S; ::_thesis: ( ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A c= B implies Integral (M,(f | A)) <= Integral (M,(f | B)) )
assume that
A1: ex E being Element of S st
( E = dom f & f is_measurable_on E ) and
A2: ( f is nonnegative & A c= B ) ; ::_thesis: Integral (M,(f | A)) <= Integral (M,(f | B))
consider E being Element of S such that
A3: E = dom f and
A4: f is_measurable_on E by A1;
R_EAL f is_measurable_on E by A4, Def1;
hence Integral (M,(f | A)) <= Integral (M,(f | B)) by A2, A3, MESFUNC5:93; ::_thesis: verum
end;
theorem :: MESFUNC6:88
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
Integral (M,(f | A)) = 0
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
Integral (M,(f | A)) = 0
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
Integral (M,(f | A)) = 0
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
Integral (M,(f | A)) = 0
let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
Integral (M,(f | A)) = 0
let A be Element of S; ::_thesis: ( ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 implies Integral (M,(f | A)) = 0 )
assume that
A1: ex E being Element of S st
( E = dom f & f is_measurable_on E ) and
A2: M . A = 0 ; ::_thesis: Integral (M,(f | A)) = 0
consider E being Element of S such that
A3: E = dom f and
A4: f is_measurable_on E by A1;
R_EAL f is_measurable_on E by A4, Def1;
hence Integral (M,(f | A)) = 0 by A2, A3, MESFUNC5:94; ::_thesis: verum
end;
theorem :: MESFUNC6:89
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for E, A being Element of S st E = dom f & f is_measurable_on E & M . A = 0 holds
Integral (M,(f | (E \ A))) = Integral (M,f)
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for E, A being Element of S st E = dom f & f is_measurable_on E & M . A = 0 holds
Integral (M,(f | (E \ A))) = Integral (M,f)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for E, A being Element of S st E = dom f & f is_measurable_on E & M . A = 0 holds
Integral (M,(f | (E \ A))) = Integral (M,f)
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for E, A being Element of S st E = dom f & f is_measurable_on E & M . A = 0 holds
Integral (M,(f | (E \ A))) = Integral (M,f)
let f be PartFunc of X,REAL; ::_thesis: for E, A being Element of S st E = dom f & f is_measurable_on E & M . A = 0 holds
Integral (M,(f | (E \ A))) = Integral (M,f)
let E, A be Element of S; ::_thesis: ( E = dom f & f is_measurable_on E & M . A = 0 implies Integral (M,(f | (E \ A))) = Integral (M,f) )
assume that
A1: E = dom f and
A2: f is_measurable_on E and
A3: M . A = 0 ; ::_thesis: Integral (M,(f | (E \ A))) = Integral (M,f)
R_EAL f is_measurable_on E by A2, Def1;
hence Integral (M,(f | (E \ A))) = Integral (M,f) by A1, A3, MESFUNC5:95; ::_thesis: verum
end;
definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,REAL;
predf is_integrable_on M means :Def4: :: MESFUNC6:def 4
R_EAL f is_integrable_on M;
end;
:: deftheorem Def4 defines is_integrable_on MESFUNC6:def_4_:_
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL holds
( f is_integrable_on M iff R_EAL f is_integrable_on M );
theorem :: MESFUNC6:90
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f is_integrable_on M holds
( -infty < Integral (M,f) & Integral (M,f) < +infty )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f is_integrable_on M holds
( -infty < Integral (M,f) & Integral (M,f) < +infty )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st f is_integrable_on M holds
( -infty < Integral (M,f) & Integral (M,f) < +infty )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st f is_integrable_on M holds
( -infty < Integral (M,f) & Integral (M,f) < +infty )
let f be PartFunc of X,REAL; ::_thesis: ( f is_integrable_on M implies ( -infty < Integral (M,f) & Integral (M,f) < +infty ) )
assume f is_integrable_on M ; ::_thesis: ( -infty < Integral (M,f) & Integral (M,f) < +infty )
then R_EAL f is_integrable_on M by Def4;
hence ( -infty < Integral (M,f) & Integral (M,f) < +infty ) by MESFUNC5:96; ::_thesis: verum
end;
theorem :: MESFUNC6:91
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A being Element of S st f is_integrable_on M holds
f | A is_integrable_on M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A being Element of S st f is_integrable_on M holds
f | A is_integrable_on M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A being Element of S st f is_integrable_on M holds
f | A is_integrable_on M
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for A being Element of S st f is_integrable_on M holds
f | A is_integrable_on M
let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st f is_integrable_on M holds
f | A is_integrable_on M
let A be Element of S; ::_thesis: ( f is_integrable_on M implies f | A is_integrable_on M )
assume f is_integrable_on M ; ::_thesis: f | A is_integrable_on M
then R_EAL f is_integrable_on M by Def4;
then R_EAL (f | A) is_integrable_on M by MESFUNC5:97;
hence f | A is_integrable_on M by Def4; ::_thesis: verum
end;
theorem :: MESFUNC6:92
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A, B being Element of S st f is_integrable_on M & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A, B being Element of S st f is_integrable_on M & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A, B being Element of S st f is_integrable_on M & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for A, B being Element of S st f is_integrable_on M & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let f be PartFunc of X,REAL; ::_thesis: for A, B being Element of S st f is_integrable_on M & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let A, B be Element of S; ::_thesis: ( f is_integrable_on M & A misses B implies Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
assume that
A1: f is_integrable_on M and
A2: A misses B ; ::_thesis: Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
R_EAL f is_integrable_on M by A1, Def4;
hence Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A2, MESFUNC5:98; ::_thesis: verum
end;
theorem :: MESFUNC6:93
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for B, A being Element of S st f is_integrable_on M & B = (dom f) \ A holds
( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for B, A being Element of S st f is_integrable_on M & B = (dom f) \ A holds
( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for B, A being Element of S st f is_integrable_on M & B = (dom f) \ A holds
( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for B, A being Element of S st f is_integrable_on M & B = (dom f) \ A holds
( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
let f be PartFunc of X,REAL; ::_thesis: for B, A being Element of S st f is_integrable_on M & B = (dom f) \ A holds
( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
let B, A be Element of S; ::_thesis: ( f is_integrable_on M & B = (dom f) \ A implies ( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) ) )
assume that
A1: f is_integrable_on M and
A2: B = (dom f) \ A ; ::_thesis: ( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
A3: R_EAL f is_integrable_on M by A1, Def4;
then R_EAL (f | A) is_integrable_on M by A2, MESFUNC5:99;
hence f | A is_integrable_on M by Def4; ::_thesis: Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
thus Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A2, A3, MESFUNC5:99; ::_thesis: verum
end;
theorem :: MESFUNC6:94
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) holds
( f is_integrable_on M iff abs f is_integrable_on M )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) holds
( f is_integrable_on M iff abs f is_integrable_on M )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) holds
( f is_integrable_on M iff abs f is_integrable_on M )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) holds
( f is_integrable_on M iff abs f is_integrable_on M )
let f be PartFunc of X,REAL; ::_thesis: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) implies ( f is_integrable_on M iff abs f is_integrable_on M ) )
assume ex A being Element of S st
( A = dom f & f is_measurable_on A ) ; ::_thesis: ( f is_integrable_on M iff abs f is_integrable_on M )
then consider A being Element of S such that
A1: A = dom f and
A2: f is_measurable_on A ;
R_EAL f is_measurable_on A by A2, Def1;
then ( R_EAL f is_integrable_on M iff |.(R_EAL f).| is_integrable_on M ) by A1, MESFUNC5:100;
then ( f is_integrable_on M iff R_EAL (abs f) is_integrable_on M ) by Def4, Th1;
hence ( f is_integrable_on M iff abs f is_integrable_on M ) by Def4; ::_thesis: verum
end;
theorem :: MESFUNC6:95
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f is_integrable_on M holds
|.(Integral (M,f)).| <= Integral (M,(abs f))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f is_integrable_on M holds
|.(Integral (M,f)).| <= Integral (M,(abs f))
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st f is_integrable_on M holds
|.(Integral (M,f)).| <= Integral (M,(abs f))
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st f is_integrable_on M holds
|.(Integral (M,f)).| <= Integral (M,(abs f))
let f be PartFunc of X,REAL; ::_thesis: ( f is_integrable_on M implies |.(Integral (M,f)).| <= Integral (M,(abs f)) )
assume f is_integrable_on M ; ::_thesis: |.(Integral (M,f)).| <= Integral (M,(abs f))
then R_EAL f is_integrable_on M by Def4;
then |.(Integral (M,f)).| <= Integral (M,|.(R_EAL f).|) by MESFUNC5:101;
hence |.(Integral (M,f)).| <= Integral (M,(abs f)) by Th1; ::_thesis: verum
end;
theorem :: MESFUNC6:96
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds
abs (f . x) <= g . x ) holds
( f is_integrable_on M & Integral (M,(abs f)) <= Integral (M,g) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds
abs (f . x) <= g . x ) holds
( f is_integrable_on M & Integral (M,(abs f)) <= Integral (M,g) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds
abs (f . x) <= g . x ) holds
( f is_integrable_on M & Integral (M,(abs f)) <= Integral (M,g) )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds
abs (f . x) <= g . x ) holds
( f is_integrable_on M & Integral (M,(abs f)) <= Integral (M,g) )
let f, g be PartFunc of X,REAL; ::_thesis: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds
abs (f . x) <= g . x ) implies ( f is_integrable_on M & Integral (M,(abs f)) <= Integral (M,g) ) )
assume that
A1: ex A being Element of S st
( A = dom f & f is_measurable_on A ) and
A2: dom f = dom g and
A3: g is_integrable_on M and
A4: for x being Element of X st x in dom f holds
abs (f . x) <= g . x ; ::_thesis: ( f is_integrable_on M & Integral (M,(abs f)) <= Integral (M,g) )
A5: R_EAL g is_integrable_on M by A3, Def4;
A6: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(R_EAL_f)_holds_
|.((R_EAL_f)_._x).|_<=_(R_EAL_g)_._x
let x be Element of X; ::_thesis: ( x in dom (R_EAL f) implies |.((R_EAL f) . x).| <= (R_EAL g) . x )
A7: abs (f . x) = |.((R_EAL f) . x).| by EXTREAL2:1;
assume x in dom (R_EAL f) ; ::_thesis: |.((R_EAL f) . x).| <= (R_EAL g) . x
hence |.((R_EAL f) . x).| <= (R_EAL g) . x by A4, A7; ::_thesis: verum
end;
consider A being Element of S such that
A8: A = dom f and
A9: f is_measurable_on A by A1;
R_EAL f is_measurable_on A by A9, Def1;
then ( R_EAL f is_integrable_on M & Integral (M,|.(R_EAL f).|) <= Integral (M,(R_EAL g)) ) by A2, A8, A5, A6, MESFUNC5:102;
hence ( f is_integrable_on M & Integral (M,(abs f)) <= Integral (M,g) ) by Def4, Th1; ::_thesis: verum
end;
theorem :: MESFUNC6:97
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for r being Real st dom f in S & 0 <= r & ( for x being set st x in dom f holds
f . x = r ) holds
Integral (M,f) = (R_EAL r) * (M . (dom f))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for r being Real st dom f in S & 0 <= r & ( for x being set st x in dom f holds
f . x = r ) holds
Integral (M,f) = (R_EAL r) * (M . (dom f))
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for r being Real st dom f in S & 0 <= r & ( for x being set st x in dom f holds
f . x = r ) holds
Integral (M,f) = (R_EAL r) * (M . (dom f))
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for r being Real st dom f in S & 0 <= r & ( for x being set st x in dom f holds
f . x = r ) holds
Integral (M,f) = (R_EAL r) * (M . (dom f))
let f be PartFunc of X,REAL; ::_thesis: for r being Real st dom f in S & 0 <= r & ( for x being set st x in dom f holds
f . x = r ) holds
Integral (M,f) = (R_EAL r) * (M . (dom f))
let r be Real; ::_thesis: ( dom f in S & 0 <= r & ( for x being set st x in dom f holds
f . x = r ) implies Integral (M,f) = (R_EAL r) * (M . (dom f)) )
assume that
A1: dom f in S and
A2: 0 <= r and
A3: for x being set st x in dom f holds
f . x = r ; ::_thesis: Integral (M,f) = (R_EAL r) * (M . (dom f))
A4: for x being set st x in dom (R_EAL f) holds
0. <= (R_EAL f) . x by A2, A3;
reconsider A = dom (R_EAL f) as Element of S by A1;
A5: R_EAL f is_measurable_on A by A3, Th2, MESFUNC2:34;
( (R_EAL r) * (M . (dom (R_EAL f))) = integral' (M,(R_EAL f)) & R_EAL f is_simple_func_in S ) by A1, A2, A3, Th2, MESFUNC5:104;
then integral+ (M,(R_EAL f)) = (R_EAL r) * (M . (dom (R_EAL f))) by A4, MESFUNC5:77, SUPINF_2:52;
hence Integral (M,f) = (R_EAL r) * (M . (dom f)) by A4, A5, MESFUNC5:88, SUPINF_2:52; ::_thesis: verum
end;
theorem :: MESFUNC6:98
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is nonnegative holds
f + g is_integrable_on M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is nonnegative holds
f + g is_integrable_on M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is nonnegative holds
f + g is_integrable_on M
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is nonnegative holds
f + g is_integrable_on M
let f, g be PartFunc of X,REAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is nonnegative implies f + g is_integrable_on M )
assume that
A1: ( f is_integrable_on M & g is_integrable_on M ) and
A2: ( f is nonnegative & g is nonnegative ) ; ::_thesis: f + g is_integrable_on M
( R_EAL f is_integrable_on M & R_EAL g is_integrable_on M ) by A1, Def4;
then (R_EAL f) + (R_EAL g) is_integrable_on M by A2, MESFUNC5:106;
then R_EAL (f + g) is_integrable_on M by Th23;
hence f + g is_integrable_on M by Def4; ::_thesis: verum
end;
theorem :: MESFUNC6:99
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
dom (f + g) in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
dom (f + g) in S
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
dom (f + g) in S
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
dom (f + g) in S
let f, g be PartFunc of X,REAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies dom (f + g) in S )
assume ( f is_integrable_on M & g is_integrable_on M ) ; ::_thesis: dom (f + g) in S
then ( R_EAL f is_integrable_on M & R_EAL g is_integrable_on M ) by Def4;
then dom ((R_EAL f) + (R_EAL g)) in S by MESFUNC5:107;
then dom (R_EAL (f + g)) in S by Th23;
hence dom (f + g) in S ; ::_thesis: verum
end;
theorem :: MESFUNC6:100
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
f + g is_integrable_on M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
f + g is_integrable_on M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
f + g is_integrable_on M
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
f + g is_integrable_on M
let f, g be PartFunc of X,REAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies f + g is_integrable_on M )
assume ( f is_integrable_on M & g is_integrable_on M ) ; ::_thesis: f + g is_integrable_on M
then ( R_EAL f is_integrable_on M & R_EAL g is_integrable_on M ) by Def4;
then (R_EAL f) + (R_EAL g) is_integrable_on M by MESFUNC5:108;
then R_EAL (f + g) is_integrable_on M by Th23;
hence f + g is_integrable_on M by Def4; ::_thesis: verum
end;
theorem :: MESFUNC6:101
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )
let f, g be PartFunc of X,REAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) )
assume ( f is_integrable_on M & g is_integrable_on M ) ; ::_thesis: ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )
then ( R_EAL f is_integrable_on M & R_EAL g is_integrable_on M ) by Def4;
then consider E being Element of S such that
A1: ( E = (dom (R_EAL f)) /\ (dom (R_EAL g)) & Integral (M,((R_EAL f) + (R_EAL g))) = (Integral (M,((R_EAL f) | E))) + (Integral (M,((R_EAL g) | E))) ) by MESFUNC5:109;
take E ; ::_thesis: ( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )
thus ( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) by A1, Th23; ::_thesis: verum
end;
theorem :: MESFUNC6:102
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for r being Real st f is_integrable_on M holds
( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = (R_EAL r) * (Integral (M,f)) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for r being Real st f is_integrable_on M holds
( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = (R_EAL r) * (Integral (M,f)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for r being Real st f is_integrable_on M holds
( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = (R_EAL r) * (Integral (M,f)) )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for r being Real st f is_integrable_on M holds
( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = (R_EAL r) * (Integral (M,f)) )
let f be PartFunc of X,REAL; ::_thesis: for r being Real st f is_integrable_on M holds
( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = (R_EAL r) * (Integral (M,f)) )
let r be Real; ::_thesis: ( f is_integrable_on M implies ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = (R_EAL r) * (Integral (M,f)) ) )
assume f is_integrable_on M ; ::_thesis: ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = (R_EAL r) * (Integral (M,f)) )
then A1: R_EAL f is_integrable_on M by Def4;
then r (#) (R_EAL f) is_integrable_on M by MESFUNC5:110;
then A2: R_EAL (r (#) f) is_integrable_on M by Th20;
Integral (M,(r (#) (R_EAL f))) = (R_EAL r) * (Integral (M,(R_EAL f))) by A1, MESFUNC5:110;
hence ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = (R_EAL r) * (Integral (M,f)) ) by A2, Def4, Th20; ::_thesis: verum
end;
definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,REAL;
let B be Element of S;
func Integral_on (M,B,f) -> Element of ExtREAL equals :: MESFUNC6:def 5
Integral (M,(f | B));
coherence
Integral (M,(f | B)) is Element of ExtREAL ;
end;
:: deftheorem defines Integral_on MESFUNC6:def_5_:_
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for B being Element of S holds Integral_on (M,B,f) = Integral (M,(f | B));
theorem :: MESFUNC6:103
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds
( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds
( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds
( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL
for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds
( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
let f, g be PartFunc of X,REAL; ::_thesis: for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds
( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
let B be Element of S; ::_thesis: ( f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) implies ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) ) )
assume that
A1: ( f is_integrable_on M & g is_integrable_on M ) and
A2: B c= dom (f + g) ; ::_thesis: ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
A3: dom (f + g) = dom (R_EAL (f + g))
.= dom ((R_EAL f) + (R_EAL g)) by Th23 ;
A4: ( R_EAL f is_integrable_on M & R_EAL g is_integrable_on M ) by A1, Def4;
then (R_EAL f) + (R_EAL g) is_integrable_on M by A2, A3, MESFUNC5:111;
then A5: R_EAL (f + g) is_integrable_on M by Th23;
Integral_on (M,B,((R_EAL f) + (R_EAL g))) = (Integral_on (M,B,(R_EAL f))) + (Integral_on (M,B,(R_EAL g))) by A2, A4, A3, MESFUNC5:111;
hence ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) ) by A5, Def4, Th23; ::_thesis: verum
end;
theorem :: MESFUNC6:104
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for r being Real
for B being Element of S st f is_integrable_on M holds
( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for r being Real
for B being Element of S st f is_integrable_on M holds
( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for r being Real
for B being Element of S st f is_integrable_on M holds
( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for r being Real
for B being Element of S st f is_integrable_on M holds
( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) )
let f be PartFunc of X,REAL; ::_thesis: for r being Real
for B being Element of S st f is_integrable_on M holds
( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) )
let r be Real; ::_thesis: for B being Element of S st f is_integrable_on M holds
( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) )
let B be Element of S; ::_thesis: ( f is_integrable_on M implies ( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) ) )
assume f is_integrable_on M ; ::_thesis: ( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) )
then A1: R_EAL f is_integrable_on M by Def4;
then Integral_on (M,B,(r (#) (R_EAL f))) = (R_EAL r) * (Integral_on (M,B,(R_EAL f))) by MESFUNC5:112;
then A2: Integral_on (M,B,(R_EAL (r (#) f))) = (R_EAL r) * (Integral_on (M,B,(R_EAL f))) by Th20;
R_EAL (f | B) is_integrable_on M by A1, MESFUNC5:112;
hence ( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) ) by A2, Def4; ::_thesis: verum
end;