let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for F being Function of Omega,REAL
for r being Real st F is Real-Valued-Random-Variable of Sigma holds
F " ].-infty,r.[ in Sigma
let Sigma be SigmaField of Omega; :: thesis: for F being Function of Omega,REAL
for r being Real st F is Real-Valued-Random-Variable of Sigma holds
F " ].-infty,r.[ in Sigma
let F be Function of Omega,REAL; :: thesis: for r being Real st F is Real-Valued-Random-Variable of Sigma holds
F " ].-infty,r.[ in Sigma
let r be Real; :: thesis: ( F is Real-Valued-Random-Variable of Sigma implies F " ].-infty,r.[ in Sigma )
assume F is Real-Valued-Random-Variable of Sigma ; :: thesis: F " ].-infty,r.[ in Sigma
then F is [#] Sigma -measurable ;
then A2: ([#] Sigma) /\ (less_dom (F,r)) in Sigma by MESFUNC6:12;
for z being object holds
( z in F " ].-infty,r.[ iff z in ([#] Sigma) /\ (less_dom (F,r)) )
proof
let z be object ; :: thesis: ( z in F " ].-infty,r.[ iff z in ([#] Sigma) /\ (less_dom (F,r)) )
hereby :: thesis: ( z in ([#] Sigma) /\ (less_dom (F,r)) implies z in F " ].-infty,r.[ )
assume A3: z in F " ].-infty,r.[ ; :: thesis: z in ([#] Sigma) /\ (less_dom (F,r))
then A4: ( z in dom F & F . z in ].-infty,r.[ ) by FUNCT_1:def 7;
then F . z in { p where p is Real : ( -infty < p & p < r ) } by RCOMP_1:def 2;
then consider w being Real such that
A5: ( F . z = w & -infty < w & w < r ) ;
z in less_dom (F,r) by A4, A5, MESFUNC1:def 11;
hence z in ([#] Sigma) /\ (less_dom (F,r)) by A3, XBOOLE_0:def 4; :: thesis: verum
end;
assume z in ([#] Sigma) /\ (less_dom (F,r)) ; :: thesis: z in F " ].-infty,r.[
then A6: ( z in [#] Sigma & z in less_dom (F,r) ) by XBOOLE_0:def 4;
then A7: ( z in dom F & F . z < r ) by MESFUNC1:def 11;
( -infty < F . z & F . z < r ) by XXREAL_0:12, FUNCT_2:5, MESFUNC1:def 11, A6;
then F . z in { p where p is Real : ( -infty < p & p < r ) } ;
then F . z in ].-infty,r.[ by RCOMP_1:def 2;
hence z in F " ].-infty,r.[ by A7, FUNCT_1:def 7; :: thesis: verum
end;
hence F " ].-infty,r.[ in Sigma by A2, TARSKI:2; :: thesis: verum