:: MESFUNC8 semantic presentation
begin
theorem Th1: :: MESFUNC8:1
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Function of NAT,S
for n being Nat holds { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } is Element of S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being Function of NAT,S
for n being Nat holds { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } is Element of S
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for F being Function of NAT,S
for n being Nat holds { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } is Element of S
let M be sigma_Measure of S; ::_thesis: for F being Function of NAT,S
for n being Nat holds { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } is Element of S
let F be Function of NAT,S; ::_thesis: for n being Nat holds { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } is Element of S
let n be Nat; ::_thesis: { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } is Element of S
set G = { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } ;
deffunc H1( Element of NAT ) -> Element of S = F . (n + $1);
consider E being Function of NAT,S such that
A1: for k being Element of NAT holds E . k = H1(k) from FUNCT_2:sch_4();
now__::_thesis:_for_z_being_set_st_z_in__{__x_where_x_is_Element_of_X_:_for_k_being_Nat_st_n_<=_k_holds_
x_in_F_._k__}__holds_
z_in_meet_(rng_E)
let z be set ; ::_thesis: ( z in { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } implies z in meet (rng E) )
assume z in { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } ; ::_thesis: z in meet (rng E)
then A2: ex x being Element of X st
( z = x & ( for k being Nat st n <= k holds
x in F . k ) ) ;
for Y being set st Y in rng E holds
z in Y
proof
let Y be set ; ::_thesis: ( Y in rng E implies z in Y )
assume Y in rng E ; ::_thesis: z in Y
then consider l being set such that
A3: l in NAT and
A4: Y = E . l by FUNCT_2:11;
reconsider l = l as Element of NAT by A3;
z in F . (n + l) by A2, NAT_1:12;
hence z in Y by A1, A4; ::_thesis: verum
end;
hence z in meet (rng E) by SETFAM_1:def_1; ::_thesis: verum
end;
then A5: { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } c= meet (rng E) by TARSKI:def_3;
rng E is N_Sub_set_fam of X by MEASURE1:23;
then rng E is N_Measure_fam of S by MEASURE2:def_1;
then A6: meet (rng E) is Element of S by MEASURE2:2;
now__::_thesis:_for_z_being_set_st_z_in_meet_(rng_E)_holds_
z_in__{__x_where_x_is_Element_of_X_:_for_k_being_Nat_st_n_<=_k_holds_
x_in_F_._k__}_
let z be set ; ::_thesis: ( z in meet (rng E) implies z in { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } )
assume A7: z in meet (rng E) ; ::_thesis: z in { x where x is Element of X : for k being Nat st n <= k holds
x in F . k }
now__::_thesis:_for_k_being_Nat_st_n_<=_k_holds_
z_in_F_._k
let k be Nat; ::_thesis: ( n <= k implies z in F . k )
assume n <= k ; ::_thesis: z in F . k
then reconsider l = k - n as Element of NAT by NAT_1:21;
E . l in rng E by FUNCT_2:4;
then z in E . l by A7, SETFAM_1:def_1;
then z in F . (n + l) by A1;
hence z in F . k ; ::_thesis: verum
end;
hence z in { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } by A6, A7; ::_thesis: verum
end;
then meet (rng E) c= { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } by TARSKI:def_3;
hence { x where x is Element of X : for k being Nat st n <= k holds
x in F . k } is Element of S by A6, A5, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th2: :: MESFUNC8:2
for X being non empty set
for F being SetSequence of X
for n being Element of NAT holds
( (superior_setsequence F) . n = union (rng (F ^\ n)) & (inferior_setsequence F) . n = meet (rng (F ^\ n)) )
proof
let X be non empty set ; ::_thesis: for F being SetSequence of X
for n being Element of NAT holds
( (superior_setsequence F) . n = union (rng (F ^\ n)) & (inferior_setsequence F) . n = meet (rng (F ^\ n)) )
let F be SetSequence of X; ::_thesis: for n being Element of NAT holds
( (superior_setsequence F) . n = union (rng (F ^\ n)) & (inferior_setsequence F) . n = meet (rng (F ^\ n)) )
let n be Element of NAT ; ::_thesis: ( (superior_setsequence F) . n = union (rng (F ^\ n)) & (inferior_setsequence F) . n = meet (rng (F ^\ n)) )
{ (F . k) where k is Element of NAT : n <= k } = rng (F ^\ n) by SETLIM_1:6;
hence (superior_setsequence F) . n = union (rng (F ^\ n)) by SETLIM_1:def_3; ::_thesis: (inferior_setsequence F) . n = meet (rng (F ^\ n))
(inferior_setsequence F) . n = meet { (F . k) where k is Element of NAT : n <= k } by SETLIM_1:def_2;
hence (inferior_setsequence F) . n = meet (rng (F ^\ n)) by SETLIM_1:6; ::_thesis: verum
end;
theorem Th3: :: MESFUNC8:3
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being SetSequence of S ex G being Function of NAT,S st
( G = inferior_setsequence F & M . (lim_inf F) = sup (rng (M * G)) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being SetSequence of S ex G being Function of NAT,S st
( G = inferior_setsequence F & M . (lim_inf F) = sup (rng (M * G)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for F being SetSequence of S ex G being Function of NAT,S st
( G = inferior_setsequence F & M . (lim_inf F) = sup (rng (M * G)) )
let M be sigma_Measure of S; ::_thesis: for F being SetSequence of S ex G being Function of NAT,S st
( G = inferior_setsequence F & M . (lim_inf F) = sup (rng (M * G)) )
let F be SetSequence of S; ::_thesis: ex G being Function of NAT,S st
( G = inferior_setsequence F & M . (lim_inf F) = sup (rng (M * G)) )
rng (inferior_setsequence F) c= S ;
then reconsider G = inferior_setsequence F as Function of NAT,S by FUNCT_2:6;
now__::_thesis:_for_n_being_Element_of_NAT_holds_G_._n_c=_G_._(n_+_1)
let n be Element of NAT ; ::_thesis: G . n c= G . (n + 1)
n <= n + 1 by NAT_1:12;
hence G . n c= G . (n + 1) by PROB_1:def_5; ::_thesis: verum
end;
then M . (union (rng G)) = sup (rng (M * G)) by MEASURE2:23;
hence ex G being Function of NAT,S st
( G = inferior_setsequence F & M . (lim_inf F) = sup (rng (M * G)) ) ; ::_thesis: verum
end;
theorem Th4: :: MESFUNC8:4
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being SetSequence of S st M . (Union F) < +infty holds
ex G being Function of NAT,S st
( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being SetSequence of S st M . (Union F) < +infty holds
ex G being Function of NAT,S st
( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for F being SetSequence of S st M . (Union F) < +infty holds
ex G being Function of NAT,S st
( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) )
let M be sigma_Measure of S; ::_thesis: for F being SetSequence of S st M . (Union F) < +infty holds
ex G being Function of NAT,S st
( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) )
let F be SetSequence of S; ::_thesis: ( M . (Union F) < +infty implies ex G being Function of NAT,S st
( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) ) )
rng (superior_setsequence F) c= S ;
then reconsider G = superior_setsequence F as Function of NAT,S by FUNCT_2:6;
reconsider F1 = F, G1 = G as SetSequence of X ;
A1: for n being Element of NAT holds G . (n + 1) c= G . n
proof
let n be Element of NAT ; ::_thesis: G . (n + 1) c= G . n
n <= n + 1 by NAT_1:12;
hence G . (n + 1) c= G . n by PROB_1:def_4; ::_thesis: verum
end;
G . 0 = union { (F . k) where k is Element of NAT : 0 <= k } by SETLIM_1:def_3;
then A2: G . 0 = union (rng F) by SETLIM_1:5;
consider f being SetSequence of X such that
A3: lim_sup F1 = meet f and
A4: for n being Element of NAT holds f . n = Union (F1 ^\ n) by KURATO_0:def_2;
now__::_thesis:_for_n_being_Element_of_NAT_holds_f_._n_=_G1_._n
let n be Element of NAT ; ::_thesis: f . n = G1 . n
f . n = Union (F1 ^\ n) by A4;
hence f . n = G1 . n by Th2; ::_thesis: verum
end;
then A5: f = G1 by FUNCT_2:63;
assume M . (Union F) < +infty ; ::_thesis: ex G being Function of NAT,S st
( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) )
then M . (meet (rng G)) = inf (rng (M * G)) by A1, A2, MEASURE3:12;
hence ex G being Function of NAT,S st
( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) ) by A3, A5; ::_thesis: verum
end;
theorem :: MESFUNC8:5
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being SetSequence of S st F is convergent holds
ex G being Function of NAT,S st
( G = inferior_setsequence F & M . (lim F) = sup (rng (M * G)) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being SetSequence of S st F is convergent holds
ex G being Function of NAT,S st
( G = inferior_setsequence F & M . (lim F) = sup (rng (M * G)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for F being SetSequence of S st F is convergent holds
ex G being Function of NAT,S st
( G = inferior_setsequence F & M . (lim F) = sup (rng (M * G)) )
let M be sigma_Measure of S; ::_thesis: for F being SetSequence of S st F is convergent holds
ex G being Function of NAT,S st
( G = inferior_setsequence F & M . (lim F) = sup (rng (M * G)) )
let F be SetSequence of S; ::_thesis: ( F is convergent implies ex G being Function of NAT,S st
( G = inferior_setsequence F & M . (lim F) = sup (rng (M * G)) ) )
assume F is convergent ; ::_thesis: ex G being Function of NAT,S st
( G = inferior_setsequence F & M . (lim F) = sup (rng (M * G)) )
then lim_inf F = lim F by KURATO_0:def_5;
hence ex G being Function of NAT,S st
( G = inferior_setsequence F & M . (lim F) = sup (rng (M * G)) ) by Th3; ::_thesis: verum
end;
theorem :: MESFUNC8:6
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being SetSequence of S st F is convergent & M . (Union F) < +infty holds
ex G being Function of NAT,S st
( G = superior_setsequence F & M . (lim F) = inf (rng (M * G)) ) by Th4;
definition
let X, Y be set ;
let F be Functional_Sequence of X,Y;
attrF is with_the_same_dom means :Def1: :: MESFUNC8:def 1
rng F is with_common_domain ;
end;
:: deftheorem Def1 defines with_the_same_dom MESFUNC8:def_1_:_
for X, Y being set
for F being Functional_Sequence of X,Y holds
( F is with_the_same_dom iff rng F is with_common_domain );
definition
let X, Y be set ;
let F be Functional_Sequence of X,Y;
redefine attr F is with_the_same_dom means :Def2: :: MESFUNC8:def 2
for n, m being Nat holds dom (F . n) = dom (F . m);
correctness
compatibility
( F is with_the_same_dom iff for n, m being Nat holds dom (F . n) = dom (F . m) );
proof
A1: ( ( for n, m being Nat holds dom (F . n) = dom (F . m) ) implies F is with_the_same_dom )
proof
assume A2: for n, m being Nat holds dom (F . n) = dom (F . m) ; ::_thesis: F is with_the_same_dom
now__::_thesis:_for_f,_g_being_Function_st_f_in_rng_F_&_g_in_rng_F_holds_
dom_f_=_dom_g
let f, g be Function; ::_thesis: ( f in rng F & g in rng F implies dom f = dom g )
assume that
A3: f in rng F and
A4: g in rng F ; ::_thesis: dom f = dom g
consider m being set such that
A5: m in dom F and
A6: g = F . m by A4, FUNCT_1:def_3;
consider n being set such that
A7: n in dom F and
A8: f = F . n by A3, FUNCT_1:def_3;
reconsider n = n, m = m as Nat by A7, A5;
dom (F . n) = dom (F . m) by A2;
hence dom f = dom g by A8, A6; ::_thesis: verum
end;
then rng F is with_common_domain by CARD_3:def_10;
hence F is with_the_same_dom by Def1; ::_thesis: verum
end;
( F is with_the_same_dom implies for n, m being Nat holds dom (F . n) = dom (F . m) )
proof
assume F is with_the_same_dom ; ::_thesis: for n, m being Nat holds dom (F . n) = dom (F . m)
then A9: rng F is with_common_domain by Def1;
hereby ::_thesis: verum
let n, m be Nat; ::_thesis: dom (F . n) = dom (F . m)
A10: dom F = NAT by FUNCT_2:def_1;
then m in dom F by ORDINAL1:def_12;
then A11: F . m in rng F by FUNCT_1:3;
n in dom F by A10, ORDINAL1:def_12;
then F . n in rng F by FUNCT_1:3;
hence dom (F . n) = dom (F . m) by A9, A11, CARD_3:def_10; ::_thesis: verum
end;
end;
hence ( F is with_the_same_dom iff for n, m being Nat holds dom (F . n) = dom (F . m) ) by A1; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines with_the_same_dom MESFUNC8:def_2_:_
for X, Y being set
for F being Functional_Sequence of X,Y holds
( F is with_the_same_dom iff for n, m being Nat holds dom (F . n) = dom (F . m) );
registration
let X, Y be set ;
cluster non empty Relation-like NAT -defined PFuncs (X,Y) -valued Function-like total V30( NAT , PFuncs (X,Y)) with_the_same_dom for Element of bool [:NAT,(PFuncs (X,Y)):];
existence
ex b1 being Functional_Sequence of X,Y st b1 is with_the_same_dom
proof
deffunc H1( Nat) -> Element of bool [:X,Y:] = <:{},X,Y:>;
consider F being Functional_Sequence of X,Y such that
A1: for n being Nat holds F . n = H1(n) from SEQFUNC:sch_1();
take F ; ::_thesis: F is with_the_same_dom
hereby :: according to MESFUNC8:def_2 ::_thesis: verum
let n, m be Nat; ::_thesis: dom (F . n) = dom (F . m)
F . n = <:{},X,Y:> by A1;
hence dom (F . n) = dom (F . m) by A1; ::_thesis: verum
end;
end;
end;
definition
let X be non empty set ;
let f be Functional_Sequence of X,ExtREAL;
func inf f -> PartFunc of X,ExtREAL means :Def3: :: MESFUNC8:def 3
( dom it = dom (f . 0) & ( for x being Element of X st x in dom it holds
it . x = inf (f # x) ) );
existence
ex b1 being PartFunc of X,ExtREAL st
( dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds
b1 . x = inf (f # x) ) )
proof
defpred S1[ set ] means $1 in dom (f . 0);
deffunc H1( Element of X) -> Element of ExtREAL = inf (f # $1);
consider g being PartFunc of X,ExtREAL such that
A1: ( ( for x being Element of X holds
( x in dom g iff S1[x] ) ) & ( for x being Element of X st x in dom g holds
g /. x = H1(x) ) ) from PARTFUN2:sch_2();
take g ; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = inf (f # x) ) )
A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_._x_=_inf_(f_#_x)
let x be Element of X; ::_thesis: ( x in dom g implies g . x = inf (f # x) )
assume A3: x in dom g ; ::_thesis: g . x = inf (f # x)
then g /. x = inf (f # x) by A1;
hence g . x = inf (f # x) by A3, PARTFUN1:def_6; ::_thesis: verum
end;
for x being set holds
( x in dom g iff x in dom (f . 0) ) by A1;
hence ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = inf (f # x) ) ) by A2, TARSKI:1; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds
b1 . x = inf (f # x) ) & dom b2 = dom (f . 0) & ( for x being Element of X st x in dom b2 holds
b2 . x = inf (f # x) ) holds
b1 = b2
proof
let g, h be PartFunc of X,ExtREAL; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = inf (f # x) ) & dom h = dom (f . 0) & ( for x being Element of X st x in dom h holds
h . x = inf (f # x) ) implies g = h )
assume that
A4: dom g = dom (f . 0) and
A5: for x being Element of X st x in dom g holds
g . x = inf (f # x) ; ::_thesis: ( not dom h = dom (f . 0) or ex x being Element of X st
( x in dom h & not h . x = inf (f # x) ) or g = h )
assume that
A6: dom h = dom (f . 0) and
A7: for x being Element of X st x in dom h holds
h . x = inf (f # x) ; ::_thesis: g = h
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_/._x_=_h_/._x
let x be Element of X; ::_thesis: ( x in dom g implies g /. x = h /. x )
assume A8: x in dom g ; ::_thesis: g /. x = h /. x
then g /. x = g . x by PARTFUN1:def_6;
then g /. x = inf (f # x) by A5, A8;
then g /. x = h . x by A4, A6, A7, A8;
hence g /. x = h /. x by A4, A6, A8, PARTFUN1:def_6; ::_thesis: verum
end;
hence g = h by A4, A6, PARTFUN2:1; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines inf MESFUNC8:def_3_:_
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b3 being PartFunc of X,ExtREAL holds
( b3 = inf f iff ( dom b3 = dom (f . 0) & ( for x being Element of X st x in dom b3 holds
b3 . x = inf (f # x) ) ) );
definition
let X be non empty set ;
let f be Functional_Sequence of X,ExtREAL;
func sup f -> PartFunc of X,ExtREAL means :Def4: :: MESFUNC8:def 4
( dom it = dom (f . 0) & ( for x being Element of X st x in dom it holds
it . x = sup (f # x) ) );
existence
ex b1 being PartFunc of X,ExtREAL st
( dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds
b1 . x = sup (f # x) ) )
proof
defpred S1[ set ] means $1 in dom (f . 0);
deffunc H1( Element of X) -> Element of ExtREAL = sup (f # $1);
consider g being PartFunc of X,ExtREAL such that
A1: ( ( for x being Element of X holds
( x in dom g iff S1[x] ) ) & ( for x being Element of X st x in dom g holds
g /. x = H1(x) ) ) from PARTFUN2:sch_2();
take g ; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = sup (f # x) ) )
A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_._x_=_sup_(f_#_x)
let x be Element of X; ::_thesis: ( x in dom g implies g . x = sup (f # x) )
assume A3: x in dom g ; ::_thesis: g . x = sup (f # x)
then g /. x = sup (f # x) by A1;
hence g . x = sup (f # x) by A3, PARTFUN1:def_6; ::_thesis: verum
end;
for x being set holds
( x in dom g iff x in dom (f . 0) ) by A1;
hence ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = sup (f # x) ) ) by A2, TARSKI:1; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds
b1 . x = sup (f # x) ) & dom b2 = dom (f . 0) & ( for x being Element of X st x in dom b2 holds
b2 . x = sup (f # x) ) holds
b1 = b2
proof
let g, h be PartFunc of X,ExtREAL; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = sup (f # x) ) & dom h = dom (f . 0) & ( for x being Element of X st x in dom h holds
h . x = sup (f # x) ) implies g = h )
assume that
A4: dom g = dom (f . 0) and
A5: for x being Element of X st x in dom g holds
g . x = sup (f # x) ; ::_thesis: ( not dom h = dom (f . 0) or ex x being Element of X st
( x in dom h & not h . x = sup (f # x) ) or g = h )
assume that
A6: dom h = dom (f . 0) and
A7: for x being Element of X st x in dom h holds
h . x = sup (f # x) ; ::_thesis: g = h
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_/._x_=_h_/._x
let x be Element of X; ::_thesis: ( x in dom g implies g /. x = h /. x )
assume A8: x in dom g ; ::_thesis: g /. x = h /. x
then g /. x = g . x by PARTFUN1:def_6;
then g /. x = sup (f # x) by A5, A8;
then g /. x = h . x by A4, A6, A7, A8;
hence g /. x = h /. x by A4, A6, A8, PARTFUN1:def_6; ::_thesis: verum
end;
hence g = h by A4, A6, PARTFUN2:1; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines sup MESFUNC8:def_4_:_
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b3 being PartFunc of X,ExtREAL holds
( b3 = sup f iff ( dom b3 = dom (f . 0) & ( for x being Element of X st x in dom b3 holds
b3 . x = sup (f # x) ) ) );
definition
let X be non empty set ;
let f be Functional_Sequence of X,ExtREAL;
func inferior_realsequence f -> with_the_same_dom Functional_Sequence of X,ExtREAL means :Def5: :: MESFUNC8:def 5
for n being Nat holds
( dom (it . n) = dom (f . 0) & ( for x being Element of X st x in dom (it . n) holds
(it . n) . x = (inferior_realsequence (f # x)) . n ) );
existence
ex b1 being with_the_same_dom Functional_Sequence of X,ExtREAL st
for n being Nat holds
( dom (b1 . n) = dom (f . 0) & ( for x being Element of X st x in dom (b1 . n) holds
(b1 . n) . x = (inferior_realsequence (f # x)) . n ) )
proof
defpred S1[ Element of NAT , Function] means ( dom $2 = dom (f . 0) & ( for x being Element of X st x in dom $2 holds
$2 . x = (inferior_realsequence (f # x)) . $1 ) );
A1: for n being Element of NAT ex y being Element of PFuncs (X,ExtREAL) st S1[n,y]
proof
defpred S2[ set ] means $1 in dom (f . 0);
let n be Element of NAT ; ::_thesis: ex y being Element of PFuncs (X,ExtREAL) st S1[n,y]
deffunc H1( Element of X) -> Element of ExtREAL = (inferior_realsequence (f # $1)) . n;
consider g being PartFunc of X,ExtREAL such that
A2: ( ( for x being Element of X holds
( x in dom g iff S2[x] ) ) & ( for x being Element of X st x in dom g holds
g /. x = H1(x) ) ) from PARTFUN2:sch_2();
take g ; ::_thesis: ( g is Element of PFuncs (X,ExtREAL) & S1[n,g] )
A3: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_._x_=_(inferior_realsequence_(f_#_x))_._n
let x be Element of X; ::_thesis: ( x in dom g implies g . x = (inferior_realsequence (f # x)) . n )
assume A4: x in dom g ; ::_thesis: g . x = (inferior_realsequence (f # x)) . n
then g /. x = (inferior_realsequence (f # x)) . n by A2;
hence g . x = (inferior_realsequence (f # x)) . n by A4, PARTFUN1:def_6; ::_thesis: verum
end;
for x being set holds
( x in dom g iff x in dom (f . 0) ) by A2;
hence ( g is Element of PFuncs (X,ExtREAL) & S1[n,g] ) by A3, PARTFUN1:45, TARSKI:1; ::_thesis: verum
end;
consider g being Function of NAT,(PFuncs (X,ExtREAL)) such that
A5: for n being Element of NAT holds S1[n,g . n] from FUNCT_2:sch_3(A1);
A6: for n being Nat holds
( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (inferior_realsequence (f # x)) . n ) )
proof
let n be Nat; ::_thesis: ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (inferior_realsequence (f # x)) . n ) )
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
dom (g . n9) = dom (f . 0) by A5;
hence ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (inferior_realsequence (f # x)) . n ) ) by A5; ::_thesis: verum
end;
reconsider g = g as Functional_Sequence of X,ExtREAL ;
now__::_thesis:_for_k,_l_being_Nat_holds_dom_(g_._k)_=_dom_(g_._l)
let k, l be Nat; ::_thesis: dom (g . k) = dom (g . l)
reconsider k9 = k, l9 = l as Element of NAT by ORDINAL1:def_12;
dom (g . k9) = dom (f . 0) by A5;
then dom (g . k) = dom (g . l9) by A5;
hence dom (g . k) = dom (g . l) ; ::_thesis: verum
end;
then reconsider g = g as with_the_same_dom Functional_Sequence of X,ExtREAL by Def2;
take g ; ::_thesis: for n being Nat holds
( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (inferior_realsequence (f # x)) . n ) )
thus for n being Nat holds
( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (inferior_realsequence (f # x)) . n ) ) by A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being with_the_same_dom Functional_Sequence of X,ExtREAL st ( for n being Nat holds
( dom (b1 . n) = dom (f . 0) & ( for x being Element of X st x in dom (b1 . n) holds
(b1 . n) . x = (inferior_realsequence (f # x)) . n ) ) ) & ( for n being Nat holds
( dom (b2 . n) = dom (f . 0) & ( for x being Element of X st x in dom (b2 . n) holds
(b2 . n) . x = (inferior_realsequence (f # x)) . n ) ) ) holds
b1 = b2
proof
let g, h be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: ( ( for n being Nat holds
( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (inferior_realsequence (f # x)) . n ) ) ) & ( for n being Nat holds
( dom (h . n) = dom (f . 0) & ( for x being Element of X st x in dom (h . n) holds
(h . n) . x = (inferior_realsequence (f # x)) . n ) ) ) implies g = h )
assume A7: for n being Nat holds
( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (inferior_realsequence (f # x)) . n ) ) ; ::_thesis: ( ex n being Nat st
( dom (h . n) = dom (f . 0) implies ex x being Element of X st
( x in dom (h . n) & not (h . n) . x = (inferior_realsequence (f # x)) . n ) ) or g = h )
assume A8: for n being Nat holds
( dom (h . n) = dom (f . 0) & ( for x being Element of X st x in dom (h . n) holds
(h . n) . x = (inferior_realsequence (f # x)) . n ) ) ; ::_thesis: g = h
now__::_thesis:_for_n_being_Element_of_NAT_holds_g_._n_=_h_._n
let n be Element of NAT ; ::_thesis: g . n = h . n
A9: dom (g . n) = dom (f . 0) by A7
.= dom (h . n) by A8 ;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(g_._n)_holds_
(g_._n)_/._x_=_(h_._n)_/._x
let x be Element of X; ::_thesis: ( x in dom (g . n) implies (g . n) /. x = (h . n) /. x )
assume A10: x in dom (g . n) ; ::_thesis: (g . n) /. x = (h . n) /. x
then (g . n) /. x = (g . n) . x by PARTFUN1:def_6;
then (g . n) /. x = (inferior_realsequence (f # x)) . n by A7, A10;
then (g . n) /. x = (h . n) . x by A8, A9, A10;
hence (g . n) /. x = (h . n) /. x by A9, A10, PARTFUN1:def_6; ::_thesis: verum
end;
hence g . n = h . n by A9, PARTFUN2:1; ::_thesis: verum
end;
hence g = h by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines inferior_realsequence MESFUNC8:def_5_:_
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b3 being with_the_same_dom Functional_Sequence of X,ExtREAL holds
( b3 = inferior_realsequence f iff for n being Nat holds
( dom (b3 . n) = dom (f . 0) & ( for x being Element of X st x in dom (b3 . n) holds
(b3 . n) . x = (inferior_realsequence (f # x)) . n ) ) );
definition
let X be non empty set ;
let f be Functional_Sequence of X,ExtREAL;
func superior_realsequence f -> with_the_same_dom Functional_Sequence of X,ExtREAL means :Def6: :: MESFUNC8:def 6
for n being Nat holds
( dom (it . n) = dom (f . 0) & ( for x being Element of X st x in dom (it . n) holds
(it . n) . x = (superior_realsequence (f # x)) . n ) );
existence
ex b1 being with_the_same_dom Functional_Sequence of X,ExtREAL st
for n being Nat holds
( dom (b1 . n) = dom (f . 0) & ( for x being Element of X st x in dom (b1 . n) holds
(b1 . n) . x = (superior_realsequence (f # x)) . n ) )
proof
defpred S1[ Element of NAT , Function] means ( dom $2 = dom (f . 0) & ( for x being Element of X st x in dom $2 holds
$2 . x = (superior_realsequence (f # x)) . $1 ) );
A1: for n being Element of NAT ex y being Element of PFuncs (X,ExtREAL) st S1[n,y]
proof
defpred S2[ set ] means $1 in dom (f . 0);
let n be Element of NAT ; ::_thesis: ex y being Element of PFuncs (X,ExtREAL) st S1[n,y]
deffunc H1( Element of X) -> Element of ExtREAL = (superior_realsequence (f # $1)) . n;
consider g being PartFunc of X,ExtREAL such that
A2: ( ( for x being Element of X holds
( x in dom g iff S2[x] ) ) & ( for x being Element of X st x in dom g holds
g /. x = H1(x) ) ) from PARTFUN2:sch_2();
take g ; ::_thesis: ( g is Element of PFuncs (X,ExtREAL) & S1[n,g] )
A3: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_._x_=_(superior_realsequence_(f_#_x))_._n
let x be Element of X; ::_thesis: ( x in dom g implies g . x = (superior_realsequence (f # x)) . n )
assume A4: x in dom g ; ::_thesis: g . x = (superior_realsequence (f # x)) . n
then g /. x = (superior_realsequence (f # x)) . n by A2;
hence g . x = (superior_realsequence (f # x)) . n by A4, PARTFUN1:def_6; ::_thesis: verum
end;
for x being set holds
( x in dom g iff x in dom (f . 0) ) by A2;
hence ( g is Element of PFuncs (X,ExtREAL) & S1[n,g] ) by A3, PARTFUN1:45, TARSKI:1; ::_thesis: verum
end;
consider g being Function of NAT,(PFuncs (X,ExtREAL)) such that
A5: for n being Element of NAT holds S1[n,g . n] from FUNCT_2:sch_3(A1);
A6: for n being Nat holds
( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (superior_realsequence (f # x)) . n ) )
proof
let n be Nat; ::_thesis: ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (superior_realsequence (f # x)) . n ) )
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
dom (g . n9) = dom (f . 0) by A5;
hence ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (superior_realsequence (f # x)) . n ) ) by A5; ::_thesis: verum
end;
reconsider g = g as Functional_Sequence of X,ExtREAL ;
now__::_thesis:_for_k,_l_being_Nat_holds_dom_(g_._k)_=_dom_(g_._l)
let k, l be Nat; ::_thesis: dom (g . k) = dom (g . l)
reconsider k9 = k, l9 = l as Element of NAT by ORDINAL1:def_12;
dom (g . k9) = dom (f . 0) by A5;
then dom (g . k) = dom (g . l9) by A5;
hence dom (g . k) = dom (g . l) ; ::_thesis: verum
end;
then reconsider g = g as with_the_same_dom Functional_Sequence of X,ExtREAL by Def2;
take g ; ::_thesis: for n being Nat holds
( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (superior_realsequence (f # x)) . n ) )
thus for n being Nat holds
( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (superior_realsequence (f # x)) . n ) ) by A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being with_the_same_dom Functional_Sequence of X,ExtREAL st ( for n being Nat holds
( dom (b1 . n) = dom (f . 0) & ( for x being Element of X st x in dom (b1 . n) holds
(b1 . n) . x = (superior_realsequence (f # x)) . n ) ) ) & ( for n being Nat holds
( dom (b2 . n) = dom (f . 0) & ( for x being Element of X st x in dom (b2 . n) holds
(b2 . n) . x = (superior_realsequence (f # x)) . n ) ) ) holds
b1 = b2
proof
let g, h be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: ( ( for n being Nat holds
( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (superior_realsequence (f # x)) . n ) ) ) & ( for n being Nat holds
( dom (h . n) = dom (f . 0) & ( for x being Element of X st x in dom (h . n) holds
(h . n) . x = (superior_realsequence (f # x)) . n ) ) ) implies g = h )
assume A7: for n being Nat holds
( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (superior_realsequence (f # x)) . n ) ) ; ::_thesis: ( ex n being Nat st
( dom (h . n) = dom (f . 0) implies ex x being Element of X st
( x in dom (h . n) & not (h . n) . x = (superior_realsequence (f # x)) . n ) ) or g = h )
assume A8: for n being Nat holds
( dom (h . n) = dom (f . 0) & ( for x being Element of X st x in dom (h . n) holds
(h . n) . x = (superior_realsequence (f # x)) . n ) ) ; ::_thesis: g = h
now__::_thesis:_for_n_being_Element_of_NAT_holds_g_._n_=_h_._n
let n be Element of NAT ; ::_thesis: g . n = h . n
A9: dom (g . n) = dom (f . 0) by A7
.= dom (h . n) by A8 ;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(g_._n)_holds_
(g_._n)_/._x_=_(h_._n)_/._x
let x be Element of X; ::_thesis: ( x in dom (g . n) implies (g . n) /. x = (h . n) /. x )
assume A10: x in dom (g . n) ; ::_thesis: (g . n) /. x = (h . n) /. x
then (g . n) /. x = (g . n) . x by PARTFUN1:def_6;
then (g . n) /. x = (superior_realsequence (f # x)) . n by A7, A10;
then (g . n) /. x = (h . n) . x by A8, A9, A10;
hence (g . n) /. x = (h . n) /. x by A9, A10, PARTFUN1:def_6; ::_thesis: verum
end;
hence g . n = h . n by A9, PARTFUN2:1; ::_thesis: verum
end;
hence g = h by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines superior_realsequence MESFUNC8:def_6_:_
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b3 being with_the_same_dom Functional_Sequence of X,ExtREAL holds
( b3 = superior_realsequence f iff for n being Nat holds
( dom (b3 . n) = dom (f . 0) & ( for x being Element of X st x in dom (b3 . n) holds
(b3 . n) . x = (superior_realsequence (f # x)) . n ) ) );
theorem Th7: :: MESFUNC8:7
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for x being Element of X st x in dom (f . 0) holds
(inferior_realsequence f) # x = inferior_realsequence (f # x)
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,ExtREAL
for x being Element of X st x in dom (f . 0) holds
(inferior_realsequence f) # x = inferior_realsequence (f # x)
let f be Functional_Sequence of X,ExtREAL; ::_thesis: for x being Element of X st x in dom (f . 0) holds
(inferior_realsequence f) # x = inferior_realsequence (f # x)
set F = inferior_realsequence f;
hereby ::_thesis: verum
let x be Element of X; ::_thesis: ( x in dom (f . 0) implies (inferior_realsequence f) # x = inferior_realsequence (f # x) )
assume A1: x in dom (f . 0) ; ::_thesis: (inferior_realsequence f) # x = inferior_realsequence (f # x)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((inferior_realsequence_f)_#_x)_._n_=_(inferior_realsequence_(f_#_x))_._n
let n be Element of NAT ; ::_thesis: ((inferior_realsequence f) # x) . n = (inferior_realsequence (f # x)) . n
A2: ((inferior_realsequence f) # x) . n = ((inferior_realsequence f) . n) . x by MESFUNC5:def_13;
dom ((inferior_realsequence f) . n) = dom (f . 0) by Def5;
hence ((inferior_realsequence f) # x) . n = (inferior_realsequence (f # x)) . n by A1, A2, Def5; ::_thesis: verum
end;
hence (inferior_realsequence f) # x = inferior_realsequence (f # x) by FUNCT_2:63; ::_thesis: verum
end;
end;
registration
let X, Y be set ;
let f be with_the_same_dom Functional_Sequence of X,Y;
let n be Element of NAT ;
clusterf ^\ n -> with_the_same_dom for Functional_Sequence of X,Y;
coherence
for b1 being Functional_Sequence of X,Y st b1 = f ^\ n holds
b1 is with_the_same_dom
proof
for k, l being Nat holds dom ((f ^\ n) . k) = dom ((f ^\ n) . l)
proof
reconsider g = f as Function of NAT,(PFuncs (X,Y)) ;
let k, l be Nat; ::_thesis: dom ((f ^\ n) . k) = dom ((f ^\ n) . l)
reconsider k9 = k, l9 = l as Element of NAT by ORDINAL1:def_12;
dom ((f ^\ n) . k) = dom (g . (n + k9)) by NAT_1:def_3;
then dom ((f ^\ n) . k) = dom (g . (n + l9)) by Def2;
hence dom ((f ^\ n) . k) = dom ((f ^\ n) . l) by NAT_1:def_3; ::_thesis: verum
end;
hence for b1 being Functional_Sequence of X,Y st b1 = f ^\ n holds
b1 is with_the_same_dom by Def2; ::_thesis: verum
end;
end;
theorem Th8: :: MESFUNC8:8
for X being non empty set
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for n being Element of NAT holds (inferior_realsequence f) . n = inf (f ^\ n)
proof
let X be non empty set ; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for n being Element of NAT holds (inferior_realsequence f) . n = inf (f ^\ n)
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for n being Element of NAT holds (inferior_realsequence f) . n = inf (f ^\ n)
let n be Element of NAT ; ::_thesis: (inferior_realsequence f) . n = inf (f ^\ n)
reconsider g = f as Function of NAT,(PFuncs (X,ExtREAL)) ;
dom (inf (f ^\ n)) = dom ((f ^\ n) . 0) by Def3;
then dom (inf (f ^\ n)) = dom (g . (n + 0)) by NAT_1:def_3;
then A1: dom (inf (f ^\ n)) = dom (f . 0) by Def2;
A2: dom ((inferior_realsequence f) . n) = dom (f . 0) by Def5;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(inf_(f_^\_n))_holds_
(inf_(f_^\_n))_._x_=_((inferior_realsequence_f)_._n)_._x
let x be Element of X; ::_thesis: ( x in dom (inf (f ^\ n)) implies (inf (f ^\ n)) . x = ((inferior_realsequence f) . n) . x )
assume A3: x in dom (inf (f ^\ n)) ; ::_thesis: (inf (f ^\ n)) . x = ((inferior_realsequence f) . n) . x
now__::_thesis:_for_k_being_Element_of_NAT_holds_((f_^\_n)_#_x)_._k_=_((f_#_x)_^\_n)_._k
let k be Element of NAT ; ::_thesis: ((f ^\ n) # x) . k = ((f # x) ^\ n) . k
((f ^\ n) # x) . k = ((f ^\ n) . k) . x by MESFUNC5:def_13;
then ((f ^\ n) # x) . k = (g . (n + k)) . x by NAT_1:def_3;
then ((f ^\ n) # x) . k = (f # x) . (n + k) by MESFUNC5:def_13;
hence ((f ^\ n) # x) . k = ((f # x) ^\ n) . k by NAT_1:def_3; ::_thesis: verum
end;
then (f ^\ n) # x = (f # x) ^\ n by FUNCT_2:63;
then A4: (inf (f ^\ n)) . x = inf ((f # x) ^\ n) by A3, Def3;
((inferior_realsequence f) . n) . x = (inferior_realsequence (f # x)) . n by A2, A1, A3, Def5;
hence (inf (f ^\ n)) . x = ((inferior_realsequence f) . n) . x by A4, RINFSUP2:27; ::_thesis: verum
end;
hence (inferior_realsequence f) . n = inf (f ^\ n) by A2, A1, PARTFUN1:5; ::_thesis: verum
end;
theorem Th9: :: MESFUNC8:9
for X being non empty set
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for n being Element of NAT holds (superior_realsequence f) . n = sup (f ^\ n)
proof
let X be non empty set ; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for n being Element of NAT holds (superior_realsequence f) . n = sup (f ^\ n)
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for n being Element of NAT holds (superior_realsequence f) . n = sup (f ^\ n)
let n be Element of NAT ; ::_thesis: (superior_realsequence f) . n = sup (f ^\ n)
reconsider g = f as Function of NAT,(PFuncs (X,ExtREAL)) ;
dom (sup (f ^\ n)) = dom ((f ^\ n) . 0) by Def4;
then dom (sup (f ^\ n)) = dom (g . (n + 0)) by NAT_1:def_3;
then A1: dom (sup (f ^\ n)) = dom (f . 0) by Def2;
A2: dom ((superior_realsequence f) . n) = dom (f . 0) by Def6;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(sup_(f_^\_n))_holds_
(sup_(f_^\_n))_._x_=_((superior_realsequence_f)_._n)_._x
let x be Element of X; ::_thesis: ( x in dom (sup (f ^\ n)) implies (sup (f ^\ n)) . x = ((superior_realsequence f) . n) . x )
assume A3: x in dom (sup (f ^\ n)) ; ::_thesis: (sup (f ^\ n)) . x = ((superior_realsequence f) . n) . x
now__::_thesis:_for_k_being_Element_of_NAT_holds_((f_^\_n)_#_x)_._k_=_((f_#_x)_^\_n)_._k
let k be Element of NAT ; ::_thesis: ((f ^\ n) # x) . k = ((f # x) ^\ n) . k
((f ^\ n) # x) . k = ((f ^\ n) . k) . x by MESFUNC5:def_13;
then ((f ^\ n) # x) . k = (g . (n + k)) . x by NAT_1:def_3;
then ((f ^\ n) # x) . k = (f # x) . (n + k) by MESFUNC5:def_13;
hence ((f ^\ n) # x) . k = ((f # x) ^\ n) . k by NAT_1:def_3; ::_thesis: verum
end;
then (f ^\ n) # x = (f # x) ^\ n by FUNCT_2:63;
then A4: (sup (f ^\ n)) . x = sup ((f # x) ^\ n) by A3, Def4;
((superior_realsequence f) . n) . x = (superior_realsequence (f # x)) . n by A2, A1, A3, Def6;
hence (sup (f ^\ n)) . x = ((superior_realsequence f) . n) . x by A4, RINFSUP2:27; ::_thesis: verum
end;
hence (superior_realsequence f) . n = sup (f ^\ n) by A2, A1, PARTFUN1:5; ::_thesis: verum
end;
theorem Th10: :: MESFUNC8:10
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for x being Element of X st x in dom (f . 0) holds
(superior_realsequence f) # x = superior_realsequence (f # x)
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,ExtREAL
for x being Element of X st x in dom (f . 0) holds
(superior_realsequence f) # x = superior_realsequence (f # x)
let f be Functional_Sequence of X,ExtREAL; ::_thesis: for x being Element of X st x in dom (f . 0) holds
(superior_realsequence f) # x = superior_realsequence (f # x)
let x be Element of X; ::_thesis: ( x in dom (f . 0) implies (superior_realsequence f) # x = superior_realsequence (f # x) )
set F = superior_realsequence f;
assume A1: x in dom (f . 0) ; ::_thesis: (superior_realsequence f) # x = superior_realsequence (f # x)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((superior_realsequence_f)_#_x)_._n_=_(superior_realsequence_(f_#_x))_._n
let n be Element of NAT ; ::_thesis: ((superior_realsequence f) # x) . n = (superior_realsequence (f # x)) . n
A2: ((superior_realsequence f) # x) . n = ((superior_realsequence f) . n) . x by MESFUNC5:def_13;
dom ((superior_realsequence f) . n) = dom (f . 0) by Def6;
hence ((superior_realsequence f) # x) . n = (superior_realsequence (f # x)) . n by A1, A2, Def6; ::_thesis: verum
end;
hence (superior_realsequence f) # x = superior_realsequence (f # x) by FUNCT_2:63; ::_thesis: verum
end;
definition
let X be non empty set ;
let f be Functional_Sequence of X,ExtREAL;
func lim_inf f -> PartFunc of X,ExtREAL means :Def7: :: MESFUNC8:def 7
( dom it = dom (f . 0) & ( for x being Element of X st x in dom it holds
it . x = lim_inf (f # x) ) );
existence
ex b1 being PartFunc of X,ExtREAL st
( dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds
b1 . x = lim_inf (f # x) ) )
proof
defpred S1[ set ] means $1 in dom (f . 0);
deffunc H1( Element of X) -> Element of ExtREAL = lim_inf (f # $1);
consider g being PartFunc of X,ExtREAL such that
A1: ( ( for x being Element of X holds
( x in dom g iff S1[x] ) ) & ( for x being Element of X st x in dom g holds
g /. x = H1(x) ) ) from PARTFUN2:sch_2();
take g ; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = lim_inf (f # x) ) )
A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_._x_=_lim_inf_(f_#_x)
let x be Element of X; ::_thesis: ( x in dom g implies g . x = lim_inf (f # x) )
assume A3: x in dom g ; ::_thesis: g . x = lim_inf (f # x)
then g /. x = lim_inf (f # x) by A1;
hence g . x = lim_inf (f # x) by A3, PARTFUN1:def_6; ::_thesis: verum
end;
for x being set holds
( x in dom g iff x in dom (f . 0) ) by A1;
hence ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = lim_inf (f # x) ) ) by A2, TARSKI:1; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds
b1 . x = lim_inf (f # x) ) & dom b2 = dom (f . 0) & ( for x being Element of X st x in dom b2 holds
b2 . x = lim_inf (f # x) ) holds
b1 = b2
proof
let g, h be PartFunc of X,ExtREAL; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = lim_inf (f # x) ) & dom h = dom (f . 0) & ( for x being Element of X st x in dom h holds
h . x = lim_inf (f # x) ) implies g = h )
assume that
A4: dom g = dom (f . 0) and
A5: for x being Element of X st x in dom g holds
g . x = lim_inf (f # x) and
A6: dom h = dom (f . 0) and
A7: for x being Element of X st x in dom h holds
h . x = lim_inf (f # x) ; ::_thesis: g = h
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_/._x_=_h_/._x
let x be Element of X; ::_thesis: ( x in dom g implies g /. x = h /. x )
assume A8: x in dom g ; ::_thesis: g /. x = h /. x
then g /. x = g . x by PARTFUN1:def_6;
then g /. x = lim_inf (f # x) by A5, A8;
then g /. x = h . x by A4, A6, A7, A8;
hence g /. x = h /. x by A4, A6, A8, PARTFUN1:def_6; ::_thesis: verum
end;
hence g = h by A4, A6, PARTFUN2:1; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines lim_inf MESFUNC8:def_7_:_
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b3 being PartFunc of X,ExtREAL holds
( b3 = lim_inf f iff ( dom b3 = dom (f . 0) & ( for x being Element of X st x in dom b3 holds
b3 . x = lim_inf (f # x) ) ) );
definition
let X be non empty set ;
let f be Functional_Sequence of X,ExtREAL;
func lim_sup f -> PartFunc of X,ExtREAL means :Def8: :: MESFUNC8:def 8
( dom it = dom (f . 0) & ( for x being Element of X st x in dom it holds
it . x = lim_sup (f # x) ) );
existence
ex b1 being PartFunc of X,ExtREAL st
( dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds
b1 . x = lim_sup (f # x) ) )
proof
defpred S1[ set ] means $1 in dom (f . 0);
deffunc H1( Element of X) -> Element of ExtREAL = lim_sup (f # $1);
consider g being PartFunc of X,ExtREAL such that
A1: ( ( for x being Element of X holds
( x in dom g iff S1[x] ) ) & ( for x being Element of X st x in dom g holds
g /. x = H1(x) ) ) from PARTFUN2:sch_2();
take g ; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = lim_sup (f # x) ) )
A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_._x_=_lim_sup_(f_#_x)
let x be Element of X; ::_thesis: ( x in dom g implies g . x = lim_sup (f # x) )
assume A3: x in dom g ; ::_thesis: g . x = lim_sup (f # x)
then g /. x = lim_sup (f # x) by A1;
hence g . x = lim_sup (f # x) by A3, PARTFUN1:def_6; ::_thesis: verum
end;
for x being set holds
( x in dom g iff x in dom (f . 0) ) by A1;
hence ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = lim_sup (f # x) ) ) by A2, TARSKI:1; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds
b1 . x = lim_sup (f # x) ) & dom b2 = dom (f . 0) & ( for x being Element of X st x in dom b2 holds
b2 . x = lim_sup (f # x) ) holds
b1 = b2
proof
let g, h be PartFunc of X,ExtREAL; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = lim_sup (f # x) ) & dom h = dom (f . 0) & ( for x being Element of X st x in dom h holds
h . x = lim_sup (f # x) ) implies g = h )
assume that
A4: dom g = dom (f . 0) and
A5: for x being Element of X st x in dom g holds
g . x = lim_sup (f # x) ; ::_thesis: ( not dom h = dom (f . 0) or ex x being Element of X st
( x in dom h & not h . x = lim_sup (f # x) ) or g = h )
assume that
A6: dom h = dom (f . 0) and
A7: for x being Element of X st x in dom h holds
h . x = lim_sup (f # x) ; ::_thesis: g = h
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_/._x_=_h_/._x
let x be Element of X; ::_thesis: ( x in dom g implies g /. x = h /. x )
assume A8: x in dom g ; ::_thesis: g /. x = h /. x
then g /. x = g . x by PARTFUN1:def_6;
then g /. x = lim_sup (f # x) by A5, A8;
then g /. x = h . x by A4, A6, A7, A8;
hence g /. x = h /. x by A4, A6, A8, PARTFUN1:def_6; ::_thesis: verum
end;
hence g = h by A4, A6, PARTFUN2:1; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines lim_sup MESFUNC8:def_8_:_
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b3 being PartFunc of X,ExtREAL holds
( b3 = lim_sup f iff ( dom b3 = dom (f . 0) & ( for x being Element of X st x in dom b3 holds
b3 . x = lim_sup (f # x) ) ) );
theorem Th11: :: MESFUNC8:11
for X being non empty set
for f being Functional_Sequence of X,ExtREAL holds
( ( for x being Element of X st x in dom (lim_inf f) holds
( (lim_inf f) . x = sup (inferior_realsequence (f # x)) & (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x ) ) & lim_inf f = sup (inferior_realsequence f) )
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,ExtREAL holds
( ( for x being Element of X st x in dom (lim_inf f) holds
( (lim_inf f) . x = sup (inferior_realsequence (f # x)) & (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x ) ) & lim_inf f = sup (inferior_realsequence f) )
let f be Functional_Sequence of X,ExtREAL; ::_thesis: ( ( for x being Element of X st x in dom (lim_inf f) holds
( (lim_inf f) . x = sup (inferior_realsequence (f # x)) & (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x ) ) & lim_inf f = sup (inferior_realsequence f) )
dom (sup (inferior_realsequence f)) = dom ((inferior_realsequence f) . 0) by Def4;
then dom (sup (inferior_realsequence f)) = dom (f . 0) by Def5;
then A1: dom (sup (inferior_realsequence f)) = dom (lim_inf f) by Def7;
A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_inf_f)_holds_
(_(lim_inf_f)_._x_=_sup_(inferior_realsequence_(f_#_x))_&_(lim_inf_f)_._x_=_sup_((inferior_realsequence_f)_#_x)_&_(lim_inf_f)_._x_=_(sup_(inferior_realsequence_f))_._x_)
let x be Element of X; ::_thesis: ( x in dom (lim_inf f) implies ( (lim_inf f) . x = sup (inferior_realsequence (f # x)) & (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x ) )
assume A3: x in dom (lim_inf f) ; ::_thesis: ( (lim_inf f) . x = sup (inferior_realsequence (f # x)) & (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x )
then A4: (lim_inf f) . x = lim_inf (f # x) by Def7;
hence (lim_inf f) . x = sup (inferior_realsequence (f # x)) ; ::_thesis: ( (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x )
dom (lim_inf f) = dom (f . 0) by Def7;
hence (lim_inf f) . x = sup ((inferior_realsequence f) # x) by A3, A4, Th7; ::_thesis: (lim_inf f) . x = (sup (inferior_realsequence f)) . x
hence (lim_inf f) . x = (sup (inferior_realsequence f)) . x by A1, A3, Def4; ::_thesis: verum
end;
then for x being Element of X st x in dom (lim_inf f) holds
(lim_inf f) . x = (sup (inferior_realsequence f)) . x ;
hence ( ( for x being Element of X st x in dom (lim_inf f) holds
( (lim_inf f) . x = sup (inferior_realsequence (f # x)) & (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x ) ) & lim_inf f = sup (inferior_realsequence f) ) by A1, A2, PARTFUN1:5; ::_thesis: verum
end;
theorem Th12: :: MESFUNC8:12
for X being non empty set
for f being Functional_Sequence of X,ExtREAL holds
( ( for x being Element of X st x in dom (lim_sup f) holds
( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) ) & lim_sup f = inf (superior_realsequence f) )
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,ExtREAL holds
( ( for x being Element of X st x in dom (lim_sup f) holds
( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) ) & lim_sup f = inf (superior_realsequence f) )
let f be Functional_Sequence of X,ExtREAL; ::_thesis: ( ( for x being Element of X st x in dom (lim_sup f) holds
( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) ) & lim_sup f = inf (superior_realsequence f) )
A1: dom (inf (superior_realsequence f)) = dom ((superior_realsequence f) . 0) by Def3
.= dom (f . 0) by Def6
.= dom (lim_sup f) by Def8 ;
A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_sup_f)_holds_
(_(lim_sup_f)_._x_=_inf_(superior_realsequence_(f_#_x))_&_(lim_sup_f)_._x_=_inf_((superior_realsequence_f)_#_x)_&_(lim_sup_f)_._x_=_(inf_(superior_realsequence_f))_._x_)
let x be Element of X; ::_thesis: ( x in dom (lim_sup f) implies ( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) )
assume A3: x in dom (lim_sup f) ; ::_thesis: ( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x )
then A4: (lim_sup f) . x = lim_sup (f # x) by Def8;
hence (lim_sup f) . x = inf (superior_realsequence (f # x)) ; ::_thesis: ( (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x )
dom (lim_sup f) = dom (f . 0) by Def8;
hence (lim_sup f) . x = inf ((superior_realsequence f) # x) by A3, A4, Th10; ::_thesis: (lim_sup f) . x = (inf (superior_realsequence f)) . x
hence (lim_sup f) . x = (inf (superior_realsequence f)) . x by A1, A3, Def3; ::_thesis: verum
end;
then for x being Element of X st x in dom (lim_sup f) holds
(lim_sup f) . x = (inf (superior_realsequence f)) . x ;
hence ( ( for x being Element of X st x in dom (lim_sup f) holds
( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) ) & lim_sup f = inf (superior_realsequence f) ) by A1, A2, PARTFUN1:5; ::_thesis: verum
end;
theorem :: MESFUNC8:13
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for x being Element of X st x in dom (f . 0) holds
( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x )
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,ExtREAL
for x being Element of X st x in dom (f . 0) holds
( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x )
let f be Functional_Sequence of X,ExtREAL; ::_thesis: for x being Element of X st x in dom (f . 0) holds
( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x )
let x be Element of X; ::_thesis: ( x in dom (f . 0) implies ( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x ) )
assume A1: x in dom (f . 0) ; ::_thesis: ( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x )
then x in dom (lim_inf f) by Def7;
then A2: (lim_inf f) . x = lim_inf (f # x) by Def7;
x in dom (lim_sup f) by A1, Def8;
then (lim_sup f) . x = lim_sup (f # x) by Def8;
hence ( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x ) by A2, RINFSUP2:40; ::_thesis: verum
end;
definition
let X be non empty set ;
let f be Functional_Sequence of X,ExtREAL;
func lim f -> PartFunc of X,ExtREAL means :Def9: :: MESFUNC8:def 9
( dom it = dom (f . 0) & ( for x being Element of X st x in dom it holds
it . x = lim (f # x) ) );
existence
ex b1 being PartFunc of X,ExtREAL st
( dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds
b1 . x = lim (f # x) ) )
proof
defpred S1[ set ] means $1 in dom (f . 0);
deffunc H1( Element of X) -> Element of ExtREAL = lim (f # $1);
consider g being PartFunc of X,ExtREAL such that
A1: ( ( for x being Element of X holds
( x in dom g iff S1[x] ) ) & ( for x being Element of X st x in dom g holds
g /. x = H1(x) ) ) from PARTFUN2:sch_2();
take g ; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = lim (f # x) ) )
A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_._x_=_lim_(f_#_x)
let x be Element of X; ::_thesis: ( x in dom g implies g . x = lim (f # x) )
assume A3: x in dom g ; ::_thesis: g . x = lim (f # x)
then g /. x = lim (f # x) by A1;
hence g . x = lim (f # x) by A3, PARTFUN1:def_6; ::_thesis: verum
end;
for x being set holds
( x in dom g iff x in dom (f . 0) ) by A1;
hence ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = lim (f # x) ) ) by A2, TARSKI:1; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds
b1 . x = lim (f # x) ) & dom b2 = dom (f . 0) & ( for x being Element of X st x in dom b2 holds
b2 . x = lim (f # x) ) holds
b1 = b2
proof
let g, h be PartFunc of X,ExtREAL; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = lim (f # x) ) & dom h = dom (f . 0) & ( for x being Element of X st x in dom h holds
h . x = lim (f # x) ) implies g = h )
assume that
A4: dom g = dom (f . 0) and
A5: for x being Element of X st x in dom g holds
g . x = lim (f # x) ; ::_thesis: ( not dom h = dom (f . 0) or ex x being Element of X st
( x in dom h & not h . x = lim (f # x) ) or g = h )
assume that
A6: dom h = dom (f . 0) and
A7: for x being Element of X st x in dom h holds
h . x = lim (f # x) ; ::_thesis: g = h
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_/._x_=_h_/._x
let x be Element of X; ::_thesis: ( x in dom g implies g /. x = h /. x )
assume A8: x in dom g ; ::_thesis: g /. x = h /. x
then g /. x = g . x by PARTFUN1:def_6;
then g /. x = lim (f # x) by A5, A8;
then g /. x = h . x by A4, A6, A7, A8;
hence g /. x = h /. x by A4, A6, A8, PARTFUN1:def_6; ::_thesis: verum
end;
hence g = h by A4, A6, PARTFUN2:1; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines lim MESFUNC8:def_9_:_
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b3 being PartFunc of X,ExtREAL holds
( b3 = lim f iff ( dom b3 = dom (f . 0) & ( for x being Element of X st x in dom b3 holds
b3 . x = lim (f # x) ) ) );
theorem Th14: :: MESFUNC8:14
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for x being Element of X st x in dom (lim f) & f # x is convergent holds
( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,ExtREAL
for x being Element of X st x in dom (lim f) & f # x is convergent holds
( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )
let f be Functional_Sequence of X,ExtREAL; ::_thesis: for x being Element of X st x in dom (lim f) & f # x is convergent holds
( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )
let x be Element of X; ::_thesis: ( x in dom (lim f) & f # x is convergent implies ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) )
assume that
A1: x in dom (lim f) and
A2: f # x is convergent ; ::_thesis: ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )
A3: lim (f # x) = lim_inf (f # x) by A2, RINFSUP2:41;
A4: x in dom (f . 0) by A1, Def9;
then x in dom (lim_sup f) by Def8;
then A5: (lim_sup f) . x = lim_sup (f # x) by Def8;
x in dom (lim_inf f) by A4, Def7;
then A6: (lim_inf f) . x = lim_inf (f # x) by Def7;
lim (f # x) = lim_sup (f # x) by A2, RINFSUP2:41;
hence ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) by A1, A5, A6, A3, Def9; ::_thesis: verum
end;
theorem Th15: :: MESFUNC8:15
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r)))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r)))
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r)))
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r)))
let F be SetSequence of S; ::_thesis: for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r)))
let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) implies union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) )
set E = dom (f . 0);
assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ; ::_thesis: union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r)))
now__::_thesis:_for_x_being_set_st_x_in_(dom_(f_._0))_/\_(great_dom_((sup_f),(R_EAL_r)))_holds_
x_in_union_(rng_F)
let x be set ; ::_thesis: ( x in (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) implies x in union (rng F) )
assume A2: x in (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) ; ::_thesis: x in union (rng F)
then reconsider z = x as Element of X ;
A3: x in dom (f . 0) by A2, XBOOLE_0:def_4;
x in great_dom ((sup f),(R_EAL r)) by A2, XBOOLE_0:def_4;
then A4: R_EAL r < (sup f) . z by MESFUNC1:def_13;
ex n being Element of NAT st R_EAL r < (f . n) . z
proof
assume A5: for n being Element of NAT holds (f . n) . z <= R_EAL r ; ::_thesis: contradiction
for x being ext-real number st x in rng (f # z) holds
x <= R_EAL r
proof
let x be ext-real number ; ::_thesis: ( x in rng (f # z) implies x <= R_EAL r )
assume x in rng (f # z) ; ::_thesis: x <= R_EAL r
then consider m being set such that
A6: m in NAT and
A7: x = (f # z) . m by FUNCT_2:11;
reconsider m = m as Element of NAT by A6;
x = (f . m) . z by A7, MESFUNC5:def_13;
hence x <= R_EAL r by A5; ::_thesis: verum
end;
then R_EAL r is UpperBound of rng (f # z) by XXREAL_2:def_1;
then A8: sup (f # z) <= R_EAL r by XXREAL_2:def_3;
x in dom (sup f) by A3, Def4;
hence contradiction by A4, A8, Def4; ::_thesis: verum
end;
then consider n being Element of NAT such that
A9: R_EAL r < (f . n) . z ;
x in dom (f . n) by A3, Def2;
then A10: x in great_dom ((f . n),(R_EAL r)) by A9, MESFUNC1:def_13;
A11: F . n in rng F by FUNCT_2:4;
A12: F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) by A1;
x in dom (f . 0) by A2, XBOOLE_0:def_4;
then x in F . n by A10, A12, XBOOLE_0:def_4;
hence x in union (rng F) by A11, TARSKI:def_4; ::_thesis: verum
end;
then A13: (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) c= union (rng F) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_union_(rng_F)_holds_
x_in_(dom_(f_._0))_/\_(great_dom_((sup_f),(R_EAL_r)))
let x be set ; ::_thesis: ( x in union (rng F) implies x in (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) )
assume x in union (rng F) ; ::_thesis: x in (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r)))
then consider y being set such that
A14: x in y and
A15: y in rng F by TARSKI:def_4;
reconsider z = x as Element of X by A14, A15;
consider n being set such that
A16: n in dom F and
A17: y = F . n by A15, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A16;
A18: F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) by A1;
then x in great_dom ((f . n),r) by A14, A17, XBOOLE_0:def_4;
then A19: r < (f . n) . z by MESFUNC1:def_13;
A20: (f . n) . z = (f # z) . n by MESFUNC5:def_13;
A21: x in dom (f . 0) by A14, A17, A18, XBOOLE_0:def_4;
then A22: x in dom (sup f) by Def4;
then (sup f) . z = sup (f # z) by Def4;
then (f . n) . z <= (sup f) . z by A20, RINFSUP2:23;
then R_EAL r < (sup f) . z by A19, XXREAL_0:2;
then x in great_dom ((sup f),(R_EAL r)) by A22, MESFUNC1:def_13;
hence x in (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) by A21, XBOOLE_0:def_4; ::_thesis: verum
end;
then union (rng F) c= (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) by TARSKI:def_3;
hence union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) by A13, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th16: :: MESFUNC8:16
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r)))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r)))
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r)))
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r)))
let F be SetSequence of S; ::_thesis: for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r)))
let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) implies meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) )
set E = dom (f . 0);
assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ; ::_thesis: meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r)))
now__::_thesis:_for_x_being_set_st_x_in_meet_(rng_F)_holds_
x_in_(dom_(f_._0))_/\_(great_eq_dom_((inf_f),(R_EAL_r)))
let x be set ; ::_thesis: ( x in meet (rng F) implies x in (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) )
assume A2: x in meet (rng F) ; ::_thesis: x in (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r)))
then reconsider z = x as Element of X ;
A3: F . 0 = (dom (f . 0)) /\ (great_eq_dom ((f . 0),(R_EAL r))) by A1;
F . 0 in rng F by FUNCT_2:4;
then x in F . 0 by A2, SETFAM_1:def_1;
then A4: x in dom (f . 0) by A3, XBOOLE_0:def_4;
then A5: x in dom (inf f) by Def3;
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_R_EAL_r_<=_(f_#_z)_._n
let n be Element of NAT ; ::_thesis: R_EAL r <= (f # z) . n
F . n in rng F by FUNCT_2:4;
then A7: z in F . n by A2, SETFAM_1:def_1;
F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) by A1;
then x in great_eq_dom ((f . n),(R_EAL r)) by A7, XBOOLE_0:def_4;
then R_EAL r <= (f . n) . z by MESFUNC1:def_14;
hence R_EAL r <= (f # z) . n by MESFUNC5:def_13; ::_thesis: verum
end;
now__::_thesis:_for_s_being_ext-real_number_st_s_in_rng_(f_#_z)_holds_
R_EAL_r_<=_s
let s be ext-real number ; ::_thesis: ( s in rng (f # z) implies R_EAL r <= s )
assume s in rng (f # z) ; ::_thesis: R_EAL r <= s
then ex k being set st
( k in NAT & s = (f # z) . k ) by FUNCT_2:11;
hence R_EAL r <= s by A6; ::_thesis: verum
end;
then R_EAL r is LowerBound of rng (f # z) by XXREAL_2:def_2;
then R_EAL r <= inf (f # z) by XXREAL_2:def_4;
then R_EAL r <= (inf f) . x by A5, Def3;
then x in great_eq_dom ((inf f),(R_EAL r)) by A5, MESFUNC1:def_14;
hence x in (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
then A8: meet (rng F) c= (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_(dom_(f_._0))_/\_(great_eq_dom_((inf_f),(R_EAL_r)))_holds_
x_in_meet_(rng_F)
let x be set ; ::_thesis: ( x in (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) implies x in meet (rng F) )
assume A9: x in (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) ; ::_thesis: x in meet (rng F)
then reconsider z = x as Element of X ;
A10: x in dom (f . 0) by A9, XBOOLE_0:def_4;
x in great_eq_dom ((inf f),(R_EAL r)) by A9, XBOOLE_0:def_4;
then A11: R_EAL r <= (inf f) . z by MESFUNC1:def_14;
now__::_thesis:_for_y_being_set_st_y_in_rng_F_holds_
x_in_y
let y be set ; ::_thesis: ( y in rng F implies x in y )
assume y in rng F ; ::_thesis: x in y
then consider n being set such that
A12: n in NAT and
A13: y = F . n by FUNCT_2:11;
reconsider n = n as Element of NAT by A12;
A14: x in dom (f . n) by A10, Def2;
x in dom (inf f) by A10, Def3;
then A15: (inf f) . z = inf (f # z) by Def3;
A16: x in dom (f . 0) by A9, XBOOLE_0:def_4;
(f . n) . z = (f # z) . n by MESFUNC5:def_13;
then inf (f # z) <= (f . n) . z by RINFSUP2:23;
then R_EAL r <= (f . n) . z by A11, A15, XXREAL_0:2;
then A17: x in great_eq_dom ((f . n),(R_EAL r)) by A14, MESFUNC1:def_14;
F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) by A1;
hence x in y by A13, A16, A17, XBOOLE_0:def_4; ::_thesis: verum
end;
hence x in meet (rng F) by SETFAM_1:def_1; ::_thesis: verum
end;
then (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) c= meet (rng F) by TARSKI:def_3;
hence meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) by A8, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th17: :: MESFUNC8:17
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
for n being Nat holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r)))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
for n being Nat holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r)))
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
for n being Nat holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r)))
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
for n being Nat holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r)))
let F be SetSequence of S; ::_thesis: for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
for n being Nat holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r)))
let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) implies for n being Nat holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) )
set E = dom (f . 0);
assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ; ::_thesis: for n being Nat holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r)))
let n be Nat; ::_thesis: (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r)))
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
set f1 = f ^\ n9;
set F1 = F ^\ n9;
A2: now__::_thesis:_for_k_being_Nat_holds_(F_^\_n9)_._k_=_(dom_(f_._0))_/\_(great_dom_(((f_^\_n9)_._k),(R_EAL_r)))
let k be Nat; ::_thesis: (F ^\ n9) . k = (dom (f . 0)) /\ (great_dom (((f ^\ n9) . k),(R_EAL r)))
reconsider k9 = k as Element of NAT by ORDINAL1:def_12;
(F ^\ n9) . k = F . (n + k9) by NAT_1:def_3;
then (F ^\ n9) . k = (dom (f . 0)) /\ (great_dom ((f . (n + k9)),(R_EAL r))) by A1;
hence (F ^\ n9) . k = (dom (f . 0)) /\ (great_dom (((f ^\ n9) . k),(R_EAL r))) by NAT_1:def_3; ::_thesis: verum
end;
A3: union (rng (F ^\ n9)) = (superior_setsequence F) . n by Th2;
consider g being Function of NAT,(PFuncs (X,ExtREAL)) such that
A6: f = g and
f ^\ n9 = g ^\ n9 ;
(f ^\ n9) . 0 = g . (n + 0) by A6, NAT_1:def_3;
then dom ((f ^\ n9) . 0) = dom (f . 0) by A6, Def2;
then union (rng (F ^\ n9)) = (dom (f . 0)) /\ (great_dom ((sup (f ^\ n9)),(R_EAL r))) by A2, Th15;
hence (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) by A3, Th9; ::_thesis: verum
end;
theorem Th18: :: MESFUNC8:18
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds
for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r)))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds
for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r)))
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds
for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r)))
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds
for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r)))
let F be SetSequence of S; ::_thesis: for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds
for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r)))
let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) implies for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r))) )
set E = dom (f . 0);
assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ; ::_thesis: for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r)))
let n be Nat; ::_thesis: (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r)))
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
set f1 = f ^\ n9;
set F1 = F ^\ n9;
A2: now__::_thesis:_for_k_being_Nat_holds_(F_^\_n9)_._k_=_(dom_(f_._0))_/\_(great_eq_dom_(((f_^\_n9)_._k),(R_EAL_r)))
let k be Nat; ::_thesis: (F ^\ n9) . k = (dom (f . 0)) /\ (great_eq_dom (((f ^\ n9) . k),(R_EAL r)))
reconsider k9 = k as Element of NAT by ORDINAL1:def_12;
(F ^\ n9) . k = F . (n + k9) by NAT_1:def_3;
then (F ^\ n9) . k = (dom (f . 0)) /\ (great_eq_dom ((f . (n + k9)),(R_EAL r))) by A1;
hence (F ^\ n9) . k = (dom (f . 0)) /\ (great_eq_dom (((f ^\ n9) . k),(R_EAL r))) by NAT_1:def_3; ::_thesis: verum
end;
A3: meet (rng (F ^\ n9)) = (inferior_setsequence F) . n by Th2;
consider g being Function of NAT,(PFuncs (X,ExtREAL)) such that
A6: f = g and
f ^\ n9 = g ^\ n9 ;
(f ^\ n9) . 0 = g . (n + 0) by A6, NAT_1:def_3;
then dom ((f ^\ n9) . 0) = dom (f . 0) by A6, Def2;
then meet (rng (F ^\ n9)) = (dom (f . 0)) /\ (great_eq_dom ((inf (f ^\ n9)),(R_EAL r))) by A2, Th16;
hence (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r))) by A3, Th8; ::_thesis: verum
end;
theorem Th19: :: MESFUNC8:19
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
for n being Nat holds (superior_realsequence f) . n is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
for n being Nat holds (superior_realsequence f) . n is_measurable_on E
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
for n being Nat holds (superior_realsequence f) . n is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
for n being Nat holds (superior_realsequence f) . n is_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) implies for n being Nat holds (superior_realsequence f) . n is_measurable_on E )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is_measurable_on E ; ::_thesis: for n being Nat holds (superior_realsequence f) . n is_measurable_on E
let n be Nat; ::_thesis: (superior_realsequence f) . n is_measurable_on E
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
A3: now__::_thesis:_for_r_being_real_number_holds_E_/\_(great_dom_(((superior_realsequence_f)_._n),(R_EAL_r)))_in_S
let r be real number ; ::_thesis: E /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) in S
deffunc H1( Element of NAT ) -> Element of bool X = E /\ (great_dom ((f . $1),(R_EAL r)));
consider F being Function of NAT,(bool X) such that
A4: for x being Element of NAT holds F . x = H1(x) from FUNCT_2:sch_4();
now__::_thesis:_for_i_being_Nat_holds_F_._i_in_S
let i be Nat; ::_thesis: F . i in S
A5: f . i is_measurable_on E by A2;
i in NAT by ORDINAL1:def_12;
then A6: F . i = E /\ (great_dom ((f . i),(R_EAL r))) by A4;
dom (f . i) = E by A1, Def2;
hence F . i in S by A6, A5, MESFUNC1:29; ::_thesis: verum
end;
then A7: rng F c= S by NAT_1:52;
A8: for x being Nat holds F . x = E /\ (great_dom ((f . x),(R_EAL r)))
proof
let x be Nat; ::_thesis: F . x = E /\ (great_dom ((f . x),(R_EAL r)))
reconsider x9 = x as Element of NAT by ORDINAL1:def_12;
F . x9 = E /\ (great_dom ((f . x9),(R_EAL r))) by A4;
hence F . x = E /\ (great_dom ((f . x),(R_EAL r))) ; ::_thesis: verum
end;
reconsider F = F as SetSequence of S by A7, RELAT_1:def_19;
(superior_setsequence F) . n9 in rng (superior_setsequence F) by NAT_1:51;
then (superior_setsequence F) . n9 in S ;
hence E /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) in S by A1, A8, Th17; ::_thesis: verum
end;
dom ((superior_realsequence f) . n9) = E by A1, Def6;
hence (superior_realsequence f) . n is_measurable_on E by A3, MESFUNC1:29; ::_thesis: verum
end;
theorem Th20: :: MESFUNC8:20
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
for n being Nat holds (inferior_realsequence f) . n is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
for n being Nat holds (inferior_realsequence f) . n is_measurable_on E
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
for n being Nat holds (inferior_realsequence f) . n is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
for n being Nat holds (inferior_realsequence f) . n is_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) implies for n being Nat holds (inferior_realsequence f) . n is_measurable_on E )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is_measurable_on E ; ::_thesis: for n being Nat holds (inferior_realsequence f) . n is_measurable_on E
let n be Nat; ::_thesis: (inferior_realsequence f) . n is_measurable_on E
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
A3: now__::_thesis:_for_r_being_real_number_holds_E_/\_(great_eq_dom_(((inferior_realsequence_f)_._n),(R_EAL_r)))_in_S
let r be real number ; ::_thesis: E /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r))) in S
deffunc H1( Element of NAT ) -> Element of bool X = E /\ (great_eq_dom ((f . $1),(R_EAL r)));
consider F being Function of NAT,(bool X) such that
A4: for x being Element of NAT holds F . x = H1(x) from FUNCT_2:sch_4();
now__::_thesis:_for_i_being_Nat_holds_F_._i_in_S
let i be Nat; ::_thesis: F . i in S
A5: f . i is_measurable_on E by A2;
i in NAT by ORDINAL1:def_12;
then A6: F . i = E /\ (great_eq_dom ((f . i),(R_EAL r))) by A4;
dom (f . i) = E by A1, Def2;
hence F . i in S by A6, A5, MESFUNC1:27; ::_thesis: verum
end;
then A7: rng F c= S by NAT_1:52;
A8: for x being Nat holds F . x = E /\ (great_eq_dom ((f . x),(R_EAL r)))
proof
let x be Nat; ::_thesis: F . x = E /\ (great_eq_dom ((f . x),(R_EAL r)))
reconsider x9 = x as Element of NAT by ORDINAL1:def_12;
F . x9 = E /\ (great_eq_dom ((f . x9),(R_EAL r))) by A4;
hence F . x = E /\ (great_eq_dom ((f . x),(R_EAL r))) ; ::_thesis: verum
end;
reconsider F = F as SetSequence of S by A7, RELAT_1:def_19;
(inferior_setsequence F) . n9 in rng (inferior_setsequence F) by NAT_1:51;
then (inferior_setsequence F) . n9 in S ;
hence E /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r))) in S by A1, A8, Th18; ::_thesis: verum
end;
dom ((inferior_realsequence f) . n9) = E by A1, Def5;
hence (inferior_realsequence f) . n is_measurable_on E by A3, MESFUNC1:27; ::_thesis: verum
end;
theorem Th21: :: MESFUNC8:21
for X being non empty set
for S being SigmaField of X
for f being Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) holds
meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r)))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) holds
meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r)))
let S be SigmaField of X; ::_thesis: for f being Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) holds
meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r)))
let f be Functional_Sequence of X,ExtREAL; ::_thesis: for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) holds
meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r)))
let F be SetSequence of S; ::_thesis: for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) holds
meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r)))
let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) implies meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r))) )
set E = dom (f . 0);
set g = superior_realsequence f;
assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ; ::_thesis: meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r)))
dom ((superior_realsequence f) . 0) = dom (f . 0) by Def6;
then meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf (superior_realsequence f)),(R_EAL r))) by A1, Th16;
hence meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r))) by Th12; ::_thesis: verum
end;
theorem Th22: :: MESFUNC8:22
for X being non empty set
for S being SigmaField of X
for f being Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom (((inferior_realsequence f) . n),(R_EAL r))) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r)))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom (((inferior_realsequence f) . n),(R_EAL r))) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r)))
let S be SigmaField of X; ::_thesis: for f being Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom (((inferior_realsequence f) . n),(R_EAL r))) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r)))
let f be Functional_Sequence of X,ExtREAL; ::_thesis: for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom (((inferior_realsequence f) . n),(R_EAL r))) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r)))
let F be SetSequence of S; ::_thesis: for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom (((inferior_realsequence f) . n),(R_EAL r))) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r)))
let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom (((inferior_realsequence f) . n),(R_EAL r))) ) implies union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r))) )
set E = dom (f . 0);
set g = inferior_realsequence f;
assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom (((inferior_realsequence f) . n),(R_EAL r))) ; ::_thesis: union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r)))
dom ((inferior_realsequence f) . 0) = dom (f . 0) by Def5;
then union (rng F) = (dom (f . 0)) /\ (great_dom ((sup (inferior_realsequence f)),(R_EAL r))) by A1, Th15;
hence union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r))) by Th11; ::_thesis: verum
end;
theorem Th23: :: MESFUNC8:23
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_sup f is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_sup f is_measurable_on E
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_sup f is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_sup f is_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) implies lim_sup f is_measurable_on E )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is_measurable_on E ; ::_thesis: lim_sup f is_measurable_on E
A3: now__::_thesis:_for_r_being_real_number_holds_E_/\_(great_eq_dom_((lim_sup_f),(R_EAL_r)))_in_S
let r be real number ; ::_thesis: E /\ (great_eq_dom ((lim_sup f),(R_EAL r))) in S
deffunc H1( Element of NAT ) -> Element of bool X = E /\ (great_eq_dom (((superior_realsequence f) . $1),(R_EAL r)));
consider F being Function of NAT,(bool X) such that
A4: for x being Element of NAT holds F . x = H1(x) from FUNCT_2:sch_4();
now__::_thesis:_for_i_being_Nat_holds_F_._i_in_S
let i be Nat; ::_thesis: F . i in S
A5: dom ((superior_realsequence f) . i) = dom (f . 0) by Def6;
i in NAT by ORDINAL1:def_12;
then A6: F . i = E /\ (great_eq_dom (((superior_realsequence f) . i),(R_EAL r))) by A4;
(superior_realsequence f) . i is_measurable_on E by A1, A2, Th19;
hence F . i in S by A1, A6, A5, MESFUNC1:27; ::_thesis: verum
end;
then A7: rng F c= S by NAT_1:52;
A8: for x being Nat holds F . x = E /\ (great_eq_dom (((superior_realsequence f) . x),(R_EAL r)))
proof
let x be Nat; ::_thesis: F . x = E /\ (great_eq_dom (((superior_realsequence f) . x),(R_EAL r)))
reconsider x9 = x as Element of NAT by ORDINAL1:def_12;
F . x9 = E /\ (great_eq_dom (((superior_realsequence f) . x9),(R_EAL r))) by A4;
hence F . x = E /\ (great_eq_dom (((superior_realsequence f) . x),(R_EAL r))) ; ::_thesis: verum
end;
reconsider F = F as SetSequence of S by A7, RELAT_1:def_19;
rng F c= S ;
then F is Function of NAT,S by FUNCT_2:6;
then A9: rng F is N_Sub_set_fam of X by MEASURE1:23;
A10: rng F is N_Measure_fam of S by A9, MEASURE2:def_1;
meet F = E /\ (great_eq_dom ((lim_sup f),(R_EAL r))) by A1, A8, Th21;
hence E /\ (great_eq_dom ((lim_sup f),(R_EAL r))) in S by A10, MEASURE2:2; ::_thesis: verum
end;
dom (lim_sup f) = dom (f . 0) by Def8;
hence lim_sup f is_measurable_on E by A1, A3, MESFUNC1:27; ::_thesis: verum
end;
theorem :: MESFUNC8:24
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_inf f is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_inf f is_measurable_on E
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_inf f is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_inf f is_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) implies lim_inf f is_measurable_on E )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is_measurable_on E ; ::_thesis: lim_inf f is_measurable_on E
A3: now__::_thesis:_for_r_being_real_number_holds_E_/\_(great_dom_((lim_inf_f),(R_EAL_r)))_in_S
let r be real number ; ::_thesis: E /\ (great_dom ((lim_inf f),(R_EAL r))) in S
deffunc H1( Element of NAT ) -> Element of bool X = E /\ (great_dom (((inferior_realsequence f) . $1),(R_EAL r)));
consider F being Function of NAT,(bool X) such that
A4: for x being Element of NAT holds F . x = H1(x) from FUNCT_2:sch_4();
now__::_thesis:_for_i_being_Nat_holds_F_._i_in_S
let i be Nat; ::_thesis: F . i in S
i in NAT by ORDINAL1:def_12;
then A5: F . i = E /\ (great_dom (((inferior_realsequence f) . i),(R_EAL r))) by A4;
A6: dom ((inferior_realsequence f) . i) = E by A1, Def5;
(inferior_realsequence f) . i is_measurable_on E by A1, A2, Th20;
hence F . i in S by A5, A6, MESFUNC1:29; ::_thesis: verum
end;
then A7: rng F c= S by NAT_1:52;
A8: for x being Nat holds F . x = E /\ (great_dom (((inferior_realsequence f) . x),(R_EAL r)))
proof
let x be Nat; ::_thesis: F . x = E /\ (great_dom (((inferior_realsequence f) . x),(R_EAL r)))
reconsider x9 = x as Element of NAT by ORDINAL1:def_12;
F . x9 = E /\ (great_dom (((inferior_realsequence f) . x9),(R_EAL r))) by A4;
hence F . x = E /\ (great_dom (((inferior_realsequence f) . x),(R_EAL r))) ; ::_thesis: verum
end;
reconsider F = F as SetSequence of S by A7, RELAT_1:def_19;
rng F c= S ;
then F is Function of NAT,S by FUNCT_2:6;
then A9: rng F is N_Sub_set_fam of X by MEASURE1:23;
A10: rng F is N_Measure_fam of S by A9, MEASURE2:def_1;
union (rng F) = E /\ (great_dom ((lim_inf f),(R_EAL r))) by A1, A8, Th22;
hence E /\ (great_dom ((lim_inf f),(R_EAL r))) in S by A10, MEASURE2:2; ::_thesis: verum
end;
dom (lim_inf f) = E by A1, Def7;
hence lim_inf f is_measurable_on E by A3, MESFUNC1:29; ::_thesis: verum
end;
theorem Th25: :: MESFUNC8:25
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) implies lim f is_measurable_on E )
assume A1: dom (f . 0) = E ; ::_thesis: ( ex n being Nat st not f . n is_measurable_on E or ex x being Element of X st
( x in E & not f # x is convergent ) or lim f is_measurable_on E )
then A2: dom (lim_sup f) = E by Def8;
assume that
A3: for n being Nat holds f . n is_measurable_on E and
A4: for x being Element of X st x in E holds
f # x is convergent ; ::_thesis: lim f is_measurable_on E
A5: dom (lim f) = E by A1, Def9;
A6: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_f)_holds_
(lim_f)_._x_=_(lim_sup_f)_._x
let x be Element of X; ::_thesis: ( x in dom (lim f) implies (lim f) . x = (lim_sup f) . x )
assume A7: x in dom (lim f) ; ::_thesis: (lim f) . x = (lim_sup f) . x
then f # x is convergent by A5, A4;
hence (lim f) . x = (lim_sup f) . x by A7, Th14; ::_thesis: verum
end;
lim_sup f is_measurable_on E by A1, A3, Th23;
hence lim f is_measurable_on E by A5, A2, A6, PARTFUN1:5; ::_thesis: verum
end;
theorem Th26: :: MESFUNC8:26
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for g being PartFunc of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
let g be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) implies g is_measurable_on E )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is_measurable_on E and
A3: dom g = E and
A4: for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ; ::_thesis: g is_measurable_on E
A5: dom (lim f) = E by A1, Def9;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_f)_holds_
g_._x_=_(lim_f)_._x
let x be Element of X; ::_thesis: ( x in dom (lim f) implies g . x = (lim f) . x )
assume A6: x in dom (lim f) ; ::_thesis: g . x = (lim f) . x
then g . x = lim (f # x) by A4, A5;
hence g . x = (lim f) . x by A6, Def9; ::_thesis: verum
end;
then A7: g = lim f by A3, A5, PARTFUN1:5;
for x being Element of X st x in E holds
f # x is convergent by A4;
hence g is_measurable_on E by A1, A2, A7, Th25; ::_thesis: verum
end;
theorem Th27: :: MESFUNC8:27
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL st ( for x being Element of X st x in dom g holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds
g is real-valued
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL st ( for x being Element of X st x in dom g holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds
g is real-valued
let f be Functional_Sequence of X,ExtREAL; ::_thesis: for g being PartFunc of X,ExtREAL st ( for x being Element of X st x in dom g holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds
g is real-valued
let g be PartFunc of X,ExtREAL; ::_thesis: ( ( for x being Element of X st x in dom g holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) implies g is real-valued )
assume A1: for x being Element of X st x in dom g holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ; ::_thesis: g is real-valued
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
|.(g_._x).|_<_+infty
let x be Element of X; ::_thesis: ( x in dom g implies |.(g . x).| < +infty )
assume A2: x in dom g ; ::_thesis: |.(g . x).| < +infty
then A3: ( not lim (f # x) = +infty or not f # x is convergent_to_+infty ) by A1, MESFUNC5:50;
f # x is convergent_to_finite_number by A1, A2;
then A4: f # x is convergent by MESFUNC5:def_11;
( not lim (f # x) = -infty or not f # x is convergent_to_-infty ) by A1, A2, MESFUNC5:51;
then consider g0 being real number such that
A5: lim (f # x) = g0 and
for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((f # x) . m) - (lim (f # x))).| < p and
f # x is convergent_to_finite_number by A4, A3, MESFUNC5:def_12;
g0 is Real by XREAL_0:def_1;
then |.(g . x).| = abs g0 by A1, A2, A5, EXTREAL2:1;
hence |.(g . x).| < +infty by XXREAL_0:9; ::_thesis: verum
end;
hence g is real-valued by MESFUNC2:def_1; ::_thesis: verum
end;
begin
theorem Th28: :: MESFUNC8:28
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL
for E being Element of S st M . E < +infty & dom (f . 0) = E & ( for n being Nat holds
( f . n is_measurable_on E & f . n is real-valued ) ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds
for r, e being real number st 0 < r & 0 < e holds
ex H being Element of S ex N being Nat st
( H c= E & M . H < r & ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL
for E being Element of S st M . E < +infty & dom (f . 0) = E & ( for n being Nat holds
( f . n is_measurable_on E & f . n is real-valued ) ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds
for r, e being real number st 0 < r & 0 < e holds
ex H being Element of S ex N being Nat st
( H c= E & M . H < r & ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL
for E being Element of S st M . E < +infty & dom (f . 0) = E & ( for n being Nat holds
( f . n is_measurable_on E & f . n is real-valued ) ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds
for r, e being real number st 0 < r & 0 < e holds
ex H being Element of S ex N being Nat st
( H c= E & M . H < r & ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) )
let M be sigma_Measure of S; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL
for E being Element of S st M . E < +infty & dom (f . 0) = E & ( for n being Nat holds
( f . n is_measurable_on E & f . n is real-valued ) ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds
for r, e being real number st 0 < r & 0 < e holds
ex H being Element of S ex N being Nat st
( H c= E & M . H < r & ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) )
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for g being PartFunc of X,ExtREAL
for E being Element of S st M . E < +infty & dom (f . 0) = E & ( for n being Nat holds
( f . n is_measurable_on E & f . n is real-valued ) ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds
for r, e being real number st 0 < r & 0 < e holds
ex H being Element of S ex N being Nat st
( H c= E & M . H < r & ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) )
let g be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S st M . E < +infty & dom (f . 0) = E & ( for n being Nat holds
( f . n is_measurable_on E & f . n is real-valued ) ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds
for r, e being real number st 0 < r & 0 < e holds
ex H being Element of S ex N being Nat st
( H c= E & M . H < r & ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) )
let E be Element of S; ::_thesis: ( M . E < +infty & dom (f . 0) = E & ( for n being Nat holds
( f . n is_measurable_on E & f . n is real-valued ) ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) implies for r, e being real number st 0 < r & 0 < e holds
ex H being Element of S ex N being Nat st
( H c= E & M . H < r & ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) ) )
assume that
A1: M . E < +infty and
A2: dom (f . 0) = E and
A3: for n being Nat holds
( f . n is_measurable_on E & f . n is real-valued ) and
A4: dom g = E and
A5: for x being Element of X st x in E holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ; ::_thesis: for r, e being real number st 0 < r & 0 < e holds
ex H being Element of S ex N being Nat st
( H c= E & M . H < r & ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) )
let r, e be real number ; ::_thesis: ( 0 < r & 0 < e implies ex H being Element of S ex N being Nat st
( H c= E & M . H < r & ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) ) )
defpred S1[ Element of NAT , set ] means $2 = E /\ (less_dom (|.((f . $1) - g).|,(R_EAL e)));
A6: g is real-valued by A4, A5, Th27;
for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) )
proof
let x be Element of X; ::_thesis: ( x in E implies ( f # x is convergent & g . x = lim (f # x) ) )
assume A7: x in E ; ::_thesis: ( f # x is convergent & g . x = lim (f # x) )
then f # x is convergent_to_finite_number by A5;
hence f # x is convergent by MESFUNC5:def_11; ::_thesis: g . x = lim (f # x)
thus g . x = lim (f # x) by A5, A7; ::_thesis: verum
end;
then A8: g is_measurable_on E by A2, A3, A4, Th26;
A9: for n being Element of NAT holds
( |.((f . n) - g).| is_measurable_on E & dom ((f . n) - g) = E & dom |.((f . n) - g).| = E )
proof
let n be Element of NAT ; ::_thesis: ( |.((f . n) - g).| is_measurable_on E & dom ((f . n) - g) = E & dom |.((f . n) - g).| = E )
A10: f . n is real-valued by A3;
dom ((f . n) - g) = (dom (f . n)) /\ (dom g) by A6, MESFUNC2:2;
then A11: dom ((f . n) - g) = E /\ E by A2, A4, Def2;
f . n is_measurable_on E by A3;
then (f . n) - g is_measurable_on E by A4, A8, A6, A10, MESFUNC2:11;
hence ( |.((f . n) - g).| is_measurable_on E & dom ((f . n) - g) = E & dom |.((f . n) - g).| = E ) by A11, MESFUNC1:def_10, MESFUNC2:27; ::_thesis: verum
end;
A12: for n being Element of NAT ex Z being Element of S st S1[n,Z]
proof
let n be Element of NAT ; ::_thesis: ex Z being Element of S st S1[n,Z]
|.((f . n) - g).| is_measurable_on E by A9;
then E /\ (less_dom (|.((f . n) - g).|,(R_EAL e))) in S by MESFUNC1:def_16;
hence ex Z being Element of S st S1[n,Z] ; ::_thesis: verum
end;
consider K being Function of NAT,S such that
A13: for n being Element of NAT holds S1[n,K . n] from FUNCT_2:sch_3(A12);
defpred S2[ Element of NAT , set ] means $2 = { x where x is Element of X : for k being Nat st $1 <= k holds
x in K . k } ;
A14: for n being Element of NAT ex Z being Element of S st S2[n,Z]
proof
let n be Element of NAT ; ::_thesis: ex Z being Element of S st S2[n,Z]
take { x where x is Element of X : for k being Nat st n <= k holds
x in K . k } ; ::_thesis: ( { x where x is Element of X : for k being Nat st n <= k holds
x in K . k } is Element of bool X & { x where x is Element of X : for k being Nat st n <= k holds
x in K . k } is Element of S & S2[n, { x where x is Element of X : for k being Nat st n <= k holds
x in K . k } ] )
thus ( { x where x is Element of X : for k being Nat st n <= k holds
x in K . k } is Element of bool X & { x where x is Element of X : for k being Nat st n <= k holds
x in K . k } is Element of S & S2[n, { x where x is Element of X : for k being Nat st n <= k holds
x in K . k } ] ) by Th1; ::_thesis: verum
end;
consider EN being Function of NAT,S such that
A15: for n being Element of NAT holds S2[n,EN . n] from FUNCT_2:sch_3(A14);
A16: 0. <= M . E by MEASURE1:def_2;
then reconsider ME = M . E as Real by A1, XXREAL_0:14;
defpred S3[ Element of NAT , set ] means $2 = M . (EN . $1);
A17: for n being Nat holds
( EN . n c= E & M . (EN . n) <= M . E & M . (EN . n) is Element of REAL & M . (E \ (EN . n)) = (M . E) - (M . (EN . n)) & M . (E \ (EN . n)) is Element of REAL )
proof
reconsider r1 = M . E as Real by A1, A16, XXREAL_0:14;
let n be Nat; ::_thesis: ( EN . n c= E & M . (EN . n) <= M . E & M . (EN . n) is Element of REAL & M . (E \ (EN . n)) = (M . E) - (M . (EN . n)) & M . (E \ (EN . n)) is Element of REAL )
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
thus A18: EN . n c= E ::_thesis: ( M . (EN . n) <= M . E & M . (EN . n) is Element of REAL & M . (E \ (EN . n)) = (M . E) - (M . (EN . n)) & M . (E \ (EN . n)) is Element of REAL )
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in EN . n or z in E )
assume z in EN . n ; ::_thesis: z in E
then z in { x where x is Element of X : for k being Nat st n9 <= k holds
x in K . k } by A15;
then ex x being Element of X st
( z = x & ( for k being Nat st n <= k holds
x in K . k ) ) ;
then z in K . n ;
then z in E /\ (less_dom (|.((f . n9) - g).|,(R_EAL e))) by A13;
hence z in E by XBOOLE_0:def_4; ::_thesis: verum
end;
hence A19: M . (EN . n) <= M . E by MEASURE1:31; ::_thesis: ( M . (EN . n) is Element of REAL & M . (E \ (EN . n)) = (M . E) - (M . (EN . n)) & M . (E \ (EN . n)) is Element of REAL )
A20: -infty < M . (EN . n) by MEASURE1:def_2;
then reconsider r2 = M . (EN . n) as Real by A1, A19, XXREAL_0:14;
thus M . (EN . n) is Element of REAL by A1, A19, A20, XXREAL_0:14; ::_thesis: ( M . (E \ (EN . n)) = (M . E) - (M . (EN . n)) & M . (E \ (EN . n)) is Element of REAL )
thus M . (E \ (EN . n)) = (M . E) - (M . (EN . n)) by A1, A18, A19, MEASURE1:32, XXREAL_0:4; ::_thesis: M . (E \ (EN . n)) is Element of REAL
(M . E) - (M . (EN . n)) = r1 - r2 by SUPINF_2:3;
hence M . (E \ (EN . n)) is Element of REAL by A18, MEASURE1:32, XXREAL_0:4; ::_thesis: verum
end;
A21: now__::_thesis:_for_n_being_Element_of_NAT_ex_y_being_Element_of_REAL_st_S3[n,y]
let n be Element of NAT ; ::_thesis: ex y being Element of REAL st S3[n,y]
M . (EN . n) is Element of REAL by A17;
hence ex y being Element of REAL st S3[n,y] ; ::_thesis: verum
end;
consider seq1 being Real_Sequence such that
A22: for n being Element of NAT holds S3[n,seq1 . n] from FUNCT_2:sch_3(A21);
assume A23: 0 < r ; ::_thesis: ( not 0 < e or ex H being Element of S ex N being Nat st
( H c= E & M . H < r & ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) ) )
assume A24: 0 < e ; ::_thesis: ex H being Element of S ex N being Nat st
( H c= E & M . H < r & ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) )
A25: E c= union (rng EN)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in E or z in union (rng EN) )
assume A26: z in E ; ::_thesis: z in union (rng EN)
then reconsider x = z as Element of X ;
A27: ( not lim (f # x) = +infty or not f # x is convergent_to_+infty ) by A5, A26, MESFUNC5:50;
f # x is convergent_to_finite_number by A5, A26;
then A28: f # x is convergent by MESFUNC5:def_11;
( not lim (f # x) = -infty or not f # x is convergent_to_-infty ) by A5, A26, MESFUNC5:51;
then ex g being real number st
( lim (f # x) = g & ( for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((f # x) . m) - (lim (f # x))).| < p ) & f # x is convergent_to_finite_number ) by A28, A27, MESFUNC5:def_12;
then consider n being Nat such that
A29: for m being Nat st n <= m holds
|.(((f # x) . m) - (lim (f # x))).| < e by A24;
reconsider n0 = n as Element of NAT by ORDINAL1:def_12;
A30: g . x = lim (f # x) by A5, A26;
now__::_thesis:_for_k_being_Nat_st_n0_<=_k_holds_
x_in_K_._k
let k be Nat; ::_thesis: ( n0 <= k implies x in K . k )
reconsider k9 = k as Element of NAT by ORDINAL1:def_12;
A31: dom |.((f . k9) - g).| = E by A9;
assume n0 <= k ; ::_thesis: x in K . k
then |.(((f # x) . k) - (lim (f # x))).| < e by A29;
then A32: |.(((f . k) . x) - (g . x)).| < e by A30, MESFUNC5:def_13;
dom ((f . k9) - g) = E by A9;
then |.(((f . k) - g) . x).| < e by A26, A32, MESFUNC1:def_4;
then |.((f . k) - g).| . x < e by A26, A31, MESFUNC1:def_10;
then x in less_dom (|.((f . k) - g).|,(R_EAL e)) by A26, A31, MESFUNC1:def_11;
then x in E /\ (less_dom (|.((f . k) - g).|,(R_EAL e))) by A26, XBOOLE_0:def_4;
then x in K . k9 by A13;
hence x in K . k ; ::_thesis: verum
end;
then x in { y where y is Element of X : for k being Nat st n0 <= k holds
y in K . k } ;
then A33: x in EN . n0 by A15;
EN . n0 in rng EN by FUNCT_2:4;
hence z in union (rng EN) by A33, TARSKI:def_4; ::_thesis: verum
end;
defpred S4[ Element of NAT , set ] means $2 = M . (E \ (EN . $1));
A34: dom (M * EN) = NAT by FUNCT_2:def_1;
A35: for n, m being Element of NAT st n <= m holds
( EN . n c= EN . m & M . (EN . n) <= M . (EN . m) )
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies ( EN . n c= EN . m & M . (EN . n) <= M . (EN . m) ) )
assume A36: n <= m ; ::_thesis: ( EN . n c= EN . m & M . (EN . n) <= M . (EN . m) )
thus EN . n c= EN . m ::_thesis: M . (EN . n) <= M . (EN . m)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in EN . n or z in EN . m )
assume z in EN . n ; ::_thesis: z in EN . m
then z in { x where x is Element of X : for k being Nat st n <= k holds
x in K . k } by A15;
then A37: ex x being Element of X st
( z = x & ( for k being Nat st n <= k holds
x in K . k ) ) ;
then for k being Nat st m <= k holds
z in K . k by A36, XXREAL_0:2;
then z in { y where y is Element of X : for k being Nat st m <= k holds
y in K . k } by A37;
hence z in EN . m by A15; ::_thesis: verum
end;
hence M . (EN . n) <= M . (EN . m) by MEASURE1:31; ::_thesis: verum
end;
set seq3 = NAT --> ME;
A38: for n being Nat holds (NAT --> ME) . n = ME
proof
let n be Nat; ::_thesis: (NAT --> ME) . n = ME
n in NAT by ORDINAL1:def_12;
hence (NAT --> ME) . n = ME by FUNCOP_1:7; ::_thesis: verum
end;
then A39: NAT --> ME is constant by VALUED_0:def_18;
A40: now__::_thesis:_for_x_being_set_st_x_in_dom_(M_*_EN)_holds_
(M_*_EN)_._x_=_seq1_._x
let x be set ; ::_thesis: ( x in dom (M * EN) implies (M * EN) . x = seq1 . x )
assume A41: x in dom (M * EN) ; ::_thesis: (M * EN) . x = seq1 . x
then reconsider n = x as Element of NAT ;
(M * EN) . x = M . (EN . n) by A41, FUNCT_1:12;
hence (M * EN) . x = seq1 . x by A22; ::_thesis: verum
end;
dom seq1 = NAT by FUNCT_2:def_1;
then A42: M * EN = seq1 by A34, A40, FUNCT_1:2;
now__::_thesis:_for_y_being_set_st_y_in_rng_EN_holds_
y_c=_E
let y be set ; ::_thesis: ( y in rng EN implies y c= E )
assume y in rng EN ; ::_thesis: y c= E
then consider x being set such that
A43: x in NAT and
A44: y = EN . x by FUNCT_2:11;
reconsider x9 = x as Nat by A43;
y = EN . x9 by A44;
hence y c= E by A17; ::_thesis: verum
end;
then union (rng EN) c= E by ZFMISC_1:76;
then A45: union (rng EN) = E by A25, XBOOLE_0:def_10;
A46: ( seq1 is convergent & lim seq1 = M . E )
proof
reconsider r1 = M . E as Real by A1, A16, XXREAL_0:14;
A47: for n being Element of NAT holds EN . n c= EN . (n + 1)
proof
let n be Element of NAT ; ::_thesis: EN . n c= EN . (n + 1)
n <= n + 1 by NAT_1:12;
hence EN . n c= EN . (n + 1) by A35; ::_thesis: verum
end;
A48: now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_<_r1_+_1
let n be Element of NAT ; ::_thesis: seq1 . n < r1 + 1
M . (EN . n) <= M . E by A17;
then A49: seq1 . n <= r1 by A22;
r1 + 0 < r1 + 1 by XREAL_1:8;
hence seq1 . n < r1 + 1 by A49, XXREAL_0:2; ::_thesis: verum
end;
then A50: seq1 is bounded_above by SEQ_2:def_3;
consider r being real number such that
A51: for n being Element of NAT holds seq1 . n < r by A48;
r is UpperBound of rng seq1
proof
let d be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not d in rng seq1 or d <= r )
assume d in rng seq1 ; ::_thesis: d <= r
then ex x being set st
( x in NAT & d = seq1 . x ) by FUNCT_2:11;
hence d <= r by A51; ::_thesis: verum
end;
then rng seq1 is bounded_above by XXREAL_2:def_10;
then A52: sup (rng (M * EN)) = upper_bound (rng seq1) by A42, RINFSUP2:1;
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_
seq1_._n_<=_seq1_._m
let n, m be Element of NAT ; ::_thesis: ( n <= m implies seq1 . n <= seq1 . m )
assume A53: n <= m ; ::_thesis: seq1 . n <= seq1 . m
A54: seq1 . m = M . (EN . m) by A22;
seq1 . n = M . (EN . n) by A22;
hence seq1 . n <= seq1 . m by A35, A53, A54; ::_thesis: verum
end;
then A55: seq1 is V53() by SEQM_3:6;
hence seq1 is convergent by A50; ::_thesis: lim seq1 = M . E
lim seq1 = upper_bound seq1 by A55, A50, RINFSUP1:24;
hence lim seq1 = M . E by A45, A52, A47, MEASURE2:23; ::_thesis: verum
end;
A56: now__::_thesis:_for_n_being_Element_of_NAT_ex_y_being_Element_of_REAL_st_S4[n,y]
let n be Element of NAT ; ::_thesis: ex y being Element of REAL st S4[n,y]
M . (E \ (EN . n)) is Element of REAL by A17;
hence ex y being Element of REAL st S4[n,y] ; ::_thesis: verum
end;
consider seq2 being Real_Sequence such that
A57: for n being Element of NAT holds S4[n,seq2 . n] from FUNCT_2:sch_3(A56);
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq2_._n_=_((NAT_-->_ME)_._n)_+_((-_seq1)_._n)
let n be Element of NAT ; ::_thesis: seq2 . n = ((NAT --> ME) . n) + ((- seq1) . n)
seq2 . n = M . (E \ (EN . n)) by A57;
then A58: seq2 . n = (M . E) - (M . (EN . n)) by A17;
M . (EN . n) = seq1 . n by A22;
then seq2 . n = ME - (seq1 . n) by A58, SUPINF_2:3;
then seq2 . n = ((NAT --> ME) . n) - (seq1 . n) by A38;
hence seq2 . n = ((NAT --> ME) . n) + ((- seq1) . n) by SEQ_1:10; ::_thesis: verum
end;
then A59: seq2 = (NAT --> ME) - seq1 by SEQ_1:7;
then A60: seq2 is convergent by A46, A39, SEQ_2:11;
A61: (NAT --> ME) . 0 = ME by A38;
lim seq2 = (lim (NAT --> ME)) - (lim seq1) by A46, A59, A39, SEQ_2:12;
then lim seq2 = ME - ME by A46, A39, A61, SEQ_4:25;
then consider N being Element of NAT such that
A62: for m being Element of NAT st N <= m holds
abs ((seq2 . m) - 0) < r by A23, A60, SEQ_2:def_7;
reconsider H = E \ (EN . N) as Element of S ;
A63: E \ H = E /\ (EN . N) by XBOOLE_1:48;
EN . N c= E by A17;
then A64: E \ H = EN . N by A63, XBOOLE_1:28;
A65: for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e
proof
let k be Nat; ::_thesis: ( N < k implies for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e )
reconsider k9 = k as Element of NAT by ORDINAL1:def_12;
assume A66: N < k ; ::_thesis: for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e
let x be Element of X; ::_thesis: ( x in E \ H implies |.(((f . k) . x) - (g . x)).| < e )
assume x in E \ H ; ::_thesis: |.(((f . k) . x) - (g . x)).| < e
then x in { y where y is Element of X : for k being Nat st N <= k holds
y in K . k } by A15, A64;
then ex y being Element of X st
( x = y & ( for k being Nat st N <= k holds
y in K . k ) ) ;
then x in K . k by A66;
then A67: x in E /\ (less_dom (|.((f . k9) - g).|,(R_EAL e))) by A13;
then A68: x in E by XBOOLE_0:def_4;
x in less_dom (|.((f . k) - g).|,(R_EAL e)) by A67, XBOOLE_0:def_4;
then A69: |.((f . k) - g).| . x < R_EAL e by MESFUNC1:def_11;
A70: dom ((f . k9) - g) = E by A9;
dom |.((f . k9) - g).| = E by A9;
then |.(((f . k) - g) . x).| < e by A68, A69, MESFUNC1:def_10;
hence |.(((f . k) . x) - (g . x)).| < e by A68, A70, MESFUNC1:def_4; ::_thesis: verum
end;
take H ; ::_thesis: ex N being Nat st
( H c= E & M . H < r & ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) )
take N ; ::_thesis: ( H c= E & M . H < r & ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) )
M . (E \ (EN . N)) = seq2 . N by A57;
then A71: 0 <= seq2 . N by MEASURE1:def_2;
abs ((seq2 . N) - 0) < r by A62;
then seq2 . N < r by A71, ABSVALUE:def_1;
hence ( H c= E & M . H < r & ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) ) by A57, A65, XBOOLE_1:36; ::_thesis: verum
end;
theorem :: MESFUNC8:29
for X, Y being non empty set
for E being set
for F, G being Function of X,Y st ( for x being Element of X holds G . x = E \ (F . x) ) holds
union (rng G) = E \ (meet (rng F))
proof
let X, Y be non empty set ; ::_thesis: for E being set
for F, G being Function of X,Y st ( for x being Element of X holds G . x = E \ (F . x) ) holds
union (rng G) = E \ (meet (rng F))
let E be set ; ::_thesis: for F, G being Function of X,Y st ( for x being Element of X holds G . x = E \ (F . x) ) holds
union (rng G) = E \ (meet (rng F))
let F, G be Function of X,Y; ::_thesis: ( ( for x being Element of X holds G . x = E \ (F . x) ) implies union (rng G) = E \ (meet (rng F)) )
assume A1: for x being Element of X holds G . x = E \ (F . x) ; ::_thesis: union (rng G) = E \ (meet (rng F))
A2: dom G = X by FUNCT_2:def_1;
now__::_thesis:_for_Z_being_set_st_Z_in_DIFFERENCE_({E},(rng_F))_holds_
Z_in_rng_G
let Z be set ; ::_thesis: ( Z in DIFFERENCE ({E},(rng F)) implies Z in rng G )
assume Z in DIFFERENCE ({E},(rng F)) ; ::_thesis: Z in rng G
then consider X1, Y being set such that
A3: X1 in {E} and
A4: Y in rng F and
A5: Z = X1 \ Y by SETFAM_1:def_6;
consider x being set such that
A6: x in dom F and
A7: Y = F . x by A4, FUNCT_1:def_3;
reconsider x = x as Element of X by A6;
X1 = E by A3, TARSKI:def_1;
then Z = G . x by A1, A5, A7;
hence Z in rng G by A2, FUNCT_1:3; ::_thesis: verum
end;
then A8: DIFFERENCE ({E},(rng F)) c= rng G by TARSKI:def_3;
A9: dom F = X by FUNCT_2:def_1;
now__::_thesis:_for_Z_being_set_st_Z_in_rng_G_holds_
Z_in_DIFFERENCE_({E},(rng_F))
let Z be set ; ::_thesis: ( Z in rng G implies Z in DIFFERENCE ({E},(rng F)) )
A10: E in {E} by TARSKI:def_1;
assume Z in rng G ; ::_thesis: Z in DIFFERENCE ({E},(rng F))
then consider x being set such that
A11: x in dom G and
A12: Z = G . x by FUNCT_1:def_3;
reconsider x = x as Element of X by A11;
A13: F . x in rng F by A9, FUNCT_1:3;
Z = E \ (F . x) by A1, A12;
hence Z in DIFFERENCE ({E},(rng F)) by A13, A10, SETFAM_1:def_6; ::_thesis: verum
end;
then rng G c= DIFFERENCE ({E},(rng F)) by TARSKI:def_3;
then DIFFERENCE ({E},(rng F)) = rng G by A8, XBOOLE_0:def_10;
hence union (rng G) = E \ (meet (rng F)) by SETFAM_1:27; ::_thesis: verum
end;
theorem :: MESFUNC8:30
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & M . E < +infty & ( for n being Nat ex L being Element of S st
( L c= E & M . (E \ L) = 0 & ( for x being Element of X st x in L holds
|.((f . n) . x).| < +infty ) ) ) & ex G being Element of S st
( G c= E & M . (E \ G) = 0 & ( for x being Element of X st x in E holds
f # x is convergent_to_finite_number ) & dom g = E & ( for x being Element of X st x in G holds
g . x = lim (f # x) ) ) holds
for e being real number st 0 < e holds
ex F being Element of S st
( F c= E & M . (E \ F) <= e & ( for p being real number st 0 < p holds
ex N being Nat st
for n being Nat st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < p ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & M . E < +infty & ( for n being Nat ex L being Element of S st
( L c= E & M . (E \ L) = 0 & ( for x being Element of X st x in L holds
|.((f . n) . x).| < +infty ) ) ) & ex G being Element of S st
( G c= E & M . (E \ G) = 0 & ( for x being Element of X st x in E holds
f # x is convergent_to_finite_number ) & dom g = E & ( for x being Element of X st x in G holds
g . x = lim (f # x) ) ) holds
for e being real number st 0 < e holds
ex F being Element of S st
( F c= E & M . (E \ F) <= e & ( for p being real number st 0 < p holds
ex N being Nat st
for n being Nat st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < p ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & M . E < +infty & ( for n being Nat ex L being Element of S st
( L c= E & M . (E \ L) = 0 & ( for x being Element of X st x in L holds
|.((f . n) . x).| < +infty ) ) ) & ex G being Element of S st
( G c= E & M . (E \ G) = 0 & ( for x being Element of X st x in E holds
f # x is convergent_to_finite_number ) & dom g = E & ( for x being Element of X st x in G holds
g . x = lim (f # x) ) ) holds
for e being real number st 0 < e holds
ex F being Element of S st
( F c= E & M . (E \ F) <= e & ( for p being real number st 0 < p holds
ex N being Nat st
for n being Nat st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < p ) )
let M be sigma_Measure of S; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & M . E < +infty & ( for n being Nat ex L being Element of S st
( L c= E & M . (E \ L) = 0 & ( for x being Element of X st x in L holds
|.((f . n) . x).| < +infty ) ) ) & ex G being Element of S st
( G c= E & M . (E \ G) = 0 & ( for x being Element of X st x in E holds
f # x is convergent_to_finite_number ) & dom g = E & ( for x being Element of X st x in G holds
g . x = lim (f # x) ) ) holds
for e being real number st 0 < e holds
ex F being Element of S st
( F c= E & M . (E \ F) <= e & ( for p being real number st 0 < p holds
ex N being Nat st
for n being Nat st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < p ) )
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for g being PartFunc of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & M . E < +infty & ( for n being Nat ex L being Element of S st
( L c= E & M . (E \ L) = 0 & ( for x being Element of X st x in L holds
|.((f . n) . x).| < +infty ) ) ) & ex G being Element of S st
( G c= E & M . (E \ G) = 0 & ( for x being Element of X st x in E holds
f # x is convergent_to_finite_number ) & dom g = E & ( for x being Element of X st x in G holds
g . x = lim (f # x) ) ) holds
for e being real number st 0 < e holds
ex F being Element of S st
( F c= E & M . (E \ F) <= e & ( for p being real number st 0 < p holds
ex N being Nat st
for n being Nat st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < p ) )
let g be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & M . E < +infty & ( for n being Nat ex L being Element of S st
( L c= E & M . (E \ L) = 0 & ( for x being Element of X st x in L holds
|.((f . n) . x).| < +infty ) ) ) & ex G being Element of S st
( G c= E & M . (E \ G) = 0 & ( for x being Element of X st x in E holds
f # x is convergent_to_finite_number ) & dom g = E & ( for x being Element of X st x in G holds
g . x = lim (f # x) ) ) holds
for e being real number st 0 < e holds
ex F being Element of S st
( F c= E & M . (E \ F) <= e & ( for p being real number st 0 < p holds
ex N being Nat st
for n being Nat st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < p ) )
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & M . E < +infty & ( for n being Nat ex L being Element of S st
( L c= E & M . (E \ L) = 0 & ( for x being Element of X st x in L holds
|.((f . n) . x).| < +infty ) ) ) & ex G being Element of S st
( G c= E & M . (E \ G) = 0 & ( for x being Element of X st x in E holds
f # x is convergent_to_finite_number ) & dom g = E & ( for x being Element of X st x in G holds
g . x = lim (f # x) ) ) implies for e being real number st 0 < e holds
ex F being Element of S st
( F c= E & M . (E \ F) <= e & ( for p being real number st 0 < p holds
ex N being Nat st
for n being Nat st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < p ) ) )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is_measurable_on E and
A3: M . E < +infty and
A4: for n being Nat ex L being Element of S st
( L c= E & M . (E \ L) = 0 & ( for x being Element of X st x in L holds
|.((f . n) . x).| < +infty ) ) and
A5: ex G being Element of S st
( G c= E & M . (E \ G) = 0 & ( for x being Element of X st x in E holds
f # x is convergent_to_finite_number ) & dom g = E & ( for x being Element of X st x in G holds
g . x = lim (f # x) ) ) ; ::_thesis: for e being real number st 0 < e holds
ex F being Element of S st
( F c= E & M . (E \ F) <= e & ( for p being real number st 0 < p holds
ex N being Nat st
for n being Nat st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < p ) )
defpred S1[ Element of NAT , set ] means ( $2 c= E & M . (E \ $2) = 0 & ( for x being Element of X st x in $2 holds
|.((f . $1) . x).| < +infty ) );
A6: for n being Element of NAT ex Z being Element of S st S1[n,Z] by A4;
consider LN being Function of NAT,S such that
A7: for n being Element of NAT holds S1[n,LN . n] from FUNCT_2:sch_3(A6);
rng LN is N_Sub_set_fam of X by MEASURE1:23;
then rng LN is N_Measure_fam of S by MEASURE2:def_1;
then reconsider MRLN = meet (rng LN) as Element of S by MEASURE2:2;
let e0 be real number ; ::_thesis: ( 0 < e0 implies ex F being Element of S st
( F c= E & M . (E \ F) <= e0 & ( for p being real number st 0 < p holds
ex N being Nat st
for n being Nat st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < p ) ) )
assume A8: 0 < e0 ; ::_thesis: ex F being Element of S st
( F c= E & M . (E \ F) <= e0 & ( for p being real number st 0 < p holds
ex N being Nat st
for n being Nat st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < p ) )
set e = e0 / 2;
consider G being Element of S such that
A9: G c= E and
A10: M . (E \ G) = 0 and
A11: for x being Element of X st x in E holds
f # x is convergent_to_finite_number and
A12: dom g = E and
A13: for x being Element of X st x in G holds
g . x = lim (f # x) by A5;
MRLN /\ G is Element of S ;
then reconsider L = (meet (rng LN)) /\ G as Element of S ;
set gL = g | L;
A14: L c= G by XBOOLE_1:17;
then M . L <= M . E by A9, MEASURE1:31, XBOOLE_1:1;
then A15: M . L < +infty by A3, XXREAL_0:2;
dom (g | L) = (dom g) /\ L by RELAT_1:61;
then A16: dom (g | L) = L by A9, A12, A14, XBOOLE_1:1, XBOOLE_1:28;
deffunc H1( Nat) -> Element of bool [:X,ExtREAL:] = (f . $1) | L;
consider fL being Functional_Sequence of X,ExtREAL such that
A17: for n being Nat holds fL . n = H1(n) from SEQFUNC:sch_1();
for n, m being Nat holds dom (fL . n) = dom (fL . m)
proof
let n, m be Nat; ::_thesis: dom (fL . n) = dom (fL . m)
fL . m = (f . m) | L by A17;
then A18: dom (fL . m) = (dom (f . m)) /\ L by RELAT_1:61;
fL . n = (f . n) | L by A17;
then dom (fL . n) = (dom (f . n)) /\ L by RELAT_1:61;
hence dom (fL . n) = dom (fL . m) by A18, Def2; ::_thesis: verum
end;
then reconsider fL = fL as with_the_same_dom Functional_Sequence of X,ExtREAL by Def2;
A19: L c= E by A9, A14, XBOOLE_1:1;
A20: for x being Element of X st x in L holds
( fL # x is convergent_to_finite_number & (g | L) . x = lim (fL # x) )
proof
let x be Element of X; ::_thesis: ( x in L implies ( fL # x is convergent_to_finite_number & (g | L) . x = lim (fL # x) ) )
A21: dom (fL # x) = NAT by FUNCT_2:def_1;
A22: dom (f # x) = NAT by FUNCT_2:def_1;
assume A23: x in L ; ::_thesis: ( fL # x is convergent_to_finite_number & (g | L) . x = lim (fL # x) )
A24: for y being set st y in NAT holds
(fL # x) . y = (f # x) . y
proof
let y be set ; ::_thesis: ( y in NAT implies (fL # x) . y = (f # x) . y )
assume y in NAT ; ::_thesis: (fL # x) . y = (f # x) . y
then reconsider n = y as Element of NAT ;
((f . n) | L) . x = (f . n) . x by A23, FUNCT_1:49;
then A25: (fL . n) . x = (f . n) . x by A17;
(f . n) . x = (f # x) . n by MESFUNC5:def_13;
hence (fL # x) . y = (f # x) . y by A25, MESFUNC5:def_13; ::_thesis: verum
end;
then A26: fL # x = f # x by FUNCT_2:12;
f # x is convergent_to_finite_number by A11, A19, A23;
hence fL # x is convergent_to_finite_number by A21, A22, A24, FUNCT_1:2; ::_thesis: (g | L) . x = lim (fL # x)
L c= G by XBOOLE_1:17;
then g . x = lim (f # x) by A13, A23;
hence (g | L) . x = lim (fL # x) by A23, A26, FUNCT_1:49; ::_thesis: verum
end;
defpred S2[ Element of NAT , set ] means ( $2 c= L & M . $2 < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . $1 & ex Np being Element of NAT st
for k being Element of NAT st Np < k holds
for x being Element of X st x in L \ $2 holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq) . $1 );
A27: for n being Nat holds
( dom (fL . n) = L & fL . n is_measurable_on L & fL . n is real-valued )
proof
let n be Nat; ::_thesis: ( dom (fL . n) = L & fL . n is_measurable_on L & fL . n is real-valued )
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
A28: fL . n = (f . n) | L by A17;
then A29: dom (fL . n) = (dom (f . n)) /\ L by RELAT_1:61;
then dom (fL . n9) = E /\ L by A1, Def2;
hence A30: dom (fL . n) = L by A9, A14, XBOOLE_1:1, XBOOLE_1:28; ::_thesis: ( fL . n is_measurable_on L & fL . n is real-valued )
f . n is_measurable_on L by A2, A19, MESFUNC1:30;
hence fL . n is_measurable_on L by A28, A29, A30, MESFUNC5:42; ::_thesis: fL . n is real-valued
for x being Element of X st x in dom (fL . n) holds
|.((fL . n) . x).| < +infty
proof
let x be Element of X; ::_thesis: ( x in dom (fL . n) implies |.((fL . n) . x).| < +infty )
dom LN = NAT by FUNCT_2:def_1;
then A31: LN . n9 in rng LN by FUNCT_1:3;
assume A32: x in dom (fL . n) ; ::_thesis: |.((fL . n) . x).| < +infty
then x in meet (rng LN) by A30, XBOOLE_0:def_4;
then x in LN . n by A31, SETFAM_1:def_1;
then |.((f . n9) . x).| < +infty by A7;
hence |.((fL . n) . x).| < +infty by A28, A32, FUNCT_1:47; ::_thesis: verum
end;
hence fL . n is real-valued by MESFUNC2:def_1; ::_thesis: verum
end;
then A33: dom (fL . 0) = L ;
A34: for p being Nat ex Hp being Element of S ex Np being Nat st
( Hp c= L & M . Hp < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p & ( for k being Nat st Np < k holds
for x being Element of X st x in L \ Hp holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq) . p ) )
proof
let p be Nat; ::_thesis: ex Hp being Element of S ex Np being Nat st
( Hp c= L & M . Hp < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p & ( for k being Nat st Np < k holds
for x being Element of X st x in L \ Hp holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq) . p ) )
reconsider p9 = p as Element of NAT by ORDINAL1:def_12;
A35: ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p = (e0 / 2) * (((1 / 2) GeoSeq) . p9) by SEQ_1:9;
0 < (1 / 2) |^ p by PREPOWER:6;
then A36: 0 < ((1 / 2) GeoSeq) . p9 by PREPOWER:def_1;
0 < (1 / 2) |^ p by PREPOWER:6;
then A37: 0 < ((1 / 2) GeoSeq) . p9 by PREPOWER:def_1;
0 < e0 / 2 by A8, XREAL_1:139;
then 0 < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p by A36, A35, XREAL_1:129;
hence ex Hp being Element of S ex Np being Nat st
( Hp c= L & M . Hp < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p & ( for k being Nat st Np < k holds
for x being Element of X st x in L \ Hp holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq) . p ) ) by A15, A27, A33, A16, A20, A37, Th28; ::_thesis: verum
end;
A38: for n being Element of NAT ex Z being Element of S st S2[n,Z]
proof
let n be Element of NAT ; ::_thesis: ex Z being Element of S st S2[n,Z]
reconsider n9 = n as Nat ;
consider Z being Element of S, Np being Nat such that
A39: Z c= L and
A40: M . Z < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . n9 and
A41: for k being Nat st Np < k holds
for x being Element of X st x in L \ Z holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq) . n9 by A34;
reconsider Np9 = Np as Element of NAT by ORDINAL1:def_12;
for k being Element of NAT st Np9 < k holds
for x being Element of X st x in L \ Z holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq) . n9 by A41;
hence ex Z being Element of S st S2[n,Z] by A39, A40; ::_thesis: verum
end;
consider HP being Function of NAT,S such that
A42: for p being Element of NAT holds S2[p,HP . p] from FUNCT_2:sch_3(A38);
defpred S3[ Element of NAT , set ] means $2 = M . (HP . $1);
A43: for n being Element of NAT ex y being Element of REAL st S3[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of REAL st S3[n,y]
A44: -infty < M . (HP . n) by MEASURE1:def_2;
M . (HP . n) < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . n by A42;
then M . (HP . n) is Real by A44, XXREAL_0:48;
hence ex y being Element of REAL st S3[n,y] ; ::_thesis: verum
end;
consider me being Real_Sequence such that
A45: for p being Element of NAT holds S3[p,me . p] from FUNCT_2:sch_3(A43);
A46: for p being Element of NAT holds me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p
proof
let p be Element of NAT ; ::_thesis: me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p
me . p = M . (HP . p) by A45;
hence me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p by A42; ::_thesis: verum
end;
A47: for p being Element of NAT holds
( 0 <= me . p & me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p )
proof
let p be Element of NAT ; ::_thesis: ( 0 <= me . p & me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p )
0. <= M . (HP . p) by MEASURE1:def_2;
hence ( 0 <= me . p & me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p ) by A45, A46; ::_thesis: verum
end;
then A48: me is nonnegative by RINFSUP1:def_3;
deffunc H2( Element of NAT ) -> M11(X,S) = E \ (LN . $1);
consider ELN being Function of NAT,S such that
A49: for n being Element of NAT holds ELN . n = H2(n) from FUNCT_2:sch_4();
rng ELN is N_Sub_set_fam of X by MEASURE1:23;
then reconsider RELN = rng ELN as N_Measure_fam of S by MEASURE2:def_1;
A50: E /\ (union (rng HP)) c= union (rng HP) by XBOOLE_1:17;
for A being set st A in RELN holds
A is measure_zero of M
proof
let A be set ; ::_thesis: ( A in RELN implies A is measure_zero of M )
assume A in RELN ; ::_thesis: A is measure_zero of M
then consider n being set such that
A51: n in NAT and
A52: A = ELN . n by FUNCT_2:11;
reconsider n = n as Element of NAT by A51;
M . (ELN . n) = M . (E \ (LN . n)) by A49
.= 0 by A7 ;
hence A is measure_zero of M by A52, MEASURE1:def_7; ::_thesis: verum
end;
then union RELN is measure_zero of M by MEASURE2:14;
then A53: M . (union RELN) = 0. by MEASURE1:def_7;
now__::_thesis:_for_x_being_set_st_x_in_E_\_(meet_(rng_LN))_holds_
x_in_union_RELN
let x be set ; ::_thesis: ( x in E \ (meet (rng LN)) implies x in union RELN )
assume A54: x in E \ (meet (rng LN)) ; ::_thesis: x in union RELN
then A55: x in E by XBOOLE_0:def_5;
not x in meet (rng LN) by A54, XBOOLE_0:def_5;
then consider Y being set such that
A56: Y in rng LN and
A57: not x in Y by SETFAM_1:def_1;
consider m being set such that
A58: m in dom LN and
A59: Y = LN . m by A56, FUNCT_1:def_3;
reconsider m = m as Element of NAT by A58;
dom ELN = NAT by FUNCT_2:def_1;
then A60: ELN . m in rng ELN by FUNCT_1:3;
ELN . m = E \ (LN . m) by A49;
then x in ELN . m by A55, A57, A59, XBOOLE_0:def_5;
hence x in union RELN by A60, TARSKI:def_4; ::_thesis: verum
end;
then A61: E \ (meet (rng LN)) c= union RELN by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_union_RELN_holds_
x_in_E_\_(meet_(rng_LN))
let x be set ; ::_thesis: ( x in union RELN implies x in E \ (meet (rng LN)) )
assume x in union RELN ; ::_thesis: x in E \ (meet (rng LN))
then consider Y being set such that
A62: x in Y and
A63: Y in RELN by TARSKI:def_4;
consider m being set such that
A64: m in dom ELN and
A65: ELN . m = Y by A63, FUNCT_1:def_3;
reconsider m = m as Element of NAT by A64;
dom LN = NAT by FUNCT_2:def_1;
then A66: LN . m in rng LN by FUNCT_1:3;
A67: Y = E \ (LN . m) by A49, A65;
then not x in LN . m by A62, XBOOLE_0:def_5;
then A68: not x in meet (rng LN) by A66, SETFAM_1:def_1;
x in E by A62, A67, XBOOLE_0:def_5;
hence x in E \ (meet (rng LN)) by A68, XBOOLE_0:def_5; ::_thesis: verum
end;
then union RELN c= E \ (meet (rng LN)) by TARSKI:def_3;
then A69: union RELN = E \ (meet (rng LN)) by A61, XBOOLE_0:def_10;
rng HP is N_Sub_set_fam of X by MEASURE1:23;
then A70: rng HP is N_Measure_fam of S by MEASURE2:def_1;
reconsider MRHP = union (rng HP) as Element of S by MEASURE1:24;
L \ MRHP is Element of S ;
then consider F being Element of S such that
A71: F = L \ (union (rng HP)) ;
E \ L = (E \ (meet (rng LN))) \/ (E \ G) by XBOOLE_1:54;
then M . (E \ L) <= (M . (union RELN)) + (M . (E \ G)) by A69, MEASURE1:33;
then M . (E \ L) <= 0. by A10, A53;
then A72: M . (E \ L) = 0 by MEASURE1:def_2;
reconsider MRHP = union (rng HP) as Element of S by MEASURE1:24;
A73: M . ((E \ L) \/ MRHP) <= (M . (E \ L)) + (M . MRHP) by MEASURE1:33;
E \ F = (E \ L) \/ (E /\ (union (rng HP))) by A71, XBOOLE_1:52;
then M . (E \ F) <= M . ((E \ L) \/ MRHP) by A50, MEASURE1:31, XBOOLE_1:9;
then M . (E \ F) <= (M . (E \ L)) + (M . MRHP) by A73, XXREAL_0:2;
then A74: M . (E \ F) <= M . MRHP by A72, XXREAL_3:4;
dom me = NAT by FUNCT_2:def_1;
then A75: dom me = dom (M * HP) by FUNCT_2:def_1;
A76: for x being set st x in dom me holds
me . x = (M * HP) . x
proof
let x be set ; ::_thesis: ( x in dom me implies me . x = (M * HP) . x )
assume A77: x in dom me ; ::_thesis: me . x = (M * HP) . x
then (M * HP) . x = M . (HP . x) by A75, FUNCT_1:12;
hence me . x = (M * HP) . x by A45, A77; ::_thesis: verum
end;
A78: abs (1 / 2) = 1 / 2 by ABSVALUE:def_1;
then A79: (1 / 2) GeoSeq is summable by SERIES_1:24;
then A80: (e0 / 2) (#) ((1 / 2) GeoSeq) is summable by SERIES_1:10;
then me is summable by A47, SERIES_1:20;
then Sum me = SUM (M * HP) by A48, A75, A76, FUNCT_1:2, PROB_4:12;
then A81: M . (union (rng HP)) <= Sum me by A70, MEASURE2:11;
A82: for q being real number st 0 < q holds
ex p being Element of NAT st ((1 / 2) GeoSeq) . p < q
proof
let q be real number ; ::_thesis: ( 0 < q implies ex p being Element of NAT st ((1 / 2) GeoSeq) . p < q )
assume A83: 0 < q ; ::_thesis: ex p being Element of NAT st ((1 / 2) GeoSeq) . p < q
A84: lim ((1 / 2) GeoSeq) = 0 by A79, SERIES_1:4;
(1 / 2) GeoSeq is convergent by A79, SERIES_1:4;
then consider p being Element of NAT such that
A85: for n being Element of NAT st p <= n holds
abs ((((1 / 2) GeoSeq) . n) - 0) < q by A83, A84, SEQ_2:def_7;
take p ; ::_thesis: ((1 / 2) GeoSeq) . p < q
0 < (1 / 2) |^ p by PREPOWER:6;
then A86: 0 <= ((1 / 2) GeoSeq) . p by PREPOWER:def_1;
abs ((((1 / 2) GeoSeq) . p) - 0) < q by A85;
hence ((1 / 2) GeoSeq) . p < q by A86, ABSVALUE:def_1; ::_thesis: verum
end;
A87: for x being Element of X st x in F holds
for p being Element of NAT holds x in L \ (HP . p)
proof
let x be Element of X; ::_thesis: ( x in F implies for p being Element of NAT holds x in L \ (HP . p) )
assume A88: x in F ; ::_thesis: for p being Element of NAT holds x in L \ (HP . p)
let p be Element of NAT ; ::_thesis: x in L \ (HP . p)
dom HP = NAT by FUNCT_2:def_1;
then HP . p in rng HP by FUNCT_1:3;
then L \ (union (rng HP)) c= L \ (HP . p) by XBOOLE_1:34, ZFMISC_1:74;
hence x in L \ (HP . p) by A71, A88; ::_thesis: verum
end;
A89: for q being real number st 0 < q holds
ex N being Nat st
for n being Nat st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < q
proof
let q be real number ; ::_thesis: ( 0 < q implies ex N being Nat st
for n being Nat st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < q )
assume 0 < q ; ::_thesis: ex N being Nat st
for n being Nat st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < q
then consider p being Element of NAT such that
A90: ((1 / 2) GeoSeq) . p < q by A82;
consider Np being Element of NAT such that
A91: for k being Element of NAT st Np < k holds
for x being Element of X st x in L \ (HP . p) holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq) . p by A42;
take Np ; ::_thesis: for n being Nat st Np < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < q
hereby ::_thesis: verum
let n be Nat; ::_thesis: ( Np < n implies for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < q )
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
assume A92: Np < n ; ::_thesis: for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < q
hereby ::_thesis: verum
let x be Element of X; ::_thesis: ( x in F implies |.(((f . n) . x) - (g . x)).| < q )
A93: fL . n = (f . n) | L by A17;
assume A94: x in F ; ::_thesis: |.(((f . n) . x) - (g . x)).| < q
then |.(((fL . n9) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq) . p by A87, A91, A92;
then A95: |.(((fL . n) . x) - ((g | L) . x)).| < q by A90, XXREAL_0:2;
A96: F c= L by A71, XBOOLE_1:36;
then (g | L) . x = g . x by A94, FUNCT_1:49;
hence |.(((f . n) . x) - (g . x)).| < q by A94, A95, A93, A96, FUNCT_1:49; ::_thesis: verum
end;
end;
end;
Sum ((1 / 2) GeoSeq) = 1 / (1 - (1 / 2)) by A78, SERIES_1:24;
then A97: Sum ((e0 / 2) (#) ((1 / 2) GeoSeq)) = (e0 / 2) * 2 by A79, SERIES_1:10;
Sum me <= Sum ((e0 / 2) (#) ((1 / 2) GeoSeq)) by A80, A47, SERIES_1:20;
then M . MRHP <= 2 * (e0 / 2) by A81, A97, XXREAL_0:2;
then A98: M . (E \ F) <= e0 by A74, XXREAL_0:2;
F c= L by A71, XBOOLE_1:36;
hence ex F being Element of S st
( F c= E & M . (E \ F) <= e0 & ( for p being real number st 0 < p holds
ex N being Nat st
for n being Nat st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < p ) ) by A19, A98, A89, XBOOLE_1:1; ::_thesis: verum
end;