:: MESFUNC2 semantic presentation
begin
definition
let X be non empty set ;
let f be PartFunc of X,ExtREAL;
:: original: real-valued
redefine attrf is real-valued means :Def1: :: MESFUNC2:def 1
for x being Element of X st x in dom f holds
|.(f . x).| < +infty ;
compatibility
( f is real-valued iff for x being Element of X st x in dom f holds
|.(f . x).| < +infty )
proof
thus ( f is real-valued implies for x being Element of X st x in dom f holds
|.(f . x).| < +infty ) ::_thesis: ( ( for x being Element of X st x in dom f holds
|.(f . x).| < +infty ) implies f is real-valued )
proof
assume A1: f is real-valued ; ::_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 A2: f . x in rng f by FUNCT_1:3;
rng f c= REAL by A1, VALUED_0:def_3;
hence |.(f . x).| < +infty by A2, EXTREAL2:30; ::_thesis: verum
end;
assume A3: for x being Element of X st x in dom f holds
|.(f . x).| < +infty ; ::_thesis: f is real-valued
let e be set ; :: according to VALUED_0:def_9 ::_thesis: ( not e in dom f or f . e is real )
assume A4: e in dom f ; ::_thesis: f . e is real
then reconsider x = e as Element of X ;
|.(f . x).| < +infty by A3, A4;
then f . x in REAL by EXTREAL2:30;
hence f . e is real ; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines real-valued MESFUNC2:def_1_:_
for X being non empty set
for f being PartFunc of X,ExtREAL holds
( f is real-valued iff for x being Element of X st x in dom f holds
|.(f . x).| < +infty );
theorem :: MESFUNC2:1
for X being non empty set
for f being PartFunc of X,ExtREAL holds f = 1 (#) f
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,ExtREAL holds f = 1 (#) f
let f be PartFunc of X,ExtREAL; ::_thesis: f = 1 (#) f
A1: dom f = dom (1 (#) f) by MESFUNC1:def_6;
for x being Element of X st x in dom (1 (#) f) holds
f . x = (1 (#) f) . x
proof
let x be Element of X; ::_thesis: ( x in dom (1 (#) f) implies f . x = (1 (#) f) . x )
assume x in dom (1 (#) f) ; ::_thesis: f . x = (1 (#) f) . x
then (1 (#) f) . x = (R_EAL 1) * (f . x) by MESFUNC1:def_6;
hence f . x = (1 (#) f) . x by XXREAL_3:81; ::_thesis: verum
end;
hence f = 1 (#) f by A1, PARTFUN1:5; ::_thesis: verum
end;
theorem Th2: :: MESFUNC2:2
for X being non empty set
for f, g being PartFunc of X,ExtREAL st ( not f is V75() or not g is V75() ) holds
( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) )
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,ExtREAL st ( not f is V75() or not g is V75() ) holds
( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) )
let f, g be PartFunc of X,ExtREAL; ::_thesis: ( ( not f is V75() or not g is V75() ) implies ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) )
assume A1: ( not f is V75() or not g is V75() ) ; ::_thesis: ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) )
now__::_thesis:_(_dom_(f_+_g)_=_(dom_f)_/\_(dom_g)_&_dom_(f_-_g)_=_(dom_f)_/\_(dom_g)_)
percases ( not f is V75() or not g is V75() ) by A1;
supposeA2: f is V75() ; ::_thesis: ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) )
then not +infty in rng f ;
then A3: f " {+infty} = {} by FUNCT_1:72;
not -infty in rng f by A2;
then A4: f " {-infty} = {} by FUNCT_1:72;
then A5: ((f " {+infty}) /\ (g " {-infty})) \/ ((f " {-infty}) /\ (g " {+infty})) = {} by A3;
A6: ((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty})) = {} by A3, A4;
dom (f + g) = ((dom f) /\ (dom g)) \ {} by A5, MESFUNC1:def_3;
hence ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) by A6, MESFUNC1:def_4; ::_thesis: verum
end;
supposeA7: g is V75() ; ::_thesis: ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) )
then not +infty in rng g ;
then A8: g " {+infty} = {} by FUNCT_1:72;
not -infty in rng g by A7;
then A9: g " {-infty} = {} by FUNCT_1:72;
then A10: ((f " {+infty}) /\ (g " {-infty})) \/ ((f " {-infty}) /\ (g " {+infty})) = {} by A8;
A11: ((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty})) = {} by A8, A9;
dom (f + g) = ((dom f) /\ (dom g)) \ {} by A10, MESFUNC1:def_3;
hence ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) by A11, MESFUNC1:def_4; ::_thesis: verum
end;
end;
end;
hence ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) ; ::_thesis: verum
end;
theorem Th3: :: MESFUNC2:3
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for F being Function of RAT,S
for r being Real
for A being Element of S st f is V75() & g is V75() & ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) holds
A /\ (less_dom ((f + g),(R_EAL 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,ExtREAL
for F being Function of RAT,S
for r being Real
for A being Element of S st f is V75() & g is V75() & ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) holds
A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F)
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,ExtREAL
for F being Function of RAT,S
for r being Real
for A being Element of S st f is V75() & g is V75() & ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) holds
A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F)
let f, g be PartFunc of X,ExtREAL; ::_thesis: for F being Function of RAT,S
for r being Real
for A being Element of S st f is V75() & g is V75() & ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) holds
A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F)
let F be Function of RAT,S; ::_thesis: for r being Real
for A being Element of S st f is V75() & g is V75() & ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) holds
A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F)
let r be Real; ::_thesis: for A being Element of S st f is V75() & g is V75() & ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) holds
A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F)
let A be Element of S; ::_thesis: ( f is V75() & g is V75() & ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) implies A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F) )
assume that
A1: f is V75() and
A2: g is V75() and
A3: for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ; ::_thesis: A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F)
A4: dom (f + g) = (dom f) /\ (dom g) by A1, Th2;
A5: A /\ (less_dom ((f + g),(R_EAL r))) c= union (rng F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A /\ (less_dom ((f + g),(R_EAL r))) or x in union (rng F) )
assume A6: x in A /\ (less_dom ((f + g),(R_EAL r))) ; ::_thesis: x in union (rng F)
then A7: x in A by XBOOLE_0:def_4;
A8: x in less_dom ((f + g),(R_EAL r)) by A6, XBOOLE_0:def_4;
then A9: x in dom (f + g) by MESFUNC1:def_11;
A10: (f + g) . x < R_EAL r by A8, MESFUNC1:def_11;
reconsider x = x as Element of X by A6;
A11: (f . x) + (g . x) < R_EAL r by A9, A10, MESFUNC1:def_3;
A12: x in dom f by A4, A9, XBOOLE_0:def_4;
A13: x in dom g by A4, A9, XBOOLE_0:def_4;
A14: |.(f . x).| < +infty by A1, A12, Def1;
A15: |.(g . x).| < +infty by A2, A13, Def1;
A16: - +infty < f . x by A14, EXTREAL2:10;
A17: f . x < +infty by A14, EXTREAL2:10;
A18: - +infty < g . x by A15, EXTREAL2:10;
A19: g . x < +infty by A15, EXTREAL2:10;
then A20: f . x < (R_EAL r) - (g . x) by A11, A17, XXREAL_3:52;
A21: -infty < f . x by A16, XXREAL_3:23;
A22: -infty < g . x by A18, XXREAL_3:23;
reconsider f1 = f . x as Real by A17, A21, XXREAL_0:14;
reconsider g1 = g . x as Real by A19, A22, XXREAL_0:14;
(R_EAL r) - (g . x) = r - g1 by SUPINF_2:3;
then consider p being Rational such that
A23: f1 < p and
A24: p < r - g1 by A20, RAT_1:7;
A25: not r - p <= g1 by A24, XREAL_1:12;
A26: x in less_dom (f,(R_EAL p)) by A12, A23, MESFUNC1:def_11;
A27: x in less_dom (g,(R_EAL (r - p))) by A13, A25, MESFUNC1:def_11;
A28: x in A /\ (less_dom (f,(R_EAL p))) by A7, A26, XBOOLE_0:def_4;
x in A /\ (less_dom (g,(R_EAL (r - p)))) by A7, A27, XBOOLE_0:def_4;
then A29: x in (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) by A28, XBOOLE_0:def_4;
p in RAT by RAT_1:def_2;
then A30: p in dom F by FUNCT_2:def_1;
A31: x in F . p by A3, A29;
F . p in rng F by A30, FUNCT_1:def_3;
hence x in union (rng F) by A31, TARSKI:def_4; ::_thesis: verum
end;
union (rng F) c= A /\ (less_dom ((f + g),(R_EAL r)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng F) or x in A /\ (less_dom ((f + g),(R_EAL r))) )
assume x in union (rng F) ; ::_thesis: x in A /\ (less_dom ((f + g),(R_EAL r)))
then consider Y being set such that
A32: x in Y and
A33: Y in rng F by TARSKI:def_4;
consider p being set such that
A34: p in dom F and
A35: Y = F . p by A33, FUNCT_1:def_3;
reconsider p = p as Rational by A34;
A36: x in (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) by A3, A32, A35;
then A37: x in A /\ (less_dom (f,(R_EAL p))) by XBOOLE_0:def_4;
A38: x in A /\ (less_dom (g,(R_EAL (r - p)))) by A36, XBOOLE_0:def_4;
A39: x in A by A37, XBOOLE_0:def_4;
A40: x in less_dom (f,(R_EAL p)) by A37, XBOOLE_0:def_4;
A41: x in less_dom (g,(R_EAL (r - p))) by A38, XBOOLE_0:def_4;
A42: x in dom f by A40, MESFUNC1:def_11;
A43: x in dom g by A41, MESFUNC1:def_11;
reconsider x = x as Element of X by A36;
A44: g . x < R_EAL (r - p) by A41, MESFUNC1:def_11;
A45: |.(f . x).| < +infty by A1, A42, Def1;
A46: |.(g . x).| < +infty by A2, A43, Def1;
A47: - +infty < f . x by A45, EXTREAL2:10;
A48: - +infty < g . x by A46, EXTREAL2:10;
A49: -infty < f . x by A47, XXREAL_3:23;
A50: f . x < +infty by A45, EXTREAL2:10;
A51: -infty < g . x by A48, XXREAL_3:23;
A52: g . x < +infty by A46, EXTREAL2:10;
reconsider f1 = f . x as Real by A49, A50, XXREAL_0:14;
reconsider g1 = g . x as Real by A51, A52, XXREAL_0:14;
A53: f1 < p by A40, MESFUNC1:def_11;
p < r - g1 by A44, XREAL_1:12;
then f1 < r - g1 by A53, XXREAL_0:2;
then A54: f1 + g1 < r by XREAL_1:20;
A55: x in dom (f + g) by A4, A42, A43, XBOOLE_0:def_4;
then (f + g) . x = (f . x) + (g . x) by MESFUNC1:def_3
.= f1 + g1 by SUPINF_2:1 ;
then x in less_dom ((f + g),(R_EAL r)) by A54, A55, MESFUNC1:def_11;
hence x in A /\ (less_dom ((f + g),(R_EAL r))) by A39, XBOOLE_0:def_4; ::_thesis: verum
end;
hence A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F) by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
theorem :: MESFUNC2:4
ex F being Function of NAT,RAT st
( F is one-to-one & dom F = NAT & rng F = RAT )
proof
consider F being Function such that
A1: F is one-to-one and
A2: ( dom F = NAT & rng F = RAT ) by MESFUNC1:5, WELLORD2:def_4;
F is Function of NAT,RAT by A2, FUNCT_2:2;
hence ex F being Function of NAT,RAT st
( F is one-to-one & dom F = NAT & rng F = RAT ) by A1, A2; ::_thesis: verum
end;
theorem Th5: :: MESFUNC2:5
for X, Y, Z being non empty set
for F being Function of X,Z st X,Y are_equipotent holds
ex G being Function of Y,Z st rng F = rng G
proof
let X, Y, Z be non empty set ; ::_thesis: for F being Function of X,Z st X,Y are_equipotent holds
ex G being Function of Y,Z st rng F = rng G
let F be Function of X,Z; ::_thesis: ( X,Y are_equipotent implies ex G being Function of Y,Z st rng F = rng G )
assume X,Y are_equipotent ; ::_thesis: ex G being Function of Y,Z st rng F = rng G
then consider H being Function such that
A1: H is one-to-one and
A2: dom H = Y and
A3: rng H = X by WELLORD2:def_4;
reconsider H = H as Function of Y,X by A2, A3, FUNCT_2:2;
reconsider G = F * H as Function of Y,Z ;
A4: dom F = X by FUNCT_2:def_1;
A5: dom G = Y by FUNCT_2:def_1;
for z being Element of Z st z in rng F holds
z in rng G
proof
let z be Element of Z; ::_thesis: ( z in rng F implies z in rng G )
assume z in rng F ; ::_thesis: z in rng G
then consider x being set such that
A6: x in dom F and
A7: z = F . x by FUNCT_1:def_3;
x in rng H by A3, A6;
then x in dom (H ") by A1, FUNCT_1:32;
then (H ") . x in rng (H ") by FUNCT_1:def_3;
then A8: (H ") . x in dom G by A1, A2, A5, FUNCT_1:33;
then G . ((H ") . x) in rng G by FUNCT_1:def_3;
then F . (H . ((H ") . x)) in rng G by A8, FUNCT_1:12;
hence z in rng G by A1, A3, A6, A7, FUNCT_1:35; ::_thesis: verum
end;
then A9: rng F c= rng G by SUBSET_1:2;
for z being Element of Z st z in rng G holds
z in rng F
proof
let z be Element of Z; ::_thesis: ( z in rng G implies z in rng F )
assume z in rng G ; ::_thesis: z in rng F
then consider y being set such that
A10: y in dom G and
A11: z = G . y by FUNCT_1:def_3;
y in rng (H ") by A1, A2, A5, A10, FUNCT_1:33;
then consider x being set such that
A12: x in dom (H ") and
A13: y = (H ") . x by FUNCT_1:def_3;
A14: x in rng H by A1, A12, FUNCT_1:33;
then A15: F . x in rng F by A4, FUNCT_1:def_3;
x = H . y by A1, A13, A14, FUNCT_1:32;
hence z in rng F by A10, A11, A15, FUNCT_1:12; ::_thesis: verum
end;
then rng G c= rng F by SUBSET_1:2;
then rng F = rng G by A9, XBOOLE_0:def_10;
hence ex G being Function of Y,Z st rng F = rng G ; ::_thesis: verum
end;
theorem Th6: :: MESFUNC2:6
for X being non empty set
for r being Real
for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for A being Element of S 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,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p)))))
proof
let X be non empty set ; ::_thesis: for r being Real
for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for A being Element of S 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,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p)))))
let r be Real; ::_thesis: for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for A being Element of S 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,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p)))))
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,ExtREAL
for A being Element of S 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,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p)))))
let f, g be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S 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,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p)))))
let A be Element of S; ::_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,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) )
assume A1: ( 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,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p)))))
defpred S1[ set , set ] means ex p being Rational st
( p = $1 & $2 = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) );
A2: for x1 being set st x1 in RAT holds
ex y1 being set st
( y1 in S & S1[x1,y1] )
proof
let x1 be set ; ::_thesis: ( x1 in RAT implies ex y1 being set st
( y1 in S & S1[x1,y1] ) )
assume x1 in RAT ; ::_thesis: ex y1 being set st
( y1 in S & S1[x1,y1] )
then consider p being Rational such that
A3: p = x1 ;
A4: ( A /\ (less_dom (f,(R_EAL p))) in S & A /\ (less_dom (g,(R_EAL (r - p)))) in S ) by A1, MESFUNC1:def_16;
take (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ; ::_thesis: ( (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) in S & S1[x1,(A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p)))))] )
thus ( (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) in S & S1[x1,(A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p)))))] ) by A3, A4, FINSUB_1:def_2; ::_thesis: verum
end;
consider G being Function of RAT,S such that
A5: for x1 being set st x1 in RAT holds
S1[x1,G . x1] from FUNCT_2:sch_1(A2);
A6: for p being Rational holds G . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p)))))
proof
let p be Rational; ::_thesis: G . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p)))))
p in RAT by RAT_1:def_2;
then ex q being Rational st
( q = p & G . p = (A /\ (less_dom (f,(R_EAL q)))) /\ (A /\ (less_dom (g,(R_EAL (r - q))))) ) by A5;
hence G . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ; ::_thesis: verum
end;
take G ; ::_thesis: for p being Rational holds G . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p)))))
thus for p being Rational holds G . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) by A6; ::_thesis: verum
end;
theorem Th7: :: MESFUNC2:7
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for A being Element of S st f is V75() & g is V75() & 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,ExtREAL
for A being Element of S st f is V75() & g is V75() & 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,ExtREAL
for A being Element of S st f is V75() & g is V75() & f is_measurable_on A & g is_measurable_on A holds
f + g is_measurable_on A
let f, g be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S st f is V75() & g is V75() & 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 V75() & g is V75() & f is_measurable_on A & g is_measurable_on A implies f + g is_measurable_on A )
assume that
A1: ( f is V75() & g is V75() ) and
A2: ( f is_measurable_on A & g is_measurable_on A ) ; ::_thesis: f + g is_measurable_on A
for r being real number holds A /\ (less_dom ((f + g),(R_EAL r))) in S
proof
let r be real number ; ::_thesis: A /\ (less_dom ((f + g),(R_EAL r))) in S
reconsider r = r as Real by XREAL_0:def_1;
consider F being Function of RAT,S such that
A3: for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) by A2, Th6;
consider G being Function of NAT,S such that
A4: rng F = rng G by Th5, MESFUNC1:5;
A /\ (less_dom ((f + g),(R_EAL r))) = union (rng G) by A1, A3, A4, Th3;
hence A /\ (less_dom ((f + g),(R_EAL r))) in S ; ::_thesis: verum
end;
hence f + g is_measurable_on A by MESFUNC1:def_16; ::_thesis: verum
end;
theorem Th8: :: MESFUNC2:8
for C being non empty set
for f1, f2 being PartFunc of C,ExtREAL holds f1 - f2 = f1 + (- f2)
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,ExtREAL holds f1 - f2 = f1 + (- f2)
let f1, f2 be PartFunc of C,ExtREAL; ::_thesis: f1 - f2 = f1 + (- f2)
A1: dom (f1 - f2) = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) by MESFUNC1:def_4;
for x being Element of C st x in f2 " {+infty} holds
x in (- f2) " {-infty}
proof
let x be Element of C; ::_thesis: ( x in f2 " {+infty} implies x in (- f2) " {-infty} )
assume A2: x in f2 " {+infty} ; ::_thesis: x in (- f2) " {-infty}
then A3: x in dom f2 by FUNCT_1:def_7;
A4: f2 . x in {+infty} by A2, FUNCT_1:def_7;
A5: x in dom (- f2) by A3, MESFUNC1:def_7;
f2 . x = +infty by A4, TARSKI:def_1;
then (- f2) . x = - +infty by A5, MESFUNC1:def_7
.= -infty by XXREAL_3:def_3 ;
then (- f2) . x in {-infty} by TARSKI:def_1;
hence x in (- f2) " {-infty} by A5, FUNCT_1:def_7; ::_thesis: verum
end;
then A6: f2 " {+infty} c= (- f2) " {-infty} by SUBSET_1:2;
for x being Element of C st x in (- f2) " {-infty} holds
x in f2 " {+infty}
proof
let x be Element of C; ::_thesis: ( x in (- f2) " {-infty} implies x in f2 " {+infty} )
assume A7: x in (- f2) " {-infty} ; ::_thesis: x in f2 " {+infty}
then A8: x in dom (- f2) by FUNCT_1:def_7;
A9: (- f2) . x in {-infty} by A7, FUNCT_1:def_7;
A10: x in dom f2 by A8, MESFUNC1:def_7;
(- f2) . x = -infty by A9, TARSKI:def_1;
then -infty = - (f2 . x) by A8, MESFUNC1:def_7;
then f2 . x in {+infty} by TARSKI:def_1, XXREAL_3:5;
hence x in f2 " {+infty} by A10, FUNCT_1:def_7; ::_thesis: verum
end;
then (- f2) " {-infty} c= f2 " {+infty} by SUBSET_1:2;
then A11: f2 " {+infty} = (- f2) " {-infty} by A6, XBOOLE_0:def_10;
for x being Element of C st x in f2 " {-infty} holds
x in (- f2) " {+infty}
proof
let x be Element of C; ::_thesis: ( x in f2 " {-infty} implies x in (- f2) " {+infty} )
assume A12: x in f2 " {-infty} ; ::_thesis: x in (- f2) " {+infty}
then A13: x in dom f2 by FUNCT_1:def_7;
A14: f2 . x in {-infty} by A12, FUNCT_1:def_7;
A15: x in dom (- f2) by A13, MESFUNC1:def_7;
f2 . x = -infty by A14, TARSKI:def_1;
then (- f2) . x = +infty by A15, MESFUNC1:def_7, XXREAL_3:5;
then (- f2) . x in {+infty} by TARSKI:def_1;
hence x in (- f2) " {+infty} by A15, FUNCT_1:def_7; ::_thesis: verum
end;
then A16: f2 " {-infty} c= (- f2) " {+infty} by SUBSET_1:2;
for x being Element of C st x in (- f2) " {+infty} holds
x in f2 " {-infty}
proof
let x be Element of C; ::_thesis: ( x in (- f2) " {+infty} implies x in f2 " {-infty} )
assume A17: x in (- f2) " {+infty} ; ::_thesis: x in f2 " {-infty}
then A18: x in dom (- f2) by FUNCT_1:def_7;
A19: (- f2) . x in {+infty} by A17, FUNCT_1:def_7;
A20: x in dom f2 by A18, MESFUNC1:def_7;
(- f2) . x = +infty by A19, TARSKI:def_1;
then +infty = - (f2 . x) by A18, MESFUNC1:def_7;
then f2 . x = - +infty
.= -infty by XXREAL_3:def_3 ;
then f2 . x in {-infty} by TARSKI:def_1;
hence x in f2 " {-infty} by A20, FUNCT_1:def_7; ::_thesis: verum
end;
then (- f2) " {+infty} c= f2 " {-infty} by SUBSET_1:2;
then A21: f2 " {-infty} = (- f2) " {+infty} by A16, XBOOLE_0:def_10;
dom (f1 + (- f2)) = ((dom f1) /\ (dom (- f2))) \ (((f1 " {-infty}) /\ ((- f2) " {+infty})) \/ ((f1 " {+infty}) /\ ((- f2) " {-infty}))) by MESFUNC1:def_3
.= ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {-infty})) \/ ((f1 " {+infty}) /\ (f2 " {+infty}))) by A11, A21, MESFUNC1:def_7 ;
then A22: dom (f1 - f2) = dom (f1 + (- f2)) by MESFUNC1:def_4;
for x being Element of C st x in dom (f1 - f2) holds
(f1 - f2) . x = (f1 + (- f2)) . x
proof
let x be Element of C; ::_thesis: ( x in dom (f1 - f2) implies (f1 - f2) . x = (f1 + (- f2)) . x )
assume A23: x in dom (f1 - f2) ; ::_thesis: (f1 - f2) . x = (f1 + (- f2)) . x
dom (f1 - f2) c= (dom f1) /\ (dom f2) by A1, XBOOLE_1:36;
then x in dom f2 by A23, XBOOLE_0:def_4;
then A24: x in dom (- f2) by MESFUNC1:def_7;
( (f1 - f2) . x = (f1 . x) - (f2 . x) & (f1 + (- f2)) . x = (f1 . x) + ((- f2) . x) ) by A22, A23, MESFUNC1:def_3, MESFUNC1:def_4;
hence (f1 - f2) . x = (f1 + (- f2)) . x by A24, MESFUNC1:def_7; ::_thesis: verum
end;
hence f1 - f2 = f1 + (- f2) by A22, PARTFUN1:5; ::_thesis: verum
end;
theorem Th9: :: MESFUNC2:9
for C being non empty set
for f being PartFunc of C,ExtREAL holds - f = (- 1) (#) f
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL holds - f = (- 1) (#) f
let f be PartFunc of C,ExtREAL; ::_thesis: - f = (- 1) (#) f
A1: dom (- f) = dom f by MESFUNC1:def_7;
A2: dom ((- 1) (#) f) = dom f by MESFUNC1:def_6;
for x being Element of C st x in dom f holds
(- f) . x = ((- 1) (#) f) . x
proof
let x be Element of C; ::_thesis: ( x in dom f implies (- f) . x = ((- 1) (#) f) . x )
assume A3: x in dom f ; ::_thesis: (- f) . x = ((- 1) (#) f) . x
then ((- 1) (#) f) . x = (R_EAL (- 1)) * (f . x) by A2, MESFUNC1:def_6;
then ((- 1) (#) f) . x = (- (R_EAL 1)) * (f . x) by SUPINF_2:2
.= - ((R_EAL 1) * (f . x)) by XXREAL_3:92
.= - (f . x) by XXREAL_3:81 ;
hence (- f) . x = ((- 1) (#) f) . x by A1, A3, MESFUNC1:def_7; ::_thesis: verum
end;
hence - f = (- 1) (#) f by A1, A2, PARTFUN1:5; ::_thesis: verum
end;
theorem Th10: :: MESFUNC2:10
for C being non empty set
for f being PartFunc of C,ExtREAL
for r being Real st f is V75() holds
r (#) f is V75()
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL
for r being Real st f is V75() holds
r (#) f is V75()
let f be PartFunc of C,ExtREAL; ::_thesis: for r being Real st f is V75() holds
r (#) f is V75()
let r be Real; ::_thesis: ( f is V75() implies r (#) f is V75() )
assume A1: f is V75() ; ::_thesis: r (#) f is V75()
for x being Element of C st x in dom (r (#) f) holds
|.((r (#) f) . x).| < +infty
proof
let x be Element of C; ::_thesis: ( x in dom (r (#) f) implies |.((r (#) f) . x).| < +infty )
assume A2: x in dom (r (#) f) ; ::_thesis: |.((r (#) f) . x).| < +infty
then x in dom f by MESFUNC1:def_6;
then A3: |.(f . x).| < +infty by A1, Def1;
then - +infty < f . x by EXTREAL2:10;
then A4: -infty < f . x by XXREAL_3:def_3;
f . x < +infty by A3, EXTREAL2:10;
then reconsider y = f . x as Real by A4, XXREAL_0:14;
A5: -infty < R_EAL (r * y) by XXREAL_0:12;
A6: R_EAL (r * y) < +infty by XXREAL_0:9;
A7: -infty < (R_EAL r) * (R_EAL y) by A5, EXTREAL1:5;
A8: (R_EAL r) * (R_EAL y) = (r (#) f) . x by A2, MESFUNC1:def_6;
then A9: - +infty < (r (#) f) . x by A7, XXREAL_3:def_3;
(r (#) f) . x < +infty by A6, A8, EXTREAL1:5;
hence |.((r (#) f) . x).| < +infty by A9, EXTREAL2:11; ::_thesis: verum
end;
hence r (#) f is V75() by Def1; ::_thesis: verum
end;
theorem :: MESFUNC2:11
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for A being Element of S st f is V75() & g is V75() & 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,ExtREAL
for A being Element of S st f is V75() & g is V75() & 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,ExtREAL
for A being Element of S st f is V75() & g is V75() & 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,ExtREAL; ::_thesis: for A being Element of S st f is V75() & g is V75() & 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 V75() & g is V75() & 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 V75() and
A2: g is V75() and
A3: f is_measurable_on A and
A4: ( g is_measurable_on A & A c= dom g ) ; ::_thesis: f - g is_measurable_on A
A5: (- 1) (#) g is V75() by A2, Th10;
A6: (- 1) (#) g is_measurable_on A by A4, MESFUNC1:37;
A7: - g is V75() by A5, Th9;
- g is_measurable_on A by A6, Th9;
then f + (- g) is_measurable_on A by A1, A3, A7, Th7;
hence f - g is_measurable_on A by Th8; ::_thesis: verum
end;
begin
definition
let C be non empty set ;
let f be PartFunc of C,ExtREAL;
deffunc H1( Element of C) -> Element of ExtREAL = max ((f . $1),0.);
func max+ f -> PartFunc of C,ExtREAL means :Def2: :: MESFUNC2:def 2
( dom it = dom f & ( for x being Element of C st x in dom it holds
it . x = max ((f . x),0.) ) );
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = dom f & ( for x being Element of C st x in dom b1 holds
b1 . x = max ((f . x),0.) ) )
proof
defpred S1[ Element of C] means $1 in dom f;
consider F being PartFunc of C,ExtREAL such that
A1: for c being Element of C holds
( c in dom F iff S1[c] ) and
A2: for c being Element of C st c in dom F holds
F . c = H1(c) from SEQ_1:sch_3();
take F ; ::_thesis: ( dom F = dom f & ( for x being Element of C st x in dom F holds
F . x = max ((f . x),0.) ) )
thus dom F = dom f ::_thesis: for x being Element of C st x in dom F holds
F . x = max ((f . x),0.)
proof
thus dom F c= dom f :: according to XBOOLE_0:def_10 ::_thesis: dom f c= dom F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom F or x in dom f )
assume x in dom F ; ::_thesis: x in dom f
hence x in dom f by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in dom F )
assume x in dom f ; ::_thesis: x in dom F
hence x in dom F by A1; ::_thesis: verum
end;
let c be Element of C; ::_thesis: ( c in dom F implies F . c = max ((f . c),0.) )
assume c in dom F ; ::_thesis: F . c = max ((f . c),0.)
hence F . c = max ((f . c),0.) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = dom f & ( for x being Element of C st x in dom b1 holds
b1 . x = max ((f . x),0.) ) & dom b2 = dom f & ( for x being Element of C st x in dom b2 holds
b2 . x = max ((f . x),0.) ) holds
b1 = b2
proof
set X = dom f;
thus for F, G being PartFunc of C,ExtREAL st dom F = dom f & ( for c being Element of C st c in dom F holds
F . c = H1(c) ) & dom G = dom f & ( for c being Element of C st c in dom G holds
G . c = H1(c) ) holds
F = G from SEQ_1:sch_4(); ::_thesis: verum
end;
deffunc H2( Element of C) -> Element of ExtREAL = max ((- (f . $1)),0.);
func max- f -> PartFunc of C,ExtREAL means :Def3: :: MESFUNC2:def 3
( dom it = dom f & ( for x being Element of C st x in dom it holds
it . x = max ((- (f . x)),0.) ) );
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = dom f & ( for x being Element of C st x in dom b1 holds
b1 . x = max ((- (f . x)),0.) ) )
proof
defpred S1[ Element of C] means $1 in dom f;
consider F being PartFunc of C,ExtREAL such that
A3: for c being Element of C holds
( c in dom F iff S1[c] ) and
A4: for c being Element of C st c in dom F holds
F . c = H2(c) from SEQ_1:sch_3();
take F ; ::_thesis: ( dom F = dom f & ( for x being Element of C st x in dom F holds
F . x = max ((- (f . x)),0.) ) )
thus dom F = dom f ::_thesis: for x being Element of C st x in dom F holds
F . x = max ((- (f . x)),0.)
proof
thus dom F c= dom f :: according to XBOOLE_0:def_10 ::_thesis: dom f c= dom F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom F or x in dom f )
assume x in dom F ; ::_thesis: x in dom f
hence x in dom f by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in dom F )
assume x in dom f ; ::_thesis: x in dom F
hence x in dom F by A3; ::_thesis: verum
end;
let c be Element of C; ::_thesis: ( c in dom F implies F . c = max ((- (f . c)),0.) )
assume c in dom F ; ::_thesis: F . c = max ((- (f . c)),0.)
hence F . c = max ((- (f . c)),0.) by A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = dom f & ( for x being Element of C st x in dom b1 holds
b1 . x = max ((- (f . x)),0.) ) & dom b2 = dom f & ( for x being Element of C st x in dom b2 holds
b2 . x = max ((- (f . x)),0.) ) holds
b1 = b2
proof
set X = dom f;
thus for F, G being PartFunc of C,ExtREAL st dom F = dom f & ( for c being Element of C st c in dom F holds
F . c = H2(c) ) & dom G = dom f & ( for c being Element of C st c in dom G holds
G . c = H2(c) ) holds
F = G from SEQ_1:sch_4(); ::_thesis: verum
end;
end;
:: deftheorem Def2 defines max+ MESFUNC2:def_2_:_
for C being non empty set
for f, b3 being PartFunc of C,ExtREAL holds
( b3 = max+ f iff ( dom b3 = dom f & ( for x being Element of C st x in dom b3 holds
b3 . x = max ((f . x),0.) ) ) );
:: deftheorem Def3 defines max- MESFUNC2:def_3_:_
for C being non empty set
for f, b3 being PartFunc of C,ExtREAL holds
( b3 = max- f iff ( dom b3 = dom f & ( for x being Element of C st x in dom b3 holds
b3 . x = max ((- (f . x)),0.) ) ) );
theorem Th12: :: MESFUNC2:12
for C being non empty set
for f being PartFunc of C,ExtREAL
for x being Element of C holds 0. <= (max+ f) . x
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL
for x being Element of C holds 0. <= (max+ f) . x
let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C holds 0. <= (max+ f) . x
let x be Element of C; ::_thesis: 0. <= (max+ f) . x
A1: dom (max+ f) = dom f by Def2;
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: 0. <= (max+ f) . x
then (max+ f) . x = max ((f . x),0.) by A1, Def2;
hence 0. <= (max+ f) . x by XXREAL_0:25; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: 0. <= (max+ f) . x
hence 0. <= (max+ f) . x by A1, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
theorem Th13: :: MESFUNC2:13
for C being non empty set
for f being PartFunc of C,ExtREAL
for x being Element of C holds 0. <= (max- f) . x
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL
for x being Element of C holds 0. <= (max- f) . x
let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C holds 0. <= (max- f) . x
let x be Element of C; ::_thesis: 0. <= (max- f) . x
A1: dom (max- f) = dom f by Def3;
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: 0. <= (max- f) . x
then (max- f) . x = max ((- (f . x)),0.) by A1, Def3;
hence 0. <= (max- f) . x by XXREAL_0:25; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: 0. <= (max- f) . x
hence 0. <= (max- f) . x by A1, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
theorem :: MESFUNC2:14
for C being non empty set
for f being PartFunc of C,ExtREAL holds max- f = max+ (- f)
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL holds max- f = max+ (- f)
let f be PartFunc of C,ExtREAL; ::_thesis: max- f = max+ (- f)
A1: dom (max- f) = dom f by Def3
.= dom (- f) by MESFUNC1:def_7 ;
then A2: dom (max- f) = dom (max+ (- f)) by Def2;
for x being Element of C st x in dom (max- f) holds
(max- f) . x = (max+ (- f)) . x
proof
let x be Element of C; ::_thesis: ( x in dom (max- f) implies (max- f) . x = (max+ (- f)) . x )
assume A3: x in dom (max- f) ; ::_thesis: (max- f) . x = (max+ (- f)) . x
then ( (max- f) . x = max ((- (f . x)),0.) & - (f . x) = (- f) . x ) by A1, Def3, MESFUNC1:def_7;
hence (max- f) . x = (max+ (- f)) . x by A2, A3, Def2; ::_thesis: verum
end;
hence max- f = max+ (- f) by A2, PARTFUN1:5; ::_thesis: verum
end;
theorem Th15: :: MESFUNC2:15
for C being non empty set
for f being PartFunc of C,ExtREAL
for x being Element of C st 0. < (max+ f) . x holds
(max- f) . x = 0.
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL
for x being Element of C st 0. < (max+ f) . x holds
(max- f) . x = 0.
let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C st 0. < (max+ f) . x holds
(max- f) . x = 0.
let x be Element of C; ::_thesis: ( 0. < (max+ f) . x implies (max- f) . x = 0. )
A1: dom (max+ f) = dom f by Def2;
percases ( x in dom f or not x in dom f ) ;
supposeA2: x in dom f ; ::_thesis: ( 0. < (max+ f) . x implies (max- f) . x = 0. )
assume A3: 0. < (max+ f) . x ; ::_thesis: (max- f) . x = 0.
A4: x in dom (max+ f) by A2, Def2;
A5: x in dom (max- f) by A2, Def3;
(max+ f) . x = max ((f . x),0.) by A4, Def2;
then ( not f . x <= 0. or not 0. <= 0. ) by A3, XXREAL_0:28;
then max ((- (f . x)),0.) = 0. by XXREAL_0:def_10;
hence (max- f) . x = 0. by A5, Def3; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: ( 0. < (max+ f) . x implies (max- f) . x = 0. )
hence ( 0. < (max+ f) . x implies (max- f) . x = 0. ) by A1, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
theorem :: MESFUNC2:16
for C being non empty set
for f being PartFunc of C,ExtREAL
for x being Element of C st 0. < (max- f) . x holds
(max+ f) . x = 0.
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL
for x being Element of C st 0. < (max- f) . x holds
(max+ f) . x = 0.
let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C st 0. < (max- f) . x holds
(max+ f) . x = 0.
let x be Element of C; ::_thesis: ( 0. < (max- f) . x implies (max+ f) . x = 0. )
A1: dom (max- f) = dom f by Def3;
percases ( x in dom f or not x in dom f ) ;
supposeA2: x in dom f ; ::_thesis: ( 0. < (max- f) . x implies (max+ f) . x = 0. )
assume A3: 0. < (max- f) . x ; ::_thesis: (max+ f) . x = 0.
A4: x in dom (max- f) by A2, Def3;
A5: x in dom (max+ f) by A2, Def2;
(max- f) . x = max ((- (f . x)),0.) by A4, Def3;
then - (- (f . x)) < - 0. by A3, XXREAL_0:28;
then max ((f . x),0.) = 0. by XXREAL_0:def_10;
hence (max+ f) . x = 0. by A5, Def2; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: ( 0. < (max- f) . x implies (max+ f) . x = 0. )
hence ( 0. < (max- f) . x implies (max+ f) . x = 0. ) by A1, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
theorem Th17: :: MESFUNC2:17
for C being non empty set
for f being PartFunc of C,ExtREAL holds
( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) )
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL holds
( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) )
let f be PartFunc of C,ExtREAL; ::_thesis: ( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) )
A1: ( dom (max+ f) = dom f & dom (max- f) = dom f ) by Def2, Def3;
(max+ f) " {+infty} misses (max- f) " {+infty}
proof
assume not (max+ f) " {+infty} misses (max- f) " {+infty} ; ::_thesis: contradiction
then consider x1 being set such that
A2: x1 in (max+ f) " {+infty} and
A3: x1 in (max- f) " {+infty} by XBOOLE_0:3;
reconsider x1 = x1 as Element of C by A2;
A4: (max+ f) . x1 in {+infty} by A2, FUNCT_1:def_7;
A5: (max- f) . x1 in {+infty} by A3, FUNCT_1:def_7;
A6: (max+ f) . x1 = +infty by A4, TARSKI:def_1;
(max- f) . x1 = +infty by A5, TARSKI:def_1;
hence contradiction by A6, Th15; ::_thesis: verum
end;
then A7: ((max+ f) " {+infty}) /\ ((max- f) " {+infty}) = {} by XBOOLE_0:def_7;
(max+ f) " {-infty} misses (max- f) " {-infty}
proof
assume not (max+ f) " {-infty} misses (max- f) " {-infty} ; ::_thesis: contradiction
then consider x1 being set such that
A8: x1 in (max+ f) " {-infty} and
x1 in (max- f) " {-infty} by XBOOLE_0:3;
reconsider x1 = x1 as Element of C by A8;
(max+ f) . x1 in {-infty} by A8, FUNCT_1:def_7;
then (max+ f) . x1 = -infty by TARSKI:def_1;
hence contradiction by Th12; ::_thesis: verum
end;
then A9: ((max+ f) " {-infty}) /\ ((max- f) " {-infty}) = {} by XBOOLE_0:def_7;
(max+ f) " {+infty} misses (max- f) " {-infty}
proof
assume not (max+ f) " {+infty} misses (max- f) " {-infty} ; ::_thesis: contradiction
then consider x1 being set such that
A10: x1 in (max+ f) " {+infty} and
A11: x1 in (max- f) " {-infty} by XBOOLE_0:3;
reconsider x1 = x1 as Element of C by A10;
(max- f) . x1 in {-infty} by A11, FUNCT_1:def_7;
then (max- f) . x1 = -infty by TARSKI:def_1;
hence contradiction by Th13; ::_thesis: verum
end;
then A12: ((max+ f) " {+infty}) /\ ((max- f) " {-infty}) = {} by XBOOLE_0:def_7;
(max+ f) " {-infty} misses (max- f) " {+infty}
proof
assume not (max+ f) " {-infty} misses (max- f) " {+infty} ; ::_thesis: contradiction
then consider x1 being set such that
A13: x1 in (max+ f) " {-infty} and
x1 in (max- f) " {+infty} by XBOOLE_0:3;
reconsider x1 = x1 as Element of C by A13;
(max+ f) . x1 in {-infty} by A13, FUNCT_1:def_7;
then (max+ f) . x1 = -infty by TARSKI:def_1;
hence contradiction by Th12; ::_thesis: verum
end;
then A14: ((max+ f) " {-infty}) /\ ((max- f) " {+infty}) = {} by XBOOLE_0:def_7;
dom ((max+ f) - (max- f)) = ((dom f) /\ (dom f)) \ ({} \/ {}) by A1, A7, A9, MESFUNC1:def_4;
hence ( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) ) by A1, A12, A14, MESFUNC1:def_3; ::_thesis: verum
end;
theorem Th18: :: MESFUNC2:18
for C being non empty set
for f being PartFunc of C,ExtREAL
for x being Element of C holds
( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) )
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL
for x being Element of C 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 C,ExtREAL; ::_thesis: for x being Element of C holds
( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) )
let x be Element of C; ::_thesis: ( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) )
A1: ( dom (max- f) = dom f & dom (max+ f) = dom f ) by Def2, Def3;
percases ( x in dom f or not x in dom f ) ;
supposeA2: 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 A3: x in dom (max+ f) by Def2;
A4: x in dom (max- f) by A2, Def3;
A5: (max+ f) . x = max ((f . x),0.) by A3, Def2;
(max- f) . x = max ((- (f . x)),0.) by A4, Def3;
hence ( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) ) by A5, XXREAL_0:16; ::_thesis: verum
end;
suppose not 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. ) )
hence ( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) ) by A1, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
theorem Th19: :: MESFUNC2:19
for C being non empty set
for f being PartFunc of C,ExtREAL
for x being Element of C st (max+ f) . x = f . x holds
(max- f) . x = 0.
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL
for x being Element of C st (max+ f) . x = f . x holds
(max- f) . x = 0.
let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C st (max+ f) . x = f . x holds
(max- f) . x = 0.
let x be Element of C; ::_thesis: ( (max+ f) . x = f . x implies (max- f) . x = 0. )
A1: dom (max- f) = dom f by Def3;
percases ( x in dom f or not x in dom f ) ;
supposeA2: x in dom f ; ::_thesis: ( (max+ f) . x = f . x implies (max- f) . x = 0. )
assume A3: (max+ f) . x = f . x ; ::_thesis: (max- f) . x = 0.
A4: x in dom (max+ f) by A2, Def2;
A5: x in dom (max- f) by A2, Def3;
A6: (max+ f) . x = max ((f . x),0.) by A4, Def2;
A7: (max- f) . x = max ((- (f . x)),0.) by A5, Def3;
0. <= f . x by A3, A6, XXREAL_0:def_10;
hence (max- f) . x = 0. by A7, XXREAL_0:def_10; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: ( (max+ f) . x = f . x implies (max- f) . x = 0. )
hence ( (max+ f) . x = f . x implies (max- f) . x = 0. ) by A1, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
theorem Th20: :: MESFUNC2:20
for C being non empty set
for f being PartFunc of C,ExtREAL
for x being Element of C st x in dom f & (max+ f) . x = 0. holds
(max- f) . x = - (f . x)
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL
for x being Element of C st x in dom f & (max+ f) . x = 0. holds
(max- f) . x = - (f . x)
let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C st x in dom f & (max+ f) . x = 0. holds
(max- f) . x = - (f . x)
let x be Element of C; ::_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)
A3: x in dom (max+ f) by A1, Def2;
A4: x in dom (max- f) by A1, Def3;
A5: (max+ f) . x = max ((f . x),0.) by A3, Def2;
A6: (max- f) . x = max ((- (f . x)),0.) by A4, Def3;
f . x <= 0. by A2, A5, XXREAL_0:def_10;
hence (max- f) . x = - (f . x) by A6, XXREAL_0:def_10; ::_thesis: verum
end;
theorem :: MESFUNC2:21
for C being non empty set
for f being PartFunc of C,ExtREAL
for x being Element of C st (max- f) . x = - (f . x) holds
(max+ f) . x = 0.
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL
for x being Element of C st (max- f) . x = - (f . x) holds
(max+ f) . x = 0.
let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C st (max- f) . x = - (f . x) holds
(max+ f) . x = 0.
let x be Element of C; ::_thesis: ( (max- f) . x = - (f . x) implies (max+ f) . x = 0. )
A1: dom (max+ f) = dom f by Def2;
percases ( x in dom f or not x in dom f ) ;
supposeA2: x in dom f ; ::_thesis: ( (max- f) . x = - (f . x) implies (max+ f) . x = 0. )
assume A3: (max- f) . x = - (f . x) ; ::_thesis: (max+ f) . x = 0.
A4: x in dom (max+ f) by A2, Def2;
A5: x in dom (max- f) by A2, Def3;
A6: (max+ f) . x = max ((f . x),0.) by A4, Def2;
(max- f) . x = max ((- (f . x)),0.) by A5, Def3;
then - (- (f . x)) <= - 0. by A3, XXREAL_0:def_10;
hence (max+ f) . x = 0. by A6, XXREAL_0:def_10; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: ( (max- f) . x = - (f . x) implies (max+ f) . x = 0. )
hence ( (max- f) . x = - (f . x) implies (max+ f) . x = 0. ) by A1, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
theorem :: MESFUNC2:22
for C being non empty set
for f being PartFunc of C,ExtREAL
for x being Element of C st x in dom f & (max- f) . x = 0. holds
(max+ f) . x = f . x
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL
for x being Element of C st x in dom f & (max- f) . x = 0. holds
(max+ f) . x = f . x
let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C st x in dom f & (max- f) . x = 0. holds
(max+ f) . x = f . x
let x be Element of C; ::_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
A3: x in dom (max+ f) by A1, Def2;
A4: x in dom (max- f) by A1, Def3;
A5: (max+ f) . x = max ((f . x),0.) by A3, Def2;
(max- f) . x = max ((- (f . x)),0.) by A4, Def3;
then - 0. <= - (- (f . x)) by A2, XXREAL_0:def_10;
hence (max+ f) . x = f . x by A5, XXREAL_0:def_10; ::_thesis: verum
end;
theorem :: MESFUNC2:23
for C being non empty set
for f being PartFunc of C,ExtREAL holds f = (max+ f) - (max- f)
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL holds f = (max+ f) - (max- f)
let f be PartFunc of C,ExtREAL; ::_thesis: f = (max+ f) - (max- f)
A1: dom f = dom ((max+ f) - (max- f)) by Th17;
for x being Element of C st x in dom f holds
f . x = ((max+ f) - (max- f)) . x
proof
let x be Element of C; ::_thesis: ( x in dom f implies f . x = ((max+ f) - (max- f)) . x )
assume A2: x in dom f ; ::_thesis: f . x = ((max+ f) - (max- f)) . x
then A3: ((max+ f) - (max- f)) . x = ((max+ f) . x) - ((max- f) . x) by A1, MESFUNC1:def_4;
percases ( (max+ f) . x = f . x or (max+ f) . x = 0. ) by Th18;
supposeA4: (max+ f) . x = f . x ; ::_thesis: f . x = ((max+ f) - (max- f)) . x
then (max- f) . x = 0. by Th19;
then - ((max- f) . x) = 0 ;
hence f . x = ((max+ f) - (max- f)) . x by A3, A4, XXREAL_3:4; ::_thesis: verum
end;
supposeA5: (max+ f) . x = 0. ; ::_thesis: f . x = ((max+ f) - (max- f)) . x
then (max- f) . x = - (f . x) by A2, Th20;
hence f . x = ((max+ f) - (max- f)) . x by A3, A5, XXREAL_3:4; ::_thesis: verum
end;
end;
end;
hence f = (max+ f) - (max- f) by A1, PARTFUN1:5; ::_thesis: verum
end;
theorem :: MESFUNC2:24
for C being non empty set
for f being PartFunc of C,ExtREAL holds |.f.| = (max+ f) + (max- f)
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL holds |.f.| = (max+ f) + (max- f)
let f be PartFunc of C,ExtREAL; ::_thesis: |.f.| = (max+ f) + (max- f)
A1: dom f = dom ((max+ f) + (max- f)) by Th17;
A2: dom f = dom |.f.| by MESFUNC1:def_10;
for x being Element of C st x in dom f holds
|.f.| . x = ((max+ f) + (max- f)) . x
proof
let x be Element of C; ::_thesis: ( x in dom f implies |.f.| . x = ((max+ f) + (max- f)) . x )
assume A3: x in dom f ; ::_thesis: |.f.| . x = ((max+ f) + (max- f)) . x
now__::_thesis:_|.f.|_._x_=_((max+_f)_+_(max-_f))_._x
percases ( (max+ f) . x = f . x or (max+ f) . x = 0. ) by Th18;
supposeA4: (max+ f) . x = f . x ; ::_thesis: |.f.| . x = ((max+ f) + (max- f)) . x
then A5: ((max+ f) . x) + ((max- f) . x) = (f . x) + 0. by Th19
.= f . x by XXREAL_3:4 ;
x in dom (max+ f) by A3, Def2;
then (max+ f) . x = max ((f . x),0.) by Def2;
then 0. <= f . x by A4, XXREAL_0:def_10;
then f . x = |.(f . x).| by EXTREAL1:def_1
.= |.f.| . x by A2, A3, MESFUNC1:def_10 ;
hence |.f.| . x = ((max+ f) + (max- f)) . x by A1, A3, A5, MESFUNC1:def_3; ::_thesis: verum
end;
supposeA6: (max+ f) . x = 0. ; ::_thesis: |.f.| . x = ((max+ f) + (max- f)) . x
then A7: ((max+ f) . x) + ((max- f) . x) = 0. + (- (f . x)) by A3, Th20
.= - (f . x) by XXREAL_3:4 ;
x in dom (max+ f) by A3, Def2;
then (max+ f) . x = max ((f . x),0.) by Def2;
then f . x <= 0. by A6, XXREAL_0:def_10;
then - (f . x) = |.(f . x).| by EXTREAL2:7
.= |.f.| . x by A2, A3, MESFUNC1:def_10 ;
hence |.f.| . x = ((max+ f) + (max- f)) . x by A1, A3, A7, MESFUNC1:def_3; ::_thesis: verum
end;
end;
end;
hence |.f.| . x = ((max+ f) + (max- f)) . x ; ::_thesis: verum
end;
hence |.f.| = (max+ f) + (max- f) by A1, A2, PARTFUN1:5; ::_thesis: verum
end;
begin
theorem :: MESFUNC2:25
for X being non empty set
for f being PartFunc of X,ExtREAL
for S being SigmaField of X
for A being Element of S st f is_measurable_on A holds
max+ f is_measurable_on A
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,ExtREAL
for S being SigmaField of X
for A being Element of S st f is_measurable_on A holds
max+ f is_measurable_on A
let f be PartFunc of X,ExtREAL; ::_thesis: for S being SigmaField of X
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 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 A1: f is_measurable_on A ; ::_thesis: max+ f is_measurable_on A
for r being real number holds A /\ (less_dom ((max+ f),(R_EAL r))) in S
proof
let r be real number ; ::_thesis: A /\ (less_dom ((max+ f),(R_EAL r))) in S
reconsider r = r as Real by XREAL_0:def_1;
now__::_thesis:_A_/\_(less_dom_((max+_f),(R_EAL_r)))_in_S
percases ( 0 < r or r <= 0 ) ;
supposeA2: 0 < r ; ::_thesis: A /\ (less_dom ((max+ f),(R_EAL r))) in S
for x being set st x in less_dom ((max+ f),(R_EAL r)) holds
x in less_dom (f,(R_EAL r))
proof
let x be set ; ::_thesis: ( x in less_dom ((max+ f),(R_EAL r)) implies x in less_dom (f,(R_EAL r)) )
assume A3: x in less_dom ((max+ f),(R_EAL r)) ; ::_thesis: x in less_dom (f,(R_EAL r))
then A4: x in dom (max+ f) by MESFUNC1:def_11;
A5: (max+ f) . x < R_EAL r by A3, MESFUNC1:def_11;
reconsider x = x as Element of X by A3;
A6: max ((f . x),0.) < R_EAL r by A4, A5, Def2;
then A7: f . x <= R_EAL r by XXREAL_0:30;
f . x <> R_EAL r
proof
assume A8: f . x = R_EAL r ; ::_thesis: contradiction
then max ((f . x),0.) = 0. by A6, XXREAL_0:16;
hence contradiction by A6, A8, XXREAL_0:def_10; ::_thesis: verum
end;
then A9: f . x < R_EAL r by A7, XXREAL_0:1;
x in dom f by A4, Def2;
hence x in less_dom (f,(R_EAL r)) by A9, MESFUNC1:def_11; ::_thesis: verum
end;
then A10: less_dom ((max+ f),(R_EAL r)) c= less_dom (f,(R_EAL r)) by TARSKI:def_3;
for x being set st x in less_dom (f,(R_EAL r)) holds
x in less_dom ((max+ f),(R_EAL r))
proof
let x be set ; ::_thesis: ( x in less_dom (f,(R_EAL r)) implies x in less_dom ((max+ f),(R_EAL r)) )
assume A11: x in less_dom (f,(R_EAL r)) ; ::_thesis: x in less_dom ((max+ f),(R_EAL r))
then A12: x in dom f by MESFUNC1:def_11;
A13: f . x < R_EAL r by A11, MESFUNC1:def_11;
reconsider x = x as Element of X by A11;
A14: x in dom (max+ f) by A12, Def2;
now__::_thesis:_x_in_less_dom_((max+_f),(R_EAL_r))
percases ( 0. <= f . x or not 0. <= f . x ) ;
suppose 0. <= f . x ; ::_thesis: x in less_dom ((max+ f),(R_EAL r))
then max ((f . x),0.) = f . x by XXREAL_0:def_10;
then (max+ f) . x = f . x by A14, Def2;
hence x in less_dom ((max+ f),(R_EAL r)) by A13, A14, MESFUNC1:def_11; ::_thesis: verum
end;
suppose not 0. <= f . x ; ::_thesis: x in less_dom ((max+ f),(R_EAL r))
then max ((f . x),0.) = 0. by XXREAL_0:def_10;
then (max+ f) . x = 0. by A14, Def2;
hence x in less_dom ((max+ f),(R_EAL r)) by A2, A14, MESFUNC1:def_11; ::_thesis: verum
end;
end;
end;
hence x in less_dom ((max+ f),(R_EAL r)) ; ::_thesis: verum
end;
then less_dom (f,(R_EAL r)) c= less_dom ((max+ f),(R_EAL r)) by TARSKI:def_3;
then less_dom ((max+ f),(R_EAL r)) = less_dom (f,(R_EAL r)) by A10, XBOOLE_0:def_10;
hence A /\ (less_dom ((max+ f),(R_EAL r))) in S by A1, MESFUNC1:def_16; ::_thesis: verum
end;
supposeA15: r <= 0 ; ::_thesis: A /\ (less_dom ((max+ f),(R_EAL r))) in S
for x being Element of X holds not x in less_dom ((max+ f),(R_EAL r))
proof
let x be Element of X; ::_thesis: not x in less_dom ((max+ f),(R_EAL r))
assume A16: x in less_dom ((max+ f),(R_EAL r)) ; ::_thesis: contradiction
then A17: x in dom (max+ f) by MESFUNC1:def_11;
A18: (max+ f) . x < R_EAL r by A16, MESFUNC1:def_11;
(max+ f) . x = max ((f . x),0.) by A17, Def2;
hence contradiction by A15, A18, XXREAL_0:25; ::_thesis: verum
end;
then less_dom ((max+ f),(R_EAL r)) = {} by SUBSET_1:4;
hence A /\ (less_dom ((max+ f),(R_EAL r))) in S by PROB_1:4; ::_thesis: verum
end;
end;
end;
hence A /\ (less_dom ((max+ f),(R_EAL r))) in S ; ::_thesis: verum
end;
hence max+ f is_measurable_on A by MESFUNC1:def_16; ::_thesis: verum
end;
theorem :: MESFUNC2:26
for X being non empty set
for f being PartFunc of X,ExtREAL
for S being SigmaField of X
for A being Element of S st f is_measurable_on A & A c= dom f holds
max- f is_measurable_on A
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,ExtREAL
for S being SigmaField of X
for A being Element of S st f is_measurable_on A & A c= dom f holds
max- f is_measurable_on A
let f be PartFunc of X,ExtREAL; ::_thesis: for S being SigmaField of X
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 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 A1: ( f is_measurable_on A & A c= dom f ) ; ::_thesis: max- f is_measurable_on A
for r being real number holds A /\ (less_dom ((max- f),(R_EAL r))) in S
proof
let r be real number ; ::_thesis: A /\ (less_dom ((max- f),(R_EAL r))) in S
reconsider r = r as Real by XREAL_0:def_1;
now__::_thesis:_A_/\_(less_dom_((max-_f),(R_EAL_r)))_in_S
percases ( 0 < r or r <= 0 ) ;
supposeA2: 0 < r ; ::_thesis: A /\ (less_dom ((max- f),(R_EAL r))) in S
(- 1) (#) f is_measurable_on A by A1, MESFUNC1:37;
then A3: - f is_measurable_on A by Th9;
for x being set st x in less_dom ((max- f),(R_EAL r)) holds
x in less_dom ((- f),(R_EAL r))
proof
let x be set ; ::_thesis: ( x in less_dom ((max- f),(R_EAL r)) implies x in less_dom ((- f),(R_EAL r)) )
assume A4: x in less_dom ((max- f),(R_EAL r)) ; ::_thesis: x in less_dom ((- f),(R_EAL r))
then A5: x in dom (max- f) by MESFUNC1:def_11;
A6: (max- f) . x < R_EAL r by A4, MESFUNC1:def_11;
reconsider x = x as Element of X by A4;
A7: max ((- (f . x)),0.) < R_EAL r by A5, A6, Def3;
then A8: - (f . x) <= R_EAL r by XXREAL_0:30;
- (f . x) <> R_EAL r
proof
assume A9: - (f . x) = R_EAL r ; ::_thesis: contradiction
then max ((- (f . x)),0.) = 0. by A7, XXREAL_0:16;
hence contradiction by A7, A9, XXREAL_0:def_10; ::_thesis: verum
end;
then A10: - (f . x) < R_EAL r by A8, XXREAL_0:1;
x in dom f by A5, Def3;
then A11: x in dom (- f) by MESFUNC1:def_7;
then (- f) . x = - (f . x) by MESFUNC1:def_7;
hence x in less_dom ((- f),(R_EAL r)) by A10, A11, MESFUNC1:def_11; ::_thesis: verum
end;
then A12: less_dom ((max- f),(R_EAL r)) c= less_dom ((- f),(R_EAL r)) by TARSKI:def_3;
for x being set st x in less_dom ((- f),(R_EAL r)) holds
x in less_dom ((max- f),(R_EAL r))
proof
let x be set ; ::_thesis: ( x in less_dom ((- f),(R_EAL r)) implies x in less_dom ((max- f),(R_EAL r)) )
assume A13: x in less_dom ((- f),(R_EAL r)) ; ::_thesis: x in less_dom ((max- f),(R_EAL r))
then A14: x in dom (- f) by MESFUNC1:def_11;
A15: (- f) . x < R_EAL r by A13, MESFUNC1:def_11;
reconsider x = x as Element of X by A13;
x in dom f by A14, MESFUNC1:def_7;
then A16: x in dom (max- f) by Def3;
now__::_thesis:_x_in_less_dom_((max-_f),(R_EAL_r))
percases ( 0. <= - (f . x) or not 0. <= - (f . x) ) ;
suppose 0. <= - (f . x) ; ::_thesis: x in less_dom ((max- f),(R_EAL r))
then max ((- (f . x)),0.) = - (f . x) by XXREAL_0:def_10;
then (max- f) . x = - (f . x) by A16, Def3
.= (- f) . x by A14, MESFUNC1:def_7 ;
hence x in less_dom ((max- f),(R_EAL r)) by A15, A16, MESFUNC1:def_11; ::_thesis: verum
end;
suppose not 0. <= - (f . x) ; ::_thesis: x in less_dom ((max- f),(R_EAL r))
then max ((- (f . x)),0.) = 0. by XXREAL_0:def_10;
then (max- f) . x = 0. by A16, Def3;
hence x in less_dom ((max- f),(R_EAL r)) by A2, A16, MESFUNC1:def_11; ::_thesis: verum
end;
end;
end;
hence x in less_dom ((max- f),(R_EAL r)) ; ::_thesis: verum
end;
then less_dom ((- f),(R_EAL r)) c= less_dom ((max- f),(R_EAL r)) by TARSKI:def_3;
then less_dom ((max- f),(R_EAL r)) = less_dom ((- f),(R_EAL r)) by A12, XBOOLE_0:def_10;
hence A /\ (less_dom ((max- f),(R_EAL r))) in S by A3, MESFUNC1:def_16; ::_thesis: verum
end;
supposeA17: r <= 0 ; ::_thesis: A /\ (less_dom ((max- f),(R_EAL r))) in S
for x being Element of X holds not x in less_dom ((max- f),(R_EAL r))
proof
let x be Element of X; ::_thesis: not x in less_dom ((max- f),(R_EAL r))
assume A18: x in less_dom ((max- f),(R_EAL r)) ; ::_thesis: contradiction
then A19: x in dom (max- f) by MESFUNC1:def_11;
A20: (max- f) . x < R_EAL r by A18, MESFUNC1:def_11;
(max- f) . x = max ((- (f . x)),0.) by A19, Def3;
hence contradiction by A17, A20, XXREAL_0:25; ::_thesis: verum
end;
then less_dom ((max- f),(R_EAL r)) = {} by SUBSET_1:4;
hence A /\ (less_dom ((max- f),(R_EAL r))) in S by PROB_1:4; ::_thesis: verum
end;
end;
end;
hence A /\ (less_dom ((max- f),(R_EAL r))) in S ; ::_thesis: verum
end;
hence max- f is_measurable_on A by MESFUNC1:def_16; ::_thesis: verum
end;
theorem :: MESFUNC2:27
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S st f is_measurable_on A & A c= dom f 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,ExtREAL
for A being Element of S st f is_measurable_on A & A c= dom f holds
|.f.| is_measurable_on A
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL
for A being Element of S st f is_measurable_on A & A c= dom f holds
|.f.| is_measurable_on A
let f be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds
|.f.| is_measurable_on A
let A be Element of S; ::_thesis: ( f is_measurable_on A & A c= dom f implies |.f.| is_measurable_on A )
assume A1: ( f is_measurable_on A & A c= dom f ) ; ::_thesis: |.f.| is_measurable_on A
for r being real number holds A /\ (less_dom (|.f.|,(R_EAL r))) in S
proof
let r be real number ; ::_thesis: A /\ (less_dom (|.f.|,(R_EAL r))) in S
reconsider r = r as Real by XREAL_0:def_1;
for x being set st x in less_dom (|.f.|,(R_EAL r)) holds
x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r))))
proof
let x be set ; ::_thesis: ( x in less_dom (|.f.|,(R_EAL r)) implies x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) )
assume A2: x in less_dom (|.f.|,(R_EAL r)) ; ::_thesis: x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r))))
then A3: x in dom |.f.| by MESFUNC1:def_11;
A4: |.f.| . x < R_EAL r by A2, MESFUNC1:def_11;
reconsider x = x as Element of X by A2;
A5: x in dom f by A3, MESFUNC1:def_10;
A6: |.(f . x).| < R_EAL r by A3, A4, MESFUNC1:def_10;
then A7: - (R_EAL r) < f . x by EXTREAL2:10;
A8: f . x < R_EAL r by A6, EXTREAL2:10;
A9: - (R_EAL r) = - r by SUPINF_2:2;
A10: x in less_dom (f,(R_EAL r)) by A5, A8, MESFUNC1:def_11;
x in great_dom (f,(R_EAL (- r))) by A5, A7, A9, MESFUNC1:def_13;
hence x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) by A10, XBOOLE_0:def_4; ::_thesis: verum
end;
then A11: less_dom (|.f.|,(R_EAL r)) c= (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) by TARSKI:def_3;
for x being set st x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) holds
x in less_dom (|.f.|,(R_EAL r))
proof
let x be set ; ::_thesis: ( x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) implies x in less_dom (|.f.|,(R_EAL r)) )
assume A12: x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) ; ::_thesis: x in less_dom (|.f.|,(R_EAL r))
then A13: x in less_dom (f,(R_EAL r)) by XBOOLE_0:def_4;
A14: x in great_dom (f,(R_EAL (- r))) by A12, XBOOLE_0:def_4;
A15: x in dom f by A13, MESFUNC1:def_11;
A16: f . x < R_EAL r by A13, MESFUNC1:def_11;
A17: R_EAL (- r) < f . x by A14, MESFUNC1:def_13;
reconsider x = x as Element of X by A12;
A18: x in dom |.f.| by A15, MESFUNC1:def_10;
- (R_EAL r) = - r by SUPINF_2:2;
then |.(f . x).| < R_EAL r by A16, A17, EXTREAL2:11;
then |.f.| . x < R_EAL r by A18, MESFUNC1:def_10;
hence x in less_dom (|.f.|,(R_EAL r)) by A18, MESFUNC1:def_11; ::_thesis: verum
end;
then (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) c= less_dom (|.f.|,(R_EAL r)) by TARSKI:def_3;
then A19: less_dom (|.f.|,(R_EAL r)) = (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) by A11, XBOOLE_0:def_10;
(A /\ (great_dom (f,(R_EAL (- r))))) /\ (less_dom (f,(R_EAL r))) in S by A1, MESFUNC1:32;
hence A /\ (less_dom (|.f.|,(R_EAL r))) in S by A19, XBOOLE_1:16; ::_thesis: verum
end;
hence |.f.| is_measurable_on A by MESFUNC1:def_16; ::_thesis: verum
end;
begin
definition
let A, X be set ;
:: original: chi
redefine func chi (A,X) -> PartFunc of X,ExtREAL;
coherence
chi (A,X) is PartFunc of X,ExtREAL
proof
now__::_thesis:_for_x_being_set_st_x_in_rng_(chi_(A,X))_holds_
x_in_ExtREAL
let x be set ; ::_thesis: ( x in rng (chi (A,X)) implies x in ExtREAL )
assume A1: x in rng (chi (A,X)) ; ::_thesis: x in ExtREAL
now__::_thesis:_x_in_ExtREAL
percases ( x = 0. or x = 1. ) by A1, MESFUNC1:def_8, TARSKI:def_2;
suppose x = 0. ; ::_thesis: x in ExtREAL
hence x in ExtREAL ; ::_thesis: verum
end;
suppose x = 1. ; ::_thesis: x in ExtREAL
hence x in ExtREAL ; ::_thesis: verum
end;
end;
end;
hence x in ExtREAL ; ::_thesis: verum
end;
then ( dom (chi (A,X)) = X & rng (chi (A,X)) c= ExtREAL ) by FUNCT_3:def_3, TARSKI:def_3;
hence chi (A,X) is PartFunc of X,ExtREAL by RELSET_1:4; ::_thesis: verum
end;
end;
theorem :: MESFUNC2:28
for X being non empty set
for S being SigmaField of X
for A being Element of S holds chi (A,X) is V75()
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for A being Element of S holds chi (A,X) is V75()
let S be SigmaField of X; ::_thesis: for A being Element of S holds chi (A,X) is V75()
let A be Element of S; ::_thesis: chi (A,X) is V75()
for x being Element of X st x in dom (chi (A,X)) holds
|.((chi (A,X)) . x).| < +infty
proof
let x be Element of X; ::_thesis: ( x in dom (chi (A,X)) implies |.((chi (A,X)) . x).| < +infty )
assume x in dom (chi (A,X)) ; ::_thesis: |.((chi (A,X)) . x).| < +infty
now__::_thesis:_|.((chi_(A,X))_._x).|_<_+infty
percases ( x in A or not x in A ) ;
suppose x in A ; ::_thesis: |.((chi (A,X)) . x).| < +infty
then (chi (A,X)) . x = 1. by FUNCT_3:def_3, MESFUNC1:def_8;
then |.((chi (A,X)) . x).| = 1. by EXTREAL1:def_1, MESFUNC1:def_8;
hence |.((chi (A,X)) . x).| < +infty by MESFUNC1:def_8, XXREAL_0:9; ::_thesis: verum
end;
suppose not x in A ; ::_thesis: |.((chi (A,X)) . x).| < +infty
then (chi (A,X)) . x = 0. by FUNCT_3:def_3;
hence |.((chi (A,X)) . x).| < +infty by EXTREAL1:def_1; ::_thesis: verum
end;
end;
end;
hence |.((chi (A,X)) . x).| < +infty ; ::_thesis: verum
end;
hence chi (A,X) is V75() by Def1; ::_thesis: verum
end;
theorem :: MESFUNC2:29
for X being non empty set
for S being SigmaField of X
for A, B being Element of S holds chi (A,X) is_measurable_on B
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for A, B being Element of S holds chi (A,X) is_measurable_on B
let S be SigmaField of X; ::_thesis: for A, B being Element of S holds chi (A,X) is_measurable_on B
let A, B be Element of S; ::_thesis: chi (A,X) is_measurable_on B
for r being real number holds B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S
proof
let r be real number ; ::_thesis: B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S
reconsider r = r as Real by XREAL_0:def_1;
now__::_thesis:_B_/\_(less_eq_dom_((chi_(A,X)),(R_EAL_r)))_in_S
percases ( r >= 1 or ( 0 <= r & r < 1 ) or r < 0 ) ;
supposeA1: r >= 1 ; ::_thesis: B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S
for x being set st x in X holds
x in less_eq_dom ((chi (A,X)),(R_EAL r))
proof
let x be set ; ::_thesis: ( x in X implies x in less_eq_dom ((chi (A,X)),(R_EAL r)) )
assume A2: x in X ; ::_thesis: x in less_eq_dom ((chi (A,X)),(R_EAL r))
then A3: x in dom (chi (A,X)) by FUNCT_3:def_3;
reconsider x = x as Element of X by A2;
(chi (A,X)) . x <= 1.
proof
now__::_thesis:_(chi_(A,X))_._x_<=_1.
percases ( x in A or not x in A ) ;
suppose x in A ; ::_thesis: (chi (A,X)) . x <= 1.
hence (chi (A,X)) . x <= 1. by FUNCT_3:def_3, MESFUNC1:def_8; ::_thesis: verum
end;
suppose not x in A ; ::_thesis: (chi (A,X)) . x <= 1.
hence (chi (A,X)) . x <= 1. by FUNCT_3:def_3, MESFUNC1:def_8; ::_thesis: verum
end;
end;
end;
hence (chi (A,X)) . x <= 1. ; ::_thesis: verum
end;
then (chi (A,X)) . x <= R_EAL r by A1, MESFUNC1:def_8, XXREAL_0:2;
hence x in less_eq_dom ((chi (A,X)),(R_EAL r)) by A3, MESFUNC1:def_12; ::_thesis: verum
end;
then X c= less_eq_dom ((chi (A,X)),(R_EAL r)) by TARSKI:def_3;
then less_eq_dom ((chi (A,X)),(R_EAL r)) = X by XBOOLE_0:def_10;
then less_eq_dom ((chi (A,X)),(R_EAL r)) in S by PROB_1:5;
hence B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S by FINSUB_1:def_2; ::_thesis: verum
end;
supposeA4: ( 0 <= r & r < 1 ) ; ::_thesis: B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S
for x being set st x in less_eq_dom ((chi (A,X)),(R_EAL r)) holds
x in X \ A
proof
let x be set ; ::_thesis: ( x in less_eq_dom ((chi (A,X)),(R_EAL r)) implies x in X \ A )
assume A5: x in less_eq_dom ((chi (A,X)),(R_EAL r)) ; ::_thesis: x in X \ A
then reconsider x = x as Element of X ;
(chi (A,X)) . x <= R_EAL r by A5, MESFUNC1:def_12;
then not x in A by A4, FUNCT_3:def_3;
hence x in X \ A by XBOOLE_0:def_5; ::_thesis: verum
end;
then A6: less_eq_dom ((chi (A,X)),(R_EAL r)) c= X \ A by TARSKI:def_3;
for x being set st x in X \ A holds
x in less_eq_dom ((chi (A,X)),(R_EAL r))
proof
let x be set ; ::_thesis: ( x in X \ A implies x in less_eq_dom ((chi (A,X)),(R_EAL r)) )
assume A7: x in X \ A ; ::_thesis: x in less_eq_dom ((chi (A,X)),(R_EAL r))
then A8: x in X ;
A9: not x in A by A7, XBOOLE_0:def_5;
reconsider x = x as Element of X by A7;
A10: (chi (A,X)) . x = 0. by A9, FUNCT_3:def_3;
x in dom (chi (A,X)) by A8, FUNCT_3:def_3;
hence x in less_eq_dom ((chi (A,X)),(R_EAL r)) by A4, A10, MESFUNC1:def_12; ::_thesis: verum
end;
then X \ A c= less_eq_dom ((chi (A,X)),(R_EAL r)) by TARSKI:def_3;
then A11: less_eq_dom ((chi (A,X)),(R_EAL r)) = X \ A by A6, XBOOLE_0:def_10;
X in S by PROB_1:5;
then less_eq_dom ((chi (A,X)),(R_EAL r)) in S by A11, MEASURE1:6;
hence B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S by FINSUB_1:def_2; ::_thesis: verum
end;
supposeA12: r < 0 ; ::_thesis: B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S
for x being Element of X holds not x in less_eq_dom ((chi (A,X)),(R_EAL r))
proof
assume ex x being Element of X st x in less_eq_dom ((chi (A,X)),(R_EAL r)) ; ::_thesis: contradiction
then consider x being Element of X such that
A13: x in less_eq_dom ((chi (A,X)),(R_EAL r)) ;
0. <= (chi (A,X)) . x
proof
now__::_thesis:_0._<=_(chi_(A,X))_._x
percases ( x in A or not x in A ) ;
suppose x in A ; ::_thesis: 0. <= (chi (A,X)) . x
hence 0. <= (chi (A,X)) . x by FUNCT_3:def_3; ::_thesis: verum
end;
suppose not x in A ; ::_thesis: 0. <= (chi (A,X)) . x
hence 0. <= (chi (A,X)) . x by FUNCT_3:def_3; ::_thesis: verum
end;
end;
end;
hence 0. <= (chi (A,X)) . x ; ::_thesis: verum
end;
hence contradiction by A12, A13, MESFUNC1:def_12; ::_thesis: verum
end;
then less_eq_dom ((chi (A,X)),(R_EAL r)) = {} by SUBSET_1:4;
hence B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S by PROB_1:4; ::_thesis: verum
end;
end;
end;
hence B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S ; ::_thesis: verum
end;
hence chi (A,X) is_measurable_on B by MESFUNC1:28; ::_thesis: verum
end;
begin
registration
let X be set ;
let S be SigmaField of X;
cluster Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like disjoint_valued for FinSequence of S;
existence
ex b1 being FinSequence of S st b1 is disjoint_valued
proof
reconsider A = {} as Element of S by PROB_1:4;
reconsider p = (Seg 1) --> A as Function of (Seg 1),S ;
A1: dom p = Seg 1 by FUNCOP_1:13;
then reconsider p = p as FinSequence by FINSEQ_1:def_2;
rng p c= S by RELAT_1:def_19;
then reconsider p = p as FinSequence of S by FINSEQ_1:def_4;
A2: for n, m being set st n <> m holds
p . n misses p . m
proof
let n, m be set ; ::_thesis: ( n <> m implies p . n misses p . m )
assume n <> m ; ::_thesis: p . n misses p . m
p . n = {}
proof
percases ( n in dom p or not n in dom p ) ;
suppose n in dom p ; ::_thesis: p . n = {}
hence p . n = {} by A1, FUNCOP_1:7; ::_thesis: verum
end;
suppose not n in dom p ; ::_thesis: p . n = {}
hence p . n = {} by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
hence p . n misses p . m by XBOOLE_1:65; ::_thesis: verum
end;
take p ; ::_thesis: p is disjoint_valued
thus p is disjoint_valued by A2, PROB_2:def_2; ::_thesis: verum
end;
end;
definition
let X be set ;
let S be SigmaField of X;
mode Finite_Sep_Sequence of S is disjoint_valued FinSequence of S;
end;
theorem Th30: :: MESFUNC2:30
for X being non empty set
for S being SigmaField of X
for F being Function st F is Finite_Sep_Sequence of S holds
ex G being Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds
F . n = G . n ) & ( for m being Nat st not m in dom F holds
G . m = {} ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for F being Function st F is Finite_Sep_Sequence of S holds
ex G being Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds
F . n = G . n ) & ( for m being Nat st not m in dom F holds
G . m = {} ) )
let S be SigmaField of X; ::_thesis: for F being Function st F is Finite_Sep_Sequence of S holds
ex G being Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds
F . n = G . n ) & ( for m being Nat st not m in dom F holds
G . m = {} ) )
let F be Function; ::_thesis: ( F is Finite_Sep_Sequence of S implies ex G being Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds
F . n = G . n ) & ( for m being Nat st not m in dom F holds
G . m = {} ) ) )
defpred S1[ set , set ] means ( ( $1 in dom F implies F . $1 = $2 ) & ( not $1 in dom F implies $2 = {} ) );
assume A1: F is Finite_Sep_Sequence of S ; ::_thesis: ex G being Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds
F . n = G . n ) & ( for m being Nat st not m in dom F holds
G . m = {} ) )
A2: for x1 being set st x1 in NAT holds
ex y1 being set st
( y1 in S & S1[x1,y1] )
proof
let x1 be set ; ::_thesis: ( x1 in NAT implies ex y1 being set st
( y1 in S & S1[x1,y1] ) )
assume x1 in NAT ; ::_thesis: ex y1 being set st
( y1 in S & S1[x1,y1] )
then reconsider x1 = x1 as Element of NAT ;
percases ( x1 in dom F or not x1 in dom F ) ;
supposeA3: x1 in dom F ; ::_thesis: ex y1 being set st
( y1 in S & S1[x1,y1] )
then A4: F . x1 in rng F by FUNCT_1:def_3;
A5: rng F c= S by A1, FINSEQ_1:def_4;
take F . x1 ; ::_thesis: ( F . x1 in S & S1[x1,F . x1] )
thus ( F . x1 in S & S1[x1,F . x1] ) by A3, A4, A5; ::_thesis: verum
end;
supposeA6: not x1 in dom F ; ::_thesis: ex y1 being set st
( y1 in S & S1[x1,y1] )
take {} ; ::_thesis: ( {} in S & S1[x1, {} ] )
thus ( {} in S & S1[x1, {} ] ) by A6, PROB_1:4; ::_thesis: verum
end;
end;
end;
consider G being Function of NAT,S such that
A7: for x1 being set st x1 in NAT holds
S1[x1,G . x1] from FUNCT_2:sch_1(A2);
for n, m being set st n <> m holds
G . n misses G . m
proof
let n, m be set ; ::_thesis: ( n <> m implies G . n misses G . m )
assume A8: n <> m ; ::_thesis: G . n misses G . m
percases ( ( n in NAT & m in NAT ) or not n in NAT or not m in NAT ) ;
supposeA9: ( n in NAT & m in NAT ) ; ::_thesis: G . n misses G . m
now__::_thesis:_G_._n_misses_G_._m
percases ( ( n in dom F & m in dom F ) or not n in dom F or not m in dom F ) ;
suppose ( n in dom F & m in dom F ) ; ::_thesis: G . n misses G . m
then ( G . n = F . n & G . m = F . m ) by A7, A9;
hence G . n misses G . m by A1, A8, PROB_2:def_2; ::_thesis: verum
end;
supposeA10: ( not n in dom F or not m in dom F ) ; ::_thesis: G . n misses G . m
now__::_thesis:_G_._n_misses_G_._m
percases ( not n in dom F or not m in dom F ) by A10;
suppose not n in dom F ; ::_thesis: G . n misses G . m
then G . n = {} by A7, A9;
hence G . n misses G . m by XBOOLE_1:65; ::_thesis: verum
end;
suppose not m in dom F ; ::_thesis: G . n misses G . m
then G . m = {} by A7, A9;
hence G . n misses G . m by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence G . n misses G . m ; ::_thesis: verum
end;
end;
end;
hence G . n misses G . m ; ::_thesis: verum
end;
suppose ( not n in NAT or not m in NAT ) ; ::_thesis: G . n misses G . m
then ( not n in dom G or not m in dom G ) ;
then ( G . n = {} or G . m = {} ) by FUNCT_1:def_2;
hence G . n misses G . m by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
then reconsider G = G as Sep_Sequence of S by PROB_2:def_2;
take G ; ::_thesis: ( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds
F . n = G . n ) & ( for m being Nat st not m in dom F holds
G . m = {} ) )
for x1 being set st x1 in union (rng F) holds
x1 in union (rng G)
proof
let x1 be set ; ::_thesis: ( x1 in union (rng F) implies x1 in union (rng G) )
assume x1 in union (rng F) ; ::_thesis: x1 in union (rng G)
then consider Y being set such that
A11: x1 in Y and
A12: Y in rng F by TARSKI:def_4;
consider k being set such that
A13: k in dom F and
A14: Y = F . k by A12, FUNCT_1:def_3;
dom F c= NAT by A1, RELAT_1:def_18;
then reconsider k = k as Element of NAT by A13;
A15: F . k = G . k by A7, A13;
G . k in rng G by FUNCT_2:4;
hence x1 in union (rng G) by A11, A14, A15, TARSKI:def_4; ::_thesis: verum
end;
then A16: union (rng F) c= union (rng G) by TARSKI:def_3;
for x1 being set st x1 in union (rng G) holds
x1 in union (rng F)
proof
let x1 be set ; ::_thesis: ( x1 in union (rng G) implies x1 in union (rng F) )
assume x1 in union (rng G) ; ::_thesis: x1 in union (rng F)
then consider Y being set such that
A17: x1 in Y and
A18: Y in rng G by TARSKI:def_4;
consider k being set such that
A19: k in dom G and
A20: Y = G . k by A18, FUNCT_1:def_3;
reconsider k = k as Element of NAT by A19;
A21: k in dom F by A7, A17, A20;
A22: F . k = G . k by A7, A17, A20;
F . k in rng F by A21, FUNCT_1:def_3;
hence x1 in union (rng F) by A17, A20, A22, TARSKI:def_4; ::_thesis: verum
end;
then union (rng G) c= union (rng F) by TARSKI:def_3;
hence union (rng F) = union (rng G) by A16, XBOOLE_0:def_10; ::_thesis: ( ( for n being Nat st n in dom F holds
F . n = G . n ) & ( for m being Nat st not m in dom F holds
G . m = {} ) )
hereby ::_thesis: for m being Nat st not m in dom F holds
G . m = {}
let n be Nat; ::_thesis: ( n in dom F implies F . n = G . n )
n in NAT by ORDINAL1:def_12;
hence ( n in dom F implies F . n = G . n ) by A7; ::_thesis: verum
end;
let m be Nat; ::_thesis: ( not m in dom F implies G . m = {} )
m in NAT by ORDINAL1:def_12;
hence ( not m in dom F implies G . m = {} ) by A7; ::_thesis: verum
end;
theorem :: MESFUNC2:31
for X being non empty set
for S being SigmaField of X
for F being Function st F is Finite_Sep_Sequence of S holds
union (rng F) in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for F being Function st F is Finite_Sep_Sequence of S holds
union (rng F) in S
let S be SigmaField of X; ::_thesis: for F being Function st F is Finite_Sep_Sequence of S holds
union (rng F) in S
let F be Function; ::_thesis: ( F is Finite_Sep_Sequence of S implies union (rng F) in S )
assume F is Finite_Sep_Sequence of S ; ::_thesis: union (rng F) in S
then ex G being Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds
F . n = G . n ) & ( for m being Nat st not m in dom F holds
G . m = {} ) ) by Th30;
hence union (rng F) in S ; ::_thesis: verum
end;
definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,ExtREAL;
predf is_simple_func_in S means :Def4: :: MESFUNC2:def 4
( f is V75() & 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 Def4 defines is_simple_func_in MESFUNC2:def_4_:_
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL holds
( f is_simple_func_in S iff ( f is V75() & 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 :: MESFUNC2:32
for X being non empty set
for f being PartFunc of X,ExtREAL st f is V75() holds
rng f is Subset of REAL
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,ExtREAL st f is V75() holds
rng f is Subset of REAL
let f be PartFunc of X,ExtREAL; ::_thesis: ( f is V75() implies rng f is Subset of REAL )
assume A1: f is V75() ; ::_thesis: rng f is Subset of REAL
rng f c= REAL
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in REAL )
assume A2: y in rng f ; ::_thesis: y in REAL
then reconsider y = y as R_eal ;
consider x being set such that
A3: x in dom f and
A4: y = f . x by A2, FUNCT_1:def_3;
reconsider x = x as Element of X by A3;
A5: |.(f . x).| < +infty by A1, A3, Def1;
then - +infty < y by A4, EXTREAL2:10;
then A6: -infty < y by XXREAL_3:def_3;
y < +infty by A4, A5, EXTREAL2:10;
hence y in REAL by A6, XXREAL_0:14; ::_thesis: verum
end;
hence rng f is Subset of REAL ; ::_thesis: verum
end;
theorem :: MESFUNC2:33
for X being non empty set
for S being SigmaField of X
for n being Nat
for F being Relation st F is Finite_Sep_Sequence of S holds
F | (Seg n) is Finite_Sep_Sequence of S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for n being Nat
for F being Relation st F is Finite_Sep_Sequence of S holds
F | (Seg n) is Finite_Sep_Sequence of S
let S be SigmaField of X; ::_thesis: for n being Nat
for F being Relation st F is Finite_Sep_Sequence of S holds
F | (Seg n) is Finite_Sep_Sequence of S
let n be Nat; ::_thesis: for F being Relation st F is Finite_Sep_Sequence of S holds
F | (Seg n) is Finite_Sep_Sequence of S
let F be Relation; ::_thesis: ( F is Finite_Sep_Sequence of S implies F | (Seg n) is Finite_Sep_Sequence of S )
assume A1: F is Finite_Sep_Sequence of S ; ::_thesis: F | (Seg n) is Finite_Sep_Sequence of S
then reconsider G = F | (Seg n) as FinSequence of S by FINSEQ_1:18;
reconsider F = F as FinSequence of S by A1;
for k, m being set st k <> m holds
G . k misses G . m
proof
let k, m be set ; ::_thesis: ( k <> m implies G . k misses G . m )
assume A2: k <> m ; ::_thesis: G . k misses G . m
percases ( ( k in dom G & m in dom G ) or not k in dom G or not m in dom G ) ;
suppose ( k in dom G & m in dom G ) ; ::_thesis: G . k misses G . m
then ( G . k = F . k & G . m = F . m ) by FUNCT_1:47;
hence G . k misses G . m by A1, A2, PROB_2:def_2; ::_thesis: verum
end;
suppose ( not k in dom G or not m in dom G ) ; ::_thesis: G . k misses G . m
then ( G . k = {} or G . m = {} ) by FUNCT_1:def_2;
hence G . k misses G . m by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence F | (Seg n) is Finite_Sep_Sequence of S by PROB_2:def_2; ::_thesis: verum
end;
theorem :: MESFUNC2:34
for X being non empty set
for f being PartFunc of X,ExtREAL
for S being SigmaField of X
for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,ExtREAL
for S being SigmaField of X
for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
let f be PartFunc of X,ExtREAL; ::_thesis: for S being SigmaField of X
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 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 A1: f is_simple_func_in S ; ::_thesis: f is_measurable_on A
then consider F being Finite_Sep_Sequence of S such that
A2: dom f = union (rng F) and
A3: 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 Def4;
reconsider F = F as FinSequence of S ;
defpred S1[ Nat] means ( $1 <= len F implies f | (union (rng (F | (Seg $1)))) is_measurable_on A );
A4: S1[ 0 ]
proof
assume A5: 0 <= len F ; ::_thesis: f | (union (rng (F | (Seg 0)))) is_measurable_on A
reconsider z = 0 as Nat ;
reconsider G = F | (Seg z) as FinSequence of S by FINSEQ_1:18;
len G = 0 by A5, FINSEQ_1:17;
then G = {} ;
then A6: dom (f | (union (rng G))) = (dom f) /\ {} by RELAT_1:38, RELAT_1:61, ZFMISC_1:2
.= {} ;
for r being real number holds A /\ (less_dom ((f | (union (rng G))),(R_EAL r))) in S
proof
let r be real number ; ::_thesis: A /\ (less_dom ((f | (union (rng G))),(R_EAL r))) in S
for x1 being set st x1 in less_dom ((f | (union (rng G))),(R_EAL r)) holds
x1 in dom (f | (union (rng G))) by MESFUNC1:def_11;
then less_dom ((f | (union (rng G))),(R_EAL r)) c= dom (f | (union (rng G))) by TARSKI:def_3;
then less_dom ((f | (union (rng G))),(R_EAL r)) = {} by A6, XBOOLE_1:3;
hence A /\ (less_dom ((f | (union (rng G))),(R_EAL r))) in S by PROB_1:4; ::_thesis: verum
end;
hence f | (union (rng (F | (Seg 0)))) is_measurable_on A by MESFUNC1:def_16; ::_thesis: verum
end;
A7: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A8: ( m <= len F implies f | (union (rng (F | (Seg m)))) is_measurable_on A ) ; ::_thesis: S1[m + 1]
reconsider m = m as Element of NAT by ORDINAL1:def_12;
( m + 1 <= len F implies f | (union (rng (F | (Seg (m + 1))))) is_measurable_on A )
proof
assume A9: m + 1 <= len F ; ::_thesis: f | (union (rng (F | (Seg (m + 1))))) is_measurable_on A
A10: m <= m + 1 by NAT_1:11;
for r being real number holds A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) in S
proof
let r be real number ; ::_thesis: A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) in S
now__::_thesis:_A_/\_(less_dom_((f_|_(union_(rng_(F_|_(Seg_(m_+_1)))))),(R_EAL_r)))_in_S
percases ( F . (m + 1) = {} or F . (m + 1) <> {} ) ;
supposeA11: F . (m + 1) = {} ; ::_thesis: A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) in S
less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) = less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))
proof
reconsider G1 = F | (Seg m) as FinSequence of S by FINSEQ_1:18;
1 <= m + 1 by NAT_1:11;
then m + 1 in Seg (len F) by A9, FINSEQ_1:1;
then m + 1 in dom F by FINSEQ_1:def_3;
then F | (Seg (m + 1)) = G1 ^ <*{}*> by A11, FINSEQ_5:10;
then rng (F | (Seg (m + 1))) = (rng G1) \/ (rng <*{}*>) by FINSEQ_1:31
.= (rng G1) \/ {{}} by FINSEQ_1:39 ;
then union (rng (F | (Seg (m + 1)))) = (union (rng G1)) \/ (union {{}}) by ZFMISC_1:78
.= (union (rng G1)) \/ {} by ZFMISC_1:25
.= union (rng G1) ;
hence less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) = less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) ; ::_thesis: verum
end;
hence A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) in S by A8, A9, A10, MESFUNC1:def_16, XXREAL_0:2; ::_thesis: verum
end;
supposeA12: F . (m + 1) <> {} ; ::_thesis: A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) in S
reconsider G1 = F | (Seg m) as FinSequence of S by FINSEQ_1:18;
1 <= m + 1 by NAT_1:11;
then m + 1 in Seg (len F) by A9, FINSEQ_1:1;
then A13: m + 1 in dom F by FINSEQ_1:def_3;
then A14: F . (m + 1) in rng F by FUNCT_1:def_3;
then F . (m + 1) in S ;
then reconsider F1 = F . (m + 1) as Subset of X ;
consider x being Element of X such that
A15: x in F1 by A12, SUBSET_1:4;
F | (Seg (m + 1)) = G1 ^ <*(F . (m + 1))*> by A13, FINSEQ_5:10;
then rng (F | (Seg (m + 1))) = (rng G1) \/ (rng <*(F . (m + 1))*>) by FINSEQ_1:31
.= (rng G1) \/ {(F . (m + 1))} by FINSEQ_1:39 ;
then A16: union (rng (F | (Seg (m + 1)))) = (union (rng G1)) \/ (union {(F . (m + 1))}) by ZFMISC_1:78
.= (union (rng G1)) \/ (F . (m + 1)) by ZFMISC_1:25 ;
A17: x in dom f by A2, A14, A15, TARSKI:def_4;
f is V75() by A1, Def4;
then A18: |.(f . x).| < +infty by A17, Def1;
then - +infty < f . x by EXTREAL2:10;
then A19: -infty < f . x by XXREAL_3:def_3;
f . x < +infty by A18, EXTREAL2:10;
then reconsider r1 = f . x as Real by A19, XXREAL_0:14;
now__::_thesis:_A_/\_(less_dom_((f_|_(union_(rng_(F_|_(Seg_(m_+_1)))))),(R_EAL_r)))_in_S
percases ( r <= r1 or r1 < r ) ;
supposeA20: r <= r1 ; ::_thesis: A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) in S
for x1 being set st x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) holds
x1 in less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))
proof
let x1 be set ; ::_thesis: ( x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) implies x1 in less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) )
assume A21: x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) ; ::_thesis: x1 in less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))
then A22: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by MESFUNC1:def_11;
then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by RELAT_1:61;
then x1 in ((dom f) /\ (union (rng G1))) \/ ((dom f) /\ (F . (m + 1))) by A16, XBOOLE_1:23;
then A23: ( x1 in (dom f) /\ (union (rng G1)) or x1 in (dom f) /\ (F . (m + 1)) ) by XBOOLE_0:def_3;
reconsider x1 = x1 as Element of X by A21;
A24: (f | (union (rng (F | (Seg (m + 1)))))) . x1 < R_EAL r by A21, MESFUNC1:def_11;
A25: (f | (union (rng (F | (Seg (m + 1)))))) . x1 = f . x1 by A22, FUNCT_1:47;
set m1 = m + 1;
not x1 in dom (f | F1)
proof
assume x1 in dom (f | F1) ; ::_thesis: contradiction
then x1 in (dom f) /\ F1 by RELAT_1:61;
then x1 in F . (m + 1) by XBOOLE_0:def_4;
hence contradiction by A3, A13, A15, A20, A24, A25; ::_thesis: verum
end;
then A26: x1 in dom (f | (union (rng G1))) by A23, RELAT_1:61;
then (f | (union (rng (F | (Seg (m + 1)))))) . x1 = (f | (union (rng G1))) . x1 by A25, FUNCT_1:47;
hence x1 in less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) by A24, A26, MESFUNC1:def_11; ::_thesis: verum
end;
then A27: less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) c= less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) by TARSKI:def_3;
for x1 being set st x1 in less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) holds
x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))
proof
let x1 be set ; ::_thesis: ( x1 in less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) implies x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) )
assume A28: x1 in less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) ; ::_thesis: x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))
then A29: x1 in dom (f | (union (rng (F | (Seg m))))) by MESFUNC1:def_11;
then A30: x1 in (dom f) /\ (union (rng G1)) by RELAT_1:61;
then A31: x1 in union (rng G1) by XBOOLE_0:def_4;
A32: x1 in dom f by A30, XBOOLE_0:def_4;
x1 in union (rng (F | (Seg (m + 1)))) by A16, A31, XBOOLE_0:def_3;
then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by A32, XBOOLE_0:def_4;
then A33: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by RELAT_1:61;
reconsider x1 = x1 as Element of X by A28;
A34: (f | (union (rng (F | (Seg m))))) . x1 < R_EAL r by A28, MESFUNC1:def_11;
(f | (union (rng (F | (Seg m))))) . x1 = f . x1 by A29, FUNCT_1:47;
then (f | (union (rng (F | (Seg m))))) . x1 = (f | (union (rng (F | (Seg (m + 1)))))) . x1 by A33, FUNCT_1:47;
hence x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) by A33, A34, MESFUNC1:def_11; ::_thesis: verum
end;
then less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) c= less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) by TARSKI:def_3;
then less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) = less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) by A27, XBOOLE_0:def_10;
hence A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) in S by A8, A9, A10, MESFUNC1:def_16, XXREAL_0:2; ::_thesis: verum
end;
supposeA35: r1 < r ; ::_thesis: A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) in S
for x1 being set st x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) holds
x1 in (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (F . (m + 1))
proof
let x1 be set ; ::_thesis: ( x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) implies x1 in (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (F . (m + 1)) )
assume A36: x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) ; ::_thesis: x1 in (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (F . (m + 1))
then A37: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by MESFUNC1:def_11;
then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by RELAT_1:61;
then A38: x1 in ((dom f) /\ (union (rng G1))) \/ ((dom f) /\ (F . (m + 1))) by A16, XBOOLE_1:23;
now__::_thesis:_x1_in_(less_dom_((f_|_(union_(rng_(F_|_(Seg_m))))),(R_EAL_r)))_\/_(F_._(m_+_1))
percases ( x1 in (dom f) /\ (union (rng G1)) or x1 in (dom f) /\ (F . (m + 1)) ) by A38, XBOOLE_0:def_3;
supposeA39: x1 in (dom f) /\ (union (rng G1)) ; ::_thesis: x1 in (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (F . (m + 1))
then reconsider x1 = x1 as Element of X ;
A40: x1 in dom (f | (union (rng G1))) by A39, RELAT_1:61;
then A41: (f | (union (rng G1))) . x1 = f . x1 by FUNCT_1:47;
A42: (f | (union (rng (F | (Seg (m + 1)))))) . x1 < R_EAL r by A36, MESFUNC1:def_11;
(f | (union (rng (F | (Seg (m + 1)))))) . x1 = (f | (union (rng G1))) . x1 by A37, A41, FUNCT_1:47;
then x1 in less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) by A40, A42, MESFUNC1:def_11;
hence x1 in (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (F . (m + 1)) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x1 in (dom f) /\ (F . (m + 1)) ; ::_thesis: x1 in (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (F . (m + 1))
then x1 in F . (m + 1) by XBOOLE_0:def_4;
hence x1 in (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (F . (m + 1)) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence x1 in (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (F . (m + 1)) ; ::_thesis: verum
end;
then A43: less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) c= (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (F . (m + 1)) by TARSKI:def_3;
for x1 being set st x1 in (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (F . (m + 1)) holds
x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))
proof
let x1 be set ; ::_thesis: ( x1 in (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (F . (m + 1)) implies x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) )
assume A44: x1 in (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (F . (m + 1)) ; ::_thesis: x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))
now__::_thesis:_x1_in_less_dom_((f_|_(union_(rng_(F_|_(Seg_(m_+_1)))))),(R_EAL_r))
percases ( x1 in less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) or x1 in F . (m + 1) ) by A44, XBOOLE_0:def_3;
supposeA45: x1 in less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) ; ::_thesis: x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))
then A46: x1 in dom (f | (union (rng (F | (Seg m))))) by MESFUNC1:def_11;
then A47: x1 in (dom f) /\ (union (rng G1)) by RELAT_1:61;
then A48: x1 in union (rng G1) by XBOOLE_0:def_4;
A49: x1 in dom f by A47, XBOOLE_0:def_4;
x1 in union (rng (F | (Seg (m + 1)))) by A16, A48, XBOOLE_0:def_3;
then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by A49, XBOOLE_0:def_4;
then A50: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by RELAT_1:61;
reconsider x1 = x1 as Element of X by A45;
A51: (f | (union (rng (F | (Seg m))))) . x1 < R_EAL r by A45, MESFUNC1:def_11;
(f | (union (rng (F | (Seg m))))) . x1 = f . x1 by A46, FUNCT_1:47;
then (f | (union (rng (F | (Seg m))))) . x1 = (f | (union (rng (F | (Seg (m + 1)))))) . x1 by A50, FUNCT_1:47;
hence x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) by A50, A51, MESFUNC1:def_11; ::_thesis: verum
end;
supposeA52: x1 in F . (m + 1) ; ::_thesis: x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))
then A53: x1 in union (rng (F | (Seg (m + 1)))) by A16, XBOOLE_0:def_3;
A54: x1 in dom f by A2, A14, A52, TARSKI:def_4;
then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by A53, XBOOLE_0:def_4;
then A55: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by RELAT_1:61;
reconsider x1 = x1 as Element of X by A54;
A56: f . x1 = R_EAL r1 by A3, A13, A15, A52;
reconsider y = f . x1 as R_eal ;
y = (f | (union (rng (F | (Seg (m + 1)))))) . x1 by A55, FUNCT_1:47;
hence x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) by A35, A55, A56, MESFUNC1:def_11; ::_thesis: verum
end;
end;
end;
hence x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) ; ::_thesis: verum
end;
then (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (F . (m + 1)) c= less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) by TARSKI:def_3;
then less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) = (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (F . (m + 1)) by A43, XBOOLE_0:def_10;
then A57: A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) = (A /\ (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)))) \/ (A /\ (F . (m + 1))) by XBOOLE_1:23;
( A /\ (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) in S & A /\ (F . (m + 1)) in S ) by A8, A9, A10, A14, FINSUB_1:def_2, MESFUNC1:def_16, XXREAL_0:2;
hence A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) in S by A57, FINSUB_1:def_1; ::_thesis: verum
end;
end;
end;
hence A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) in S ; ::_thesis: verum
end;
end;
end;
hence A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) in S ; ::_thesis: verum
end;
hence f | (union (rng (F | (Seg (m + 1))))) is_measurable_on A by MESFUNC1:def_16; ::_thesis: verum
end;
hence S1[m + 1] ; ::_thesis: verum
end;
A58: for n being Nat holds S1[n] from NAT_1:sch_2(A4, A7);
F | (Seg (len F)) = F by FINSEQ_3:49;
then f | (dom f) is_measurable_on A by A2, A58;
hence f is_measurable_on A by RELAT_1:68; ::_thesis: verum
end;