:: Egoroff's Theorem :: by Noboru Endou , Yasunari Shidama and Keiko Narita :: :: Received October 30, 2007 :: Copyright (c) 2007 Association of Mizar Users environ vocabularies PARTFUN1, MEASURE1, MEASURE2, RELAT_1, ABSVALUE, FUNCT_1, FUNCT_2, ORDINAL2, FINSEQ_4, COMPLEX1, SEQ_1, SEQ_2, SEQM_3, PREPOWER, MEASURE6, BOOLE, ARYTM, ARYTM_1, SETFAM_1, MESFUNC1, TARSKI, ARYTM_3, RLVECT_1, GROUP_1, PROB_1, SEQFUNC, TDGROUP, MESFUNC5, SUPINF_1, SUPINF_2, SETLIM_1, RINFSUP1, MESFUNC8, FINSET_1, PRALG_2; notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, XXREAL_0, SUPINF_1, PROB_1, REAL_1, SETFAM_1, MEASURE1, KURATO_2, SETLIM_1, MEASURE2, MEASURE6, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, RFUNCT_3, FUNCT_2, SUPINF_2, RINFSUP1, SEQFUNC, PSCOMP_1, VALUED_1, NAT_1, SEQ_1, SEQ_4, SEQ_2, SEQM_3, NEWTON, PREPOWER, SERIES_1, EXTREAL1, MESFUNC1, MESFUNC2, MESFUNC5, RINFSUP2, CARD_3; constructors REAL_1, NAT_1, EXTREAL1, NEWTON, PREPOWER, SERIES_1, MESFUNC1, PROB_2, MEASURE6, MEASURE3, PARTFUN3, KURATO_2, RINFSUP1, SETLIM_1, MESFUNC5, RINFSUP2, SEQ_1; registrations SUBSET_1, XREAL_0, MEMBERED, ORDINAL1, PARTFUN1, MEASURE1, FUNCT_2, RELAT_1, XXREAL_0, XBOOLE_0, FUNCT_1, NUMBERS, VALUED_0, VALUED_1, SETLIM_1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; definitions TARSKI, CARD_3, FUNCT_6, MEASURE6, RINFSUP1, SETLIM_1, XCMPLX_0, RINFSUP2, VALUED_1; theorems ABSVALUE, MEASURE1, MEASURE2, MEASURE3, NAT_1, TARSKI, SUPINF_1, PARTFUN1, FUNCT_1, FUNCT_2, SEQFUNC, KURATO_2, SUPINF_2, RELSET_1, EXTREAL1, EXTREAL2, SETFAM_1, SEQ_1, SEQ_2, SEQM_3, SEQ_4, SERIES_1, RINFSUP1, MESFUNC1, XREAL_0, PROB_1, XBOOLE_0, XBOOLE_1, MESFUNC2, XREAL_1, PREPOWER, XXREAL_0, ZFMISC_1, SETLIM_1, REAL_2, PROB_4, PARTFUN2, ORDINAL1, MESFUNC5, RINFSUP2, CARD_3; schemes SEQ_1, FUNCT_2, SEQFUNC, PARTFUN2; begin :: Selected Properties of Functional Sequences reserve n,k for natural number, X for non empty set, S for SigmaField of X; theorem Th1: for M be sigma_Measure of S, F be Function of NAT,S, n holds {x where x is Element of X : for k st n <= k holds x in F.k } is Element of S proof let M be sigma_Measure of S, F be Function of NAT,S, n; set G = {x where x is Element of X : for k st n <= k holds x in F.k}; deffunc Fn(Element of NAT) = F.(n+$1); consider E be Function of NAT,S such that A1: for k be Element of NAT holds E.k=Fn(k) from FUNCT_2:sch 4; rng E is N_Sub_set_fam of X by MEASURE1:52; then rng E is N_Measure_fam of S by MEASURE2:def 1; then A2: meet rng E is Element of S by MEASURE2:3; now let z be set; assume z in G; then A3: ex x be Element of X st z=x & for k be natural number st n <= k holds x in F.k; for Y be set st Y in rng E holds z in Y proof let Y be set; assume Y in rng E; then consider l be set such that A4: l in NAT & Y=E.l by FUNCT_2:17; reconsider l as Element of NAT by A4; z in F.(n+l) by A3,NAT_1:12; hence z in Y by A1,A4; end; hence z in meet rng E by SETFAM_1:def 1; end; then A5: G c= meet rng E by TARSKI:def 3; now let z be set; assume A6: z in meet rng E; now let k be natural number; assume n <= k; then reconsider l=k-n as Element of NAT by NAT_1:21; E.l in rng E by FUNCT_2:6; then z in E.l by A6,SETFAM_1:def 1; then z in F.(n+l) by A1; hence z in F.k; end; hence z in G by A2,A6; end; then meet rng E c= G by TARSKI:def 3; hence thesis by A2,A5,XBOOLE_0:def 10; end; theorem Th2: for F be SetSequence of X, n be Element of NAT holds (superior_setsequence F).n = union rng(F^\n) & (inferior_setsequence F).n = meet rng(F^\n) proof let F be SetSequence of X, n be Element of NAT; {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; (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; end; theorem Th3: for M be sigma_Measure of S, F be SetSequence of S ex G be Function of NAT,S st G = inferior_setsequence F & M.(lim_inf F) = sup rng(M*G) proof let M be sigma_Measure of S, F be SetSequence of S; A1: dom(inferior_setsequence(F)) = NAT by FUNCT_2:def 1; for x be set st x in NAT holds (inferior_setsequence(F)).x in S by PROB_1:def 9; then reconsider G= inferior_setsequence(F) as Function of NAT,S by A1, FUNCT_2:5; now let n being Element of NAT; A2: n<=n+1 by NAT_1:12; inferior_setsequence(F) is non-decreasing by SETLIM_1:73; hence G.n c= G.(n+1) by A2,PROB_1:def 7; end; then M.(union rng G)= sup rng(M*G) by MEASURE2:27; hence thesis; end; theorem Th4: for M be sigma_Measure of S, F be SetSequence of S st M.(Union F) < +infty holds ex G be Function of NAT,S st G= superior_setsequence F & M.(lim_sup F) = inf rng(M*G) proof let M be sigma_Measure of S, F be SetSequence of S; assume A1: M.(Union F) < +infty; A2: dom(superior_setsequence F) = NAT by FUNCT_2:def 1; for x be set st x in NAT holds (superior_setsequence F).x in S by PROB_1:def 9; then reconsider G= superior_setsequence F as Function of NAT,S by A2, FUNCT_2:5; A3: for n being Element of NAT holds G.(n+1) c= G.n proof let n be Element of NAT; A4: n<=n+1 by NAT_1:12; superior_setsequence F is non-increasing by SETLIM_1:72; hence thesis by A4,PROB_1:def 6; end; G.0 = union {F.k where k is Element of NAT : 0 <= k} by SETLIM_1:def 3; then G.0 = union rng F by SETLIM_1:5; then A5: M.(meet rng G)= inf rng(M*G) by A1,A3,MEASURE3:14; reconsider F1 = F, G1 = G as SetSequence of X; consider f being SetSequence of X such that A6: lim_sup F1 = meet f & for n being Element of NAT holds f.n = Union (F1^\n) by KURATO_2:def 4; now let n be Element of NAT; f.n = Union (F1^\n) by A6; hence f.n = G1.n by Th2; end; then f = G1 by FUNCT_2:113; hence thesis by A5,A6; end; theorem for M be sigma_Measure of S, F be SetSequence of S st F is convergent holds ex G be Function of NAT,S st G= inferior_setsequence F & M.(lim F) = sup rng (M*G) proof let M be sigma_Measure of S, F be SetSequence of S; assume F is convergent; then lim_inf F = lim F by KURATO_2:def 7; hence thesis by Th3; end; theorem for M be sigma_Measure of S, F be SetSequence of S st F is convergent & M.(Union F) < +infty holds ex G be Function of NAT,S st G = superior_setsequence F & M.(lim F) = inf rng(M*G) proof let M be sigma_Measure of S, F be SetSequence of S; assume A1: F is convergent & M.(Union F) < +infty; then lim_sup F = lim F by KURATO_2:def 7; hence thesis by A1,Th4; end; definition let X,Y be set, F be Functional_Sequence of X,Y; attr F is with_the_same_dom means :Def1: rng F is with_common_domain; end; definition let X,Y be set, F be Functional_Sequence of X,Y; redefine attr F is with_the_same_dom means :Def2: for n,m be natural number holds dom(F.n) = dom(F.m); correctness proof A1: F is with_the_same_dom implies for n,m be natural number holds dom(F.n) = dom(F.m) proof assume F is with_the_same_dom; then A2: rng F is with_common_domain by Def1; hereby let n,m be natural number; dom F = NAT by SEQFUNC:def 1; then n in dom F & m in dom F by ORDINAL1:def 13; then F.n in rng F & F.m in rng F by FUNCT_1:12; hence dom(F.n) = dom(F.m) by A2,CARD_3:def 10; end; end; (for n,m be natural number holds dom(F.n) = dom(F.m)) implies F is with_the_same_dom proof assume A3: for n,m be natural number holds dom(F.n)=dom(F.m); now let f,g be Function; assume A4: f in rng F & g in rng F; then consider n be set such that A5: n in dom F & f = F.n by FUNCT_1:def 5; consider m be set such that A6: m in dom F & g = F.m by A4,FUNCT_1:def 5; n in NAT & m in NAT by A5,A6,SEQFUNC:def 1; then reconsider n,m as Nat by ORDINAL1:def 13; dom(F.n) = dom(F.m) by A3; hence dom f = dom g by A5,A6; end; then rng F is with_common_domain by CARD_3:def 10; hence F is with_the_same_dom by Def1; end; hence thesis by A1; end; end; registration let X,Y be set; cluster with_the_same_dom Functional_Sequence of X,Y; existence proof deffunc f(Nat) = <:{},X,Y:>; consider F be Functional_Sequence of X,Y such that A1: for n be Nat holds F.n = f(n) from SEQFUNC:sch 1; take F; hereby let n,m be natural number; F.n = <:{},X,Y:> & F.m = <:{},X,Y:> by A1; hence dom(F.n) = dom(F.m); end; end; end; definition let X be non empty set, f be Functional_Sequence of X,ExtREAL; func inf f -> PartFunc of X,ExtREAL means :Def3: dom it = dom(f.0) & for x be Element of X st x in dom it holds it.x = inf(f#x); existence proof deffunc F(Element of X) = inf (f#$1); defpred P[set] means $1 in dom(f.0); consider g being PartFunc of X,ExtREAL such that A1: (for x be Element of X holds x in dom g iff P[x]) & (for x be Element of X st x in dom g holds g/.x = F(x)) from PARTFUN2:sch 2; take g; A2: for x be set holds x in dom g iff x in dom(f.0) by A1; now let x be Element of X; assume A3: x in dom g; then g/.x = inf (f#x) by A1; hence g.x = inf (f#x) by A3,PARTFUN1:def 8; end; hence thesis by A2,TARSKI:2; end; uniqueness proof let g,h be PartFunc of X,ExtREAL; assume A4: dom g = dom (f.0) & for x be Element of X st x in dom g holds g.x=inf(f#x); assume A5: dom h = dom (f.0) & for x be Element of X st x in dom h holds h.x=inf(f#x); now let x be Element of X; assume A6: x in dom g; then g/.x = g.x by PARTFUN1:def 8; then g/.x = inf(f#x) by A4,A6; then g/.x = h.x by A4,A5,A6; hence g/.x = h/.x by A4,A5,A6,PARTFUN1:def 8; end; hence thesis by A4,A5,PARTFUN2:3; end; end; definition let X be non empty set, f be Functional_Sequence of X,ExtREAL; func sup f -> PartFunc of X,ExtREAL means :Def4: dom it = dom(f.0) & for x be Element of X st x in dom it holds it.x = sup(f#x); existence proof deffunc F(Element of X) = sup(f#$1); defpred P[set] means $1 in dom(f.0); consider g being PartFunc of X,ExtREAL such that A1: (for x be Element of X holds x in dom g iff P[x]) & for x be Element of X st x in dom g holds g/.x = F(x) from PARTFUN2:sch 2; take g; A2: for x be set holds x in dom g iff x in dom(f.0) by A1; now let x be Element of X; assume A3: x in dom g; then g/.x =sup (f#x) by A1; hence g.x =sup (f#x) by A3,PARTFUN1:def 8; end; hence thesis by A2,TARSKI:2; end; uniqueness proof let g,h be PartFunc of X,ExtREAL; assume A4: dom g = dom(f.0) & for x be Element of X st x in dom g holds g.x=sup(f#x); assume A5: dom h = dom(f.0) & for x be Element of X st x in dom h holds h.x=sup(f#x); now let x be Element of X; assume A6: x in dom g; then g/.x = g.x by PARTFUN1:def 8; then g/.x = sup(f#x) by A4,A6; then g/.x = h.x by A4,A5,A6; hence g/.x = h/.x by A4,A5,A6,PARTFUN1:def 8; end; hence thesis by A4,A5,PARTFUN2:3; end; end; definition let X be non empty set, f be Functional_Sequence of X,ExtREAL; func inferior_realsequence f -> with_the_same_dom Functional_Sequence of X,ExtREAL means :Def5: for n be natural number holds dom(it.n) = dom(f.0) & for x be Element of X st x in dom(it.n) holds (it.n).x=(inferior_realsequence(f#x)).n; existence proof defpred P[Element of NAT,Function] means dom $2 = dom(f.0) & for x be 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 P[n,y] proof let n being Element of NAT; deffunc F(Element of X) = (inferior_realsequence(f#$1)).n; defpred P[set] means $1 in dom(f.0); consider g being PartFunc of X,ExtREAL such that A2: (for x be Element of X holds x in dom g iff P[x]) & for x be Element of X st x in dom g holds g/.x = F(x) from PARTFUN2:sch 2; take g; A3: for x be set holds x in dom g iff x in dom(f.0) by A2; now let x be Element of X; assume A4: x in dom g; then g/.x =(inferior_realsequence (f#x)).n by A2; hence g.x =(inferior_realsequence (f#x)).n by A4,PARTFUN1:def 8; end; hence thesis by A3,PARTFUN1:119,TARSKI:2; end; consider g being Function of NAT,PFuncs(X,ExtREAL) such that A5: for n being Element of NAT holds P[n,g.n] from FUNCT_2:sch 10(A1); A6: for n holds dom(g.n) = dom(f.0) & for x be Element of X st x in dom(g.n) holds (g.n).x = (inferior_realsequence(f#x)).n proof let n; reconsider n'=n as Element of NAT by ORDINAL1:def 13; dom(g.n') = dom(f.0) & for x be Element of X st x in dom(g.n') holds (g.n').x = (inferior_realsequence(f#x)).n' by A5; hence thesis; end; A7: dom g = NAT by FUNCT_2:def 1; for n be Element of NAT holds g.n is PartFunc of X,ExtREAL; then reconsider g as Functional_Sequence of X,ExtREAL by A7,SEQFUNC:1; now let k,l be natural number; reconsider k'=k, l'=l as Element of NAT by ORDINAL1:def 13; dom(g.k') = dom(f.0) by A5; then dom(g.k) = dom(g.l') by A5; hence dom(g.k) = dom(g.l); end; then reconsider g as with_the_same_dom Functional_Sequence of X,ExtREAL by Def2; take g; thus thesis by A6; end; uniqueness proof let g,h be with_the_same_dom Functional_Sequence of X,ExtREAL; assume A8: for n be natural number holds dom (g.n) = dom (f.0) & for x be Element of X st x in dom (g.n) holds (g.n).x=(inferior_realsequence(f#x)).n; assume A9: for n be natural number holds dom (h.n) = dom (f.0) & for x be Element of X st x in dom (h.n) holds (h.n).x=(inferior_realsequence(f#x)).n; now let n be Element of NAT; A10: dom(g.n) = dom(f.0) by A8 .=dom(h.n) by A9; now let x be Element of X; assume A11: x in dom (g.n); then (g.n)/.x = (g.n).x by PARTFUN1:def 8; then (g.n)/.x = (inferior_realsequence (f#x)).n by A8,A11; then (g.n)/.x = (h.n).x by A9,A10,A11; hence (g.n)/.x = (h.n)/.x by A10,A11,PARTFUN1:def 8; end; hence g.n=h.n by A10,PARTFUN2:3; end; hence thesis by SEQFUNC:2; end; end; definition let X be non empty set, f be Functional_Sequence of X,ExtREAL; func superior_realsequence f -> with_the_same_dom Functional_Sequence of X,ExtREAL means :Def6: for n be natural number holds dom(it.n) = dom(f.0) & for x be Element of X st x in dom(it.n) holds (it.n).x = (superior_realsequence(f#x)).n; existence proof defpred P[Element of NAT,Function] means dom $2 = dom(f.0) & for x be 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 P[n, y] proof let n being Element of NAT; deffunc F(Element of X) = (superior_realsequence(f#$1)).n; defpred P[set] means $1 in dom(f.0); consider g being PartFunc of X,ExtREAL such that A2: (for x be Element of X holds x in dom g iff P[x]) & (for x be Element of X st x in dom g holds g/.x = F(x)) from PARTFUN2:sch 2; take g; A3: for x be set holds x in dom g iff x in dom(f.0) by A2; now let x be Element of X; assume A4: x in dom g; then g/.x =(superior_realsequence(f#x)).n by A2; hence g.x =(superior_realsequence(f#x)).n by A4,PARTFUN1:def 8; end; hence thesis by A3,PARTFUN1:119,TARSKI:2; end; consider g being Function of NAT, PFuncs(X,ExtREAL) such that A5: for n being Element of NAT holds P[n,g.n] from FUNCT_2:sch 10(A1); A6: for n holds dom(g.n) = dom(f.0) & for x be Element of X st x in dom(g.n) holds (g.n).x = (superior_realsequence(f#x)).n proof let n; reconsider n'=n as Element of NAT by ORDINAL1:def 13; dom(g.n') = dom(f.0) & for x be Element of X st x in dom(g.n') holds (g.n').x = (superior_realsequence(f#x)).n' by A5; hence thesis; end; A7: dom g = NAT by FUNCT_2:def 1; for n be Element of NAT holds g.n is PartFunc of X,ExtREAL; then reconsider g as Functional_Sequence of X,ExtREAL by A7,SEQFUNC:1; now let k,l be Nat; reconsider k'=k, l'=l as Element of NAT by ORDINAL1:def 13; dom(g.k') = dom(f.0) by A5; then dom(g.k) = dom(g.l') by A5; hence dom(g.k) = dom(g.l); end; then reconsider g as with_the_same_dom Functional_Sequence of X,ExtREAL by Def2; take g; thus thesis by A6; end; uniqueness proof let g,h be with_the_same_dom Functional_Sequence of X,ExtREAL; assume A8: for n holds dom (g.n) = dom (f.0) & for x be Element of X st x in dom (g.n) holds (g.n).x=(superior_realsequence(f#x)).n; assume A9: for n holds dom (h.n) = dom (f.0) & for x be Element of X st x in dom (h.n) holds (h.n).x=(superior_realsequence(f#x)).n; now let n be Element of NAT; A10: dom(g.n) = dom(f.0) by A8 .=dom(h.n) by A9; now let x be Element of X; assume A11: x in dom (g.n); then (g.n)/.x =(g.n).x by PARTFUN1:def 8; then (g.n)/.x =(superior_realsequence(f#x)).n by A8,A11; then (g.n)/.x =(h.n).x by A9,A10,A11; hence (g.n)/.x =(h.n)/.x by A10,A11,PARTFUN1:def 8; end; hence g.n=h.n by A10,PARTFUN2:3; end; hence thesis by SEQFUNC:2; end; end; theorem Th7: for f be Functional_Sequence of X,ExtREAL holds for x be Element of X st x in dom (f.0) holds (inferior_realsequence f)#x = inferior_realsequence(f#x) proof let f be Functional_Sequence of X,ExtREAL; set F = inferior_realsequence f; hereby let x be Element of X; assume A1: x in dom (f.0); now let n be Element of NAT; A2: dom(F.n) = dom (f.0) by Def5; (F#x).n = (F.n).x by MESFUNC5:def 13; hence (F#x).n =(inferior_realsequence (f#x)).n by A1,A2,Def5; end; hence F#x = inferior_realsequence(f#x) by FUNCT_2:113; end; end; definition let X,Y be set; redefine mode Functional_Sequence of X,Y -> Function of NAT,PFuncs(X,Y); coherence proof let f be Functional_Sequence of X,Y; dom f = NAT & rng f c= PFuncs(X,Y) by SEQFUNC:def 1; hence thesis by FUNCT_2:4; end; end; definition canceled; :: let X,Y be set, f be Functional_Sequence of X,Y, n be Element of NAT; :: func f^\n -> Functional_Sequence of X,Y equals :: f^\n; :: correctness; 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; cluster f^\n -> with_the_same_dom; coherence proof for k,l be Nat holds dom((f^\n).k)=dom((f^\n).l) proof let k,l be Nat; reconsider k'=k, l'=l as Element of NAT by ORDINAL1:def 13; reconsider g=f as Function of NAT,PFuncs(X,Y); dom((f^\n).k) = dom((g.(n+k'))) by KURATO_2:def 2; then dom((f^\n).k) = dom((g.(n+l'))) by Def2; hence dom((f^\n).k)=dom((f^\n).l) by KURATO_2:def 2; end; hence f^\n is with_the_same_dom by Def2; end; end; theorem Th8: for f be with_the_same_dom Functional_Sequence of X,ExtREAL, n be Element of NAT holds (inferior_realsequence f).n = inf(f^\n) proof let f be with_the_same_dom Functional_Sequence of X,ExtREAL, n be Element of NAT; reconsider g=f as Function of NAT,PFuncs(X,ExtREAL); A1: dom((inferior_realsequence f).n) = dom(f.0) by Def5; dom inf(f^\n) =dom((f^\n).0) by Def3; then dom inf(f^\n) =dom(g.(n+(0 qua Nat))) by KURATO_2:def 2; then A2: dom inf(f^\n) =dom(f.0) by Def2; now let x be Element of X; assume A3: x in dom inf(f^\n); now let k be Element of NAT; ((f^\n)#x).k =((f^\n).k).x by MESFUNC5:def 13; then ((f^\n)#x).k =(g.(n+k)).x by KURATO_2:def 2; then ((f^\n)#x).k =(f#x).(n+k) by MESFUNC5:def 13; hence ((f^\n)#x).k = ((f#x)^\n).k by KURATO_2:def 2; end; then (f^\n)#x = (f#x)^\n by FUNCT_2:113; then A4: (inf(f^\n)).x =inf((f#x)^\n) by A3,Def3; ((inferior_realsequence f).n ).x = (inferior_realsequence(f#x)).n by A1,A2,A3,Def5; hence (inf(f^\n)).x = ((inferior_realsequence f).n).x by A4,RINFSUP2:27; end; hence thesis by A1,A2,PARTFUN1:34; end; theorem Th9: for f be with_the_same_dom Functional_Sequence of X,ExtREAL, n be Element of NAT holds (superior_realsequence f).n = sup(f^\n) proof let f be with_the_same_dom Functional_Sequence of X,ExtREAL, n be Element of NAT; reconsider g=f as Function of NAT,PFuncs(X,ExtREAL); A1: dom ((superior_realsequence f).n) = dom(f.0) by Def6; dom sup(f^\n) = dom((f^\n).0) by Def4; then dom sup(f^\n) = dom(g.(n+(0 qua Nat))) by KURATO_2:def 2; then A2: dom sup(f^\n) = dom(f.0) by Def2; now let x be Element of X; assume A3: x in dom sup(f^\n); now let k be Element of NAT; ((f^\n)#x).k =((f^\n).k).x by MESFUNC5:def 13; then ((f^\n)#x).k =(g.(n+k)).x by KURATO_2:def 2; then ((f^\n)#x).k =(f#x).(n+k) by MESFUNC5:def 13; hence ((f^\n)#x).k = ((f#x)^\n).k by KURATO_2:def 2; end; then (f^\n)#x = (f#x)^\n by FUNCT_2:113; then A4: (sup(f^\n)).x =sup ((f#x)^\n) by A3,Def4; ((superior_realsequence f).n ).x = (superior_realsequence (f#x)).n by A1,A2,A3,Def6; hence (sup (f^\n)).x = ((superior_realsequence f).n ).x by A4,RINFSUP2:27; end; hence thesis by A1,A2,PARTFUN1:34; end; theorem Th10: for f be Functional_Sequence of X,ExtREAL, x be Element of X st x in dom(f.0) holds (superior_realsequence f)#x = superior_realsequence(f#x) proof let f be Functional_Sequence of X,ExtREAL, x be Element of X; assume A1: x in dom(f.0); set F = superior_realsequence f; now let n be Element of NAT; dom(F.n) = dom(f.0) & (F#x).n = (F.n).x by Def6,MESFUNC5:def 13; hence (F#x).n =(superior_realsequence(f#x)).n by A1,Def6; end; hence F#x = superior_realsequence(f#x) by FUNCT_2:113; end; definition let X be non empty set, f be Functional_Sequence of X,ExtREAL; func lim_inf f -> PartFunc of X,ExtREAL means :Def8: dom it = dom (f.0) & for x be Element of X st x in dom it holds it.x = lim_inf(f#x); existence proof deffunc F(Element of X) = lim_inf(f#$1); defpred P[set] means $1 in dom(f.0); consider g being PartFunc of X,ExtREAL such that A1: (for x be Element of X holds x in dom g iff P[x]) & for x be Element of X st x in dom g holds g/.x = F(x) from PARTFUN2:sch 2; take g; A2: for x be set holds x in dom g iff x in dom(f.0) by A1; now let x be Element of X; assume A3: x in dom g; then g/.x =lim_inf(f#x) by A1; hence g.x =lim_inf(f#x) by A3,PARTFUN1:def 8; end; hence thesis by A2,TARSKI:2; end; uniqueness proof let g,h be PartFunc of X,ExtREAL; assume that A4: dom g = dom(f.0) & for x be Element of X st x in dom g holds g.x=lim_inf(f#x) and A5: dom h = dom(f.0) & for x be Element of X st x in dom h holds h.x=lim_inf(f#x); now let x be Element of X; assume A6: x in dom g; then g/.x =g.x by PARTFUN1:def 8; then g/.x =lim_inf (f#x) by A4,A6; then g/.x =h.x by A4,A5,A6; hence g/.x =h/.x by A4,A5,A6,PARTFUN1:def 8; end; hence thesis by A4,A5,PARTFUN2:3; end; end; definition let X be non empty set, f be Functional_Sequence of X,ExtREAL; func lim_sup f -> PartFunc of X,ExtREAL means :Def9: dom it = dom (f.0) & for x be Element of X st x in dom it holds it.x = lim_sup(f#x); existence proof deffunc F(Element of X) = lim_sup(f#$1); defpred P[set] means $1 in dom(f.0); consider g being PartFunc of X,ExtREAL such that A1: (for x be Element of X holds x in dom g iff P[x]) & for x be Element of X st x in dom g holds g/.x = F(x) from PARTFUN2:sch 2; take g; A2: for x be set holds x in dom g iff x in dom(f.0) by A1; now let x be Element of X; assume A3: x in dom g; then g/.x =lim_sup(f#x) by A1; hence g.x =lim_sup(f#x) by A3,PARTFUN1:def 8; end; hence thesis by A2,TARSKI:2; end; uniqueness proof let g,h be PartFunc of X,ExtREAL; assume A4: dom g = dom(f.0) & for x be Element of X st x in dom g holds g.x=lim_sup(f#x); assume A5: dom h = dom(f.0) & for x be Element of X st x in dom h holds h.x=lim_sup(f#x); now let x be Element of X; assume A6: x in dom g; then g/.x = g.x by PARTFUN1:def 8; then g/.x = lim_sup (f#x) by A4,A6; then g/.x = h.x by A4,A5,A6; hence g/.x = h/.x by A4,A5,A6,PARTFUN1:def 8; end; hence thesis by A4,A5,PARTFUN2:3; end; end; theorem Th11: for f be Functional_Sequence of X,ExtREAL holds (for x be 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 f be Functional_Sequence of X,ExtREAL; 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 Def8; A2: now let x be Element of X; assume A3: x in dom lim_inf f; then A4: (lim_inf f).x=lim_inf(f#x) by Def8; hence (lim_inf f).x= sup inferior_realsequence(f#x); dom lim_inf f = dom(f.0) by Def8; hence (lim_inf f).x = sup((inferior_realsequence f)#x) by A3,A4,Th7; hence (lim_inf f).x =(sup inferior_realsequence f).x by A1,A3,Def4; end; then for x be Element of X st x in dom lim_inf f holds (lim_inf f).x =(sup inferior_realsequence f).x; hence thesis by A1,A2,PARTFUN1:34; end; theorem Th12: for f be Functional_Sequence of X,ExtREAL holds (for x be 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 f be Functional_Sequence of X,ExtREAL; A1: dom(inf superior_realsequence f) =dom((superior_realsequence f).0) by Def3 .=dom(f.0) by Def6 .=dom lim_sup f by Def9; A2: now let x be Element of X; assume A3: x in dom (lim_sup f); then A4: (lim_sup f).x=lim_sup (f#x) by Def9; hence (lim_sup f).x = inf superior_realsequence(f#x); dom lim_sup f = dom(f.0) by Def9; hence (lim_sup f).x = inf((superior_realsequence f)#x) by A3,A4,Th10; hence (lim_sup f).x = (inf superior_realsequence f).x by A1,A3,Def3; end; then for x be Element of X st x in dom lim_sup f holds (lim_sup f).x =(inf superior_realsequence f).x; hence thesis by A1,A2,PARTFUN1:34; end; theorem for f be Functional_Sequence of X,ExtREAL, x be 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 f be Functional_Sequence of X,ExtREAL, x be Element of X; assume x in dom(f.0); then x in dom(lim_sup f) & x in dom(lim_inf f) by Def8,Def9; then (lim_sup f).x = lim_sup (f#x) & (lim_inf f).x = lim_inf (f#x) by Def8,Def9; hence thesis by RINFSUP2:40; end; definition let X be non empty set, f be Functional_Sequence of X,ExtREAL; func lim f -> PartFunc of X,ExtREAL means :Def10: dom it = dom (f.0) & for x be Element of X st x in dom it holds it.x=lim(f#x); existence proof deffunc F(Element of X) = lim (f#$1); defpred P[set] means $1 in dom(f.0); consider g being PartFunc of X,ExtREAL such that A1: (for x be Element of X holds x in dom g iff P[x]) & for x be Element of X st x in dom g holds g/.x = F(x) from PARTFUN2:sch 2; take g; A2: for x be set holds x in dom g iff x in dom(f.0) by A1; now let x be Element of X; assume A3: x in dom g; then g/.x =lim(f#x) by A1; hence g.x =lim(f#x) by A3,PARTFUN1:def 8; end; hence thesis by A2,TARSKI:2; end; uniqueness proof let g,h be PartFunc of X,ExtREAL; assume A4: dom g = dom (f.0) & for x be Element of X st x in dom g holds g.x=lim(f#x); assume A5: dom h = dom (f.0) & for x be Element of X st x in dom h holds h.x=lim(f#x); now let x be Element of X; assume A6: x in dom g; then g/.x = g.x by PARTFUN1:def 8; then g/.x = lim (f#x) by A4,A6; then g/.x = h.x by A4,A5,A6; hence g/.x = h/.x by A4,A5,A6,PARTFUN1:def 8; end; hence thesis by A4,A5,PARTFUN2:3; end; end; theorem Th14: for f be Functional_Sequence of X,ExtREAL, x be 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 f be Functional_Sequence of X,ExtREAL; let x be Element of X; assume A1: x in dom lim f & f#x is convergent; then x in dom (f.0) by Def10; then x in dom(lim_sup f) & x in dom(lim_inf f) by Def8,Def9; then A2: (lim_sup f).x = lim_sup (f#x) & (lim_inf f).x = lim_inf (f#x) by Def8,Def9; lim (f#x) = lim_sup (f#x) & lim (f#x) = lim_inf (f#x) by A1,RINFSUP2:41; hence thesis by A1,A2,Def10; end; theorem Th15: for f be with_the_same_dom Functional_Sequence of X,ExtREAL, F be SetSequence of S, r be real number st (for n be natural number 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 f be with_the_same_dom Functional_Sequence of X,ExtREAL, F be SetSequence of S, r be real number; set E = dom(f.0); assume A1: for n be natural number holds F.n = E /\ great_dom(f.n,R_EAL r); now let x be set; assume x in union rng F; then consider y be set such that A2: x in y & y in rng F by TARSKI:def 4; consider n be set such that A3: n in dom F & y=F.n by A2,FUNCT_1:def 5; reconsider z=x as Element of X by A2; reconsider n as Element of NAT by A3; F.n = E /\ great_dom(f.n,R_EAL r) by A1; then A4: x in E & x in great_dom(f.n,r) by A2,A3,XBOOLE_0:def 3; then A5: r < (f.n).z by MESFUNC1:def 14; A6: x in dom (sup f) by A4,Def4; then A7: (sup f).z = sup(f#z) by Def4; (f.n).z=(f#z).n by MESFUNC5:def 13; then (f.n).z <= (sup f).z by A7,RINFSUP2:23; then R_EAL r < (sup f).z by A5,XXREAL_0:2; then x in great_dom(sup f,R_EAL r) by A6,MESFUNC1:def 14; hence x in E /\ great_dom(sup f,R_EAL r) by A4,XBOOLE_0:def 3; end; then A8: union rng F c= E /\ great_dom(sup f,R_EAL r) by TARSKI:def 3; now let x be set; assume A9: x in E /\ great_dom(sup f,R_EAL r); then reconsider z=x as Element of X; A10: x in E & x in great_dom(sup f,R_EAL r) by A9,XBOOLE_0:def 3; then A11: R_EAL r < (sup f).z by MESFUNC1:def 14; ex n be Element of NAT st R_EAL r < (f.n).z proof assume A12: for n be Element of NAT holds (f.n).z <= R_EAL r; for x be ext-real number st x in rng (f#z) holds x <= R_EAL r proof let x be ext-real number; assume x in rng (f#z); then consider m be set such that A13: m in NAT & x=(f#z).m by FUNCT_2:17; reconsider m as Element of NAT by A13; x=(f.m).z by A13,MESFUNC5:def 13; hence thesis by A12; end; then R_EAL r is majorant of rng (f#z) by SUPINF_1:def 9; then A14: sup (f#z) <= R_EAL r by SUPINF_1:def 16; x in dom (sup f) by A10,Def4; hence contradiction by A11,A14,Def4; end; then consider n be Element of NAT such that A15: R_EAL r < (f.n).z; x in dom (f.n) by A10,Def2; then A16: x in E & x in great_dom(f.n,R_EAL r) by A9,A15,MESFUNC1:def 14,XBOOLE_0:def 3; F.n = E /\ great_dom(f.n,R_EAL r) by A1; then A17: x in F.n by A16,XBOOLE_0:def 3; F.n in rng F by FUNCT_2:6; hence x in union rng F by A17,TARSKI:def 4; end; then E /\ great_dom((sup f),R_EAL r) c= union rng F by TARSKI:def 3; hence union rng F = E /\ great_dom(sup f,R_EAL r) by A8,XBOOLE_0:def 10; end; theorem Th16: for f be with_the_same_dom Functional_Sequence of X,ExtREAL, F be SetSequence of S, r be real number st (for n be natural number 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 f be with_the_same_dom Functional_Sequence of X,ExtREAL, F be SetSequence of S, r be real number; assume A1: for n be natural number holds F.n = dom(f.0) /\ great_eq_dom(f.n,R_EAL r); set E = dom(f.0); now let x be set; assume A2: x in meet rng F; then reconsider z=x as Element of X; F.0 in rng F by FUNCT_2:6; then A3: x in F.0 by A2,SETFAM_1:def 1; F.0 = E /\ great_eq_dom(f.0,R_EAL r) by A1; then A4: x in E & x in great_eq_dom(f.0,R_EAL r) by A3,XBOOLE_0:def 3; A5: now let n be Element of NAT; F.n in rng F by FUNCT_2:6; then A6: z in F.n by A2,SETFAM_1:def 1; F.n = E /\ great_eq_dom(f.n,R_EAL r) by A1; then z in E & x in great_eq_dom(f.n,R_EAL r) by A6,XBOOLE_0:def 3; then R_EAL r <= (f.n).z by MESFUNC1:def 15; hence R_EAL r <= (f#z).n by MESFUNC5:def 13; end; now let s be ext-real number; assume s in rng (f#z); then ex k be set st k in NAT & s=(f#z).k by FUNCT_2:17; hence R_EAL r <= s by A5; end; then R_EAL r is minorant of rng (f#z) by SUPINF_1:def 10; then A7: R_EAL r <= inf (f#z) by SUPINF_1:def 17; A8: x in dom (inf f) by A4,Def3; then R_EAL r <= (inf f).x by A7,Def3; then x in great_eq_dom(inf f,R_EAL r) by A8,MESFUNC1:def 15; hence x in E /\ great_eq_dom(inf f,R_EAL r) by A4,XBOOLE_0:def 3; end; then A9: meet rng F c= E /\ great_eq_dom(inf f,R_EAL r) by TARSKI:def 3; now let x be set; assume A10: x in E /\ great_eq_dom(inf f,R_EAL r); then reconsider z=x as Element of X; A11: x in E & x in great_eq_dom(inf f,R_EAL r) by A10,XBOOLE_0:def 3; then A12: R_EAL r <= (inf f).z by MESFUNC1:def 15; now let y be set; assume y in rng F; then consider n be set such that A13: n in NAT & y=F.n by FUNCT_2:17; reconsider n as Element of NAT by A13; x in dom inf f by A11,Def3; then A14: (inf f).z = inf(f#z) by Def3; (f.n).z=(f#z).n by MESFUNC5:def 13; then inf (f#z)<= (f.n).z by RINFSUP2:23; then A15: R_EAL r <= (f.n).z by A12,A14,XXREAL_0:2; x in dom (f.n) by A11,Def2; then A16: x in E & x in great_eq_dom(f.n,R_EAL r) by A10,A15,MESFUNC1:def 15,XBOOLE_0:def 3; F.n = E /\ great_eq_dom(f.n,R_EAL r) by A1; hence x in y by A13,A16,XBOOLE_0:def 3; end; hence x in meet rng F by SETFAM_1:def 1; end; then E /\ great_eq_dom((inf f),R_EAL r) c= meet rng F by TARSKI:def 3; hence meet rng F = E /\ great_eq_dom(inf f,R_EAL r) by A9,XBOOLE_0:def 10; end; theorem Th17: for f be with_the_same_dom Functional_Sequence of X,ExtREAL, F be SetSequence of S, r be real number st (for n be natural number holds F.n = dom(f.0) /\ great_dom(f.n,R_EAL r)) holds for n be natural number holds (superior_setsequence F).n = dom(f.0) /\ great_dom((superior_realsequence f).n,R_EAL r) proof let f be with_the_same_dom Functional_Sequence of X,ExtREAL, F be SetSequence of S, r be real number; set E = dom(f.0); assume A1: for n be natural number holds F.n = E /\ great_dom(f.n,R_EAL r); let n be natural number; reconsider n'=n as Element of NAT by ORDINAL1:def 13; set f1=f^\n'; set F1=F^\n'; now let k be Element of NAT; F1.k= F.(n+k) by KURATO_2:def 2; hence F1.k in S by PROB_1:def 9; end; then A2: F1 is SetSequence of S by PROB_1:def 9; consider g be Function of NAT,PFuncs(X,ExtREAL) such that A3: f=g & f^\n'=g^\n'; f1.0 = g.(n+(0 qua Nat)) by A3,KURATO_2:def 2; then A4: dom(f1.0)= E by A3,Def2; now let k be natural number; reconsider k'=k as Element of NAT by ORDINAL1:def 13; F1.k = F.(n+k') by KURATO_2:def 2; then F1.k = E /\ great_dom(f.(n+k'),R_EAL r) by A1; hence F1.k = E /\ great_dom(f1.k,R_EAL r) by KURATO_2:def 2; end; then A5: union rng F1 = E /\ great_dom(sup f1,R_EAL r) by A2,A4,Th15; union rng (F^\n') = (superior_setsequence F).n by Th2; hence thesis by A5,Th9; end; theorem Th18: for f be with_the_same_dom Functional_Sequence of X,ExtREAL, F be SetSequence of S, r be real number st (for n be natural number holds F.n = dom(f.0) /\ great_eq_dom(f.n,R_EAL r)) holds for n be natural number holds (inferior_setsequence F).n = dom(f.0) /\ great_eq_dom((inferior_realsequence f).n,R_EAL r) proof let f be with_the_same_dom Functional_Sequence of X,ExtREAL, F be SetSequence of S, r be real number; set E = dom(f.0); assume that A1: for n be natural number holds F.n = E /\ great_eq_dom(f.n,R_EAL r); let n be natural number; reconsider n'=n as Element of NAT by ORDINAL1:def 13; set f1=f^\n'; set F1=F^\n'; now let k be Element of NAT; F1.k= F.(n+k) by KURATO_2:def 2; hence F1.k in S by PROB_1:def 9; end; then A2: F1 is SetSequence of S by PROB_1:def 9; consider g be Function of NAT,PFuncs(X,ExtREAL) such that A3: f=g & f^\n'=g^\n'; f1.0 = g.(n+(0 qua Nat)) by A3,KURATO_2:def 2; then A4: dom(f1.0) = E by A3,Def2; now let k be natural number; reconsider k'=k as Element of NAT by ORDINAL1:def 13; F1.k = F.(n+k') by KURATO_2:def 2; then F1.k = E /\ great_eq_dom(f.(n+k'),R_EAL r) by A1; hence F1.k = E /\ great_eq_dom(f1.k,R_EAL r) by KURATO_2:def 2; end; then A5: meet rng F1 = E /\ great_eq_dom(inf f1,R_EAL r) by A2,A4,Th16; meet rng(F^\n') = (inferior_setsequence F).n by Th2; hence thesis by A5,Th8; end; theorem Th19: for f be with_the_same_dom Functional_Sequence of X,ExtREAL, E be Element of S st dom (f.0) = E & (for n be natural number holds f.n is_measurable_on E) holds for n holds (superior_realsequence f).n is_measurable_on E proof let f be with_the_same_dom Functional_Sequence of X,ExtREAL, E be Element of S; assume A1: dom (f.0) = E & for n be natural number holds f.n is_measurable_on E; let n; reconsider n'=n as Element of NAT by ORDINAL1:def 13; A2: dom((superior_realsequence f).n') = E by A1,Def6; now let r be real number; deffunc G(Element of NAT) = E /\ great_dom(f.$1,R_EAL r); consider F being Function of NAT,bool X such that A3: for x being Element of NAT holds F.x = G(x) from FUNCT_2:sch 4; A4: for x being natural number holds F.x = E /\ great_dom(f.x,R_EAL r) proof let x be natural number; reconsider x'=x as Element of NAT by ORDINAL1:def 13; F.x' = E /\ great_dom(f.x',R_EAL r) by A3; hence thesis; end; now let i be Element of NAT; A5: F.i=E /\ great_dom(f.i,R_EAL r) by A3; A6: f.i is_measurable_on E by A1; dom (f.i) = E by A1,Def2; hence F.i in S by A5,A6,MESFUNC1:33; end; then reconsider F as SetSequence of S by PROB_1:def 9; for x be set st x in NAT holds (superior_setsequence F).x in S by PROB_1:def 9; then (superior_setsequence F).n' in S; hence E /\ great_dom((superior_realsequence f).n,R_EAL r) is_measurable_on S by A1,A4,Th17; end; hence (superior_realsequence f).n is_measurable_on E by A2,MESFUNC1:33; end; theorem Th20: for f be with_the_same_dom Functional_Sequence of X,ExtREAL, E be Element of S st dom (f.0) = E & (for n be natural number holds f.n is_measurable_on E) holds for n be natural number holds (inferior_realsequence f).n is_measurable_on E proof let f be with_the_same_dom Functional_Sequence of X,ExtREAL, E be Element of S; assume A1: dom(f.0) = E & for n be natural number holds f.n is_measurable_on E; let n be natural number; reconsider n'=n as Element of NAT by ORDINAL1:def 13; A2: dom((inferior_realsequence f).n') = E by A1,Def5; now let r be real number; deffunc G(Element of NAT) = E /\ great_eq_dom(f.$1,R_EAL r); consider F being Function of NAT,bool X such that A3: for x being Element of NAT holds F.x = G(x) from FUNCT_2:sch 4; A4: for x being natural number holds F.x = E /\ great_eq_dom(f.x,R_EAL r) proof let x be natural number; reconsider x'=x as Element of NAT by ORDINAL1:def 13; F.x' = E /\ great_eq_dom(f.x',R_EAL r) by A3; hence thesis; end; now let i be Element of NAT; A5: F.i=E /\ great_eq_dom(f.i,R_EAL r) by A3; A6: f.i is_measurable_on E by A1; dom (f.i) = E by A1,Def2; hence F.i in S by A5,A6,MESFUNC1:31; end; then reconsider F as SetSequence of S by PROB_1:def 9; for x be set st x in NAT holds (inferior_setsequence F).x in S by PROB_1:def 9; then (inferior_setsequence F).n' in S; hence E /\ great_eq_dom((inferior_realsequence f).n,R_EAL r ) is_measurable_on S by A1,A4,Th18; end; hence (inferior_realsequence f).n is_measurable_on E by A2,MESFUNC1:31; end; theorem Th21: for f be Functional_Sequence of X,ExtREAL, F be SetSequence of S, r be real number st (for n be natural number 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 f be Functional_Sequence of X,ExtREAL, F be SetSequence of S, r be real number; set E = dom(f.0); set g=superior_realsequence f; assume A1: for n be natural number holds F.n = E /\ great_eq_dom(g.n,R_EAL r); dom(g.0) = dom(f.0) by Def6; then meet rng F = E /\ great_eq_dom(inf g,R_EAL r) by A1,Th16; hence thesis by Th12; end; theorem Th22: for f be Functional_Sequence of X,ExtREAL, F be SetSequence of S, r be real number st (for n be natural number 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 f be Functional_Sequence of X,ExtREAL, F be SetSequence of S, r be real number; set E = dom(f.0); set g=inferior_realsequence f; assume A1: for n be natural number holds F.n = E /\ great_dom(g.n,R_EAL r); dom(g.0) = dom(f.0) by Def5; then union rng F = E /\ great_dom(sup g,R_EAL r) by A1,Th15; hence thesis by Th11; end; theorem Th23: for f be with_the_same_dom Functional_Sequence of X,ExtREAL, E be Element of S st dom (f.0) = E & (for n be natural number holds f.n is_measurable_on E) holds lim_sup f is_measurable_on E proof let f be with_the_same_dom Functional_Sequence of X,ExtREAL, E be Element of S; assume A1: dom (f.0) = E & for n be natural number holds f.n is_measurable_on E; A2: dom (lim_sup f) = dom(f.0) by Def9; now let r be real number; deffunc G(Element of NAT) = E /\ great_eq_dom((superior_realsequence f).$1,R_EAL r); consider F being Function of NAT,bool X such that A3: for x being Element of NAT holds F.x = G(x) from FUNCT_2:sch 4; A4: for x being natural number holds F.x = E /\ great_eq_dom((superior_realsequence f).x,R_EAL r) proof let x be natural number; reconsider x'=x as Element of NAT by ORDINAL1:def 13; F.x' = E /\ great_eq_dom((superior_realsequence f).x',R_EAL r) by A3; hence thesis; end; now let i be Element of NAT; A5: F.i = E /\ great_eq_dom((superior_realsequence f).i,R_EAL r) by A3; A6: (superior_realsequence f).i is_measurable_on E by A1,Th19; dom((superior_realsequence f).i) = dom(f.0) by Def6; hence F.i in S by A1,A5,A6,MESFUNC1:31; end; then reconsider F as SetSequence of S by PROB_1:def 9; A7: meet F = E /\ great_eq_dom(lim_sup f,R_EAL r) by A1,A4,Th21; A8: dom F = NAT by FUNCT_2:def 1; for x be set st x in NAT holds F.x in S by PROB_1:def 9; then A9: F is Function of NAT,S by A8,FUNCT_2:5; then A10: rng F is N_Sub_set_fam of X by MEASURE1:52; rng F c= S by A9,RELSET_1:12; then rng F is N_Measure_fam of S by A10,MEASURE2:def 1; hence E /\ great_eq_dom(lim_sup f,R_EAL r) is_measurable_on S by A7, MEASURE2:3; end; hence lim_sup f is_measurable_on E by A1,A2,MESFUNC1:31; end; theorem for f be with_the_same_dom Functional_Sequence of X,ExtREAL, E be Element of S st dom(f.0) = E & (for n be natural number holds f.n is_measurable_on E) holds lim_inf f is_measurable_on E proof let f be with_the_same_dom Functional_Sequence of X,ExtREAL, E be Element of S; assume A1: dom(f.0) = E & for n be natural number holds f.n is_measurable_on E; then A2: dom lim_inf f = E by Def8; now let r be real number; deffunc G(Element of NAT) = E /\ great_dom((inferior_realsequence f).$1,R_EAL r); consider F being Function of NAT,bool X such that A3: for x being Element of NAT holds F.x = G(x) from FUNCT_2:sch 4; A4: for x be natural number holds F.x = E /\ great_dom((inferior_realsequence f).x,R_EAL r) proof let x be natural number; reconsider x'=x as Element of NAT by ORDINAL1:def 13; F.x' = E /\ great_dom((inferior_realsequence f).x',R_EAL r) by A3; hence thesis; end; now let i be Element of NAT; A5: F.i = E /\ great_dom((inferior_realsequence f).i,R_EAL r) by A3; A6: (inferior_realsequence f).i is_measurable_on E by A1,Th20; dom((inferior_realsequence f).i) = E by A1,Def5; hence F.i in S by A5,A6,MESFUNC1:33; end; then reconsider F as SetSequence of S by PROB_1:def 9; A7: union rng F = E /\ great_dom(lim_inf f,R_EAL r) by A1,A4,Th22; A8: dom F = NAT by FUNCT_2:def 1; for x be set st x in NAT holds F.x in S by PROB_1:def 9; then A9: F is Function of NAT,S by A8,FUNCT_2:5; then A10: rng F c= S by RELSET_1:12; rng F is N_Sub_set_fam of X by A9,MEASURE1:52; then rng F is N_Measure_fam of S by A10,MEASURE2:def 1; hence E /\ great_dom(lim_inf f,R_EAL r) is_measurable_on S by A7,MEASURE2:3; end; hence lim_inf f is_measurable_on E by A2,MESFUNC1:33; end; theorem Th25: for f be with_the_same_dom Functional_Sequence of X,ExtREAL, E be Element of S st dom(f.0) = E & (for n be natural number holds f.n is_measurable_on E) & (for x be Element of X st x in E holds f#x is convergent) holds lim f is_measurable_on E proof let f be with_the_same_dom Functional_Sequence of X,ExtREAL, E be Element of S; assume A1: dom (f.0) = E; then A2: dom lim f = E & dom lim_sup f = E by Def9,Def10; assume that A3: for n be natural number holds f.n is_measurable_on E and A4: for x be Element of X st x in E holds f#x is convergent; A5: now let x be Element of X; assume A6: x in dom lim f; then f#x is convergent by A2,A4; hence (lim f).x= (lim_sup f).x by A6,Th14; end; lim_sup f is_measurable_on E by A1,A3,Th23; hence thesis by A2,A5,PARTFUN1:34; end; theorem Th26: for f be with_the_same_dom Functional_Sequence of X,ExtREAL, g be PartFunc of X,ExtREAL, E be Element of S st dom(f.0) = E & (for n be natural number holds f.n is_measurable_on E) & dom g = E & for x be 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 f be with_the_same_dom Functional_Sequence of X,ExtREAL, g be PartFunc of X,ExtREAL, E be Element of S; assume that A1: dom (f.0) = E & for n be natural number holds f.n is_measurable_on E and A2: dom g = E and A3: for x be Element of X st x in E holds f#x is convergent & g.x = lim(f#x); A4: for x be Element of X st x in E holds f#x is convergent by A3; A5: dom lim f = E by A1,Def10; now let x be Element of X; assume A6: x in dom lim f; then g.x= lim(f#x) by A3,A5; hence g.x = (lim f).x by A6,Def10; end; then g = lim f by A2,A5,PARTFUN1:34; hence thesis by A1,A4,Th25; end; theorem Th27: for f be Functional_Sequence of X,ExtREAL, g be PartFunc of X,ExtREAL st for x be Element of X st x in dom g holds f#x is convergent_to_finite_number & g.x = lim (f#x) holds g is finite proof let f be Functional_Sequence of X,ExtREAL, g be PartFunc of X,ExtREAL; assume that A1: for x be Element of X st x in dom g holds f#x is convergent_to_finite_number & g.x = lim (f#x); now let x be Element of X; assume A2: x in dom g; then A3: f#x is convergent_to_finite_number & g.x = lim (f#x) by A1; then A4: f#x is convergent by MESFUNC5:def 11; not (lim (f#x)=-infty & f#x is convergent_to_-infty ) & not (lim (f#x)=+infty & f#x is convergent_to_+infty ) by A3,MESFUNC5:56,57; then consider g0 be real number such that A5: lim (f#x) = g0 & (for p be real number st 0