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 natural number 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 natural number 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 natural number 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 natural number 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 natural number holds f . n is_measurable_on E ; :: thesis: lim_inf f is_measurable_on E

A3: now

let r be real number ; :: thesis: E /\ (great_dom (lim_inf f),(R_EAL r)) in S
deffunc H₁( 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 = H₁(x) from FUNCT_2:sch 4();

now

let i be Nat; :: thesis: F . i in S
i in NAT by ORDINAL1:def 13;
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:33; :: thesis: verum

end;

then A7: rng F c= S by NAT_1:53;
A8: for x being natural number holds F . x = E /\ (great_dom ((inferior_realsequence f) . x),(R_EAL r))

proof

let x be natural number ; :: thesis: F . x = E /\ (great_dom ((inferior_realsequence f) . x),(R_EAL r))
reconsider x9 = x as Element of NAT by ORDINAL1:def 13;
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 by RELAT_1:def 19;
then F is Function of NAT ,S by FUNCT_2:8;
then A9: rng F is N_Sub_set_fam of X by MEASURE1:52;
rng F c= S by RELAT_1:def 19;
then 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:3; :: thesis: verum

end;

dom (lim_inf f) = E by A1, Def8;
hence lim_inf f is_measurable_on E by A3, MESFUNC1:33; :: thesis: verum