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 A1: ( dom (f . 0 ) = E & ( for n being natural number holds f . n is_measurable_on E ) ) ; :: thesis: lim_inf f is_measurable_on E
then A2: dom (lim_inf f) = E by Def8;

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
A3: for x being Element of NAT holds F . x = H₁(x) from FUNCT_2:sch 4();
A4: 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 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 F . x = E /\ (great_dom ((inferior_realsequence f) . x),(R_EAL r)) ; :: thesis: verum

end;

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 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; :: thesis: verum

end;

then rng F c= S by NAT_1:53;
then reconsider F = F as SetSequence of by RELAT_1:def 19;
A7: union (rng F) = E /\ (great_dom (lim_inf f),(R_EAL r)) by A1, A4, Th22;
rng F c= S by RELAT_1:def 19;
then A9: F is Function of NAT ,S by FUNCT_2:8;
A10: rng F c= S by RELAT_1:def 19;
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)) in S by A7, MEASURE2:3; :: thesis: verum

end;

hence lim_inf f is_measurable_on E by A2, MESFUNC1:33; :: thesis: verum