let X be non empty set ; :: thesis: for S being SigmaField of X

for f being with_the_same_dom Functional_Sequence of X,REAL

for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) holds

lim_inf f is E -measurable

let S be SigmaField of X; :: thesis: for f being with_the_same_dom Functional_Sequence of X,REAL

for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) holds

lim_inf f is E -measurable

let f be with_the_same_dom Functional_Sequence of X,REAL; :: thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) holds

lim_inf f is E -measurable

let E be Element of S; :: thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) implies lim_inf f is E -measurable )

assume that

A1: dom (f . 0) = E and

A2: for n being Nat holds f . n is E -measurable ; :: thesis: lim_inf f is E -measurable

for n being Nat holds (R_EAL f) . n is E -measurable

for f being with_the_same_dom Functional_Sequence of X,REAL

for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) holds

lim_inf f is E -measurable

let S be SigmaField of X; :: thesis: for f being with_the_same_dom Functional_Sequence of X,REAL

for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) holds

lim_inf f is E -measurable

let f be with_the_same_dom Functional_Sequence of X,REAL; :: thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) holds

lim_inf f is E -measurable

let E be Element of S; :: thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is E -measurable ) implies lim_inf f is E -measurable )

assume that

A1: dom (f . 0) = E and

A2: for n being Nat holds f . n is E -measurable ; :: thesis: lim_inf f is E -measurable

for n being Nat holds (R_EAL f) . n is E -measurable

proof

hence
lim_inf f is E -measurable
by A1, MESFUNC8:24; :: thesis: verum
let n be Nat; :: thesis: (R_EAL f) . n is E -measurable

f . n is E -measurable by A2;

hence (R_EAL f) . n is E -measurable by Th7; :: thesis: verum

end;f . n is E -measurable by A2;

hence (R_EAL f) . n is E -measurable by Th7; :: thesis: verum