let Omega be non empty set ; 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; 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; for r being Real st F is Real-Valued-Random-Variable of Sigma holds
F " ].-infty,r.[ in Sigma
let r be Real; ( F is Real-Valued-Random-Variable of Sigma implies F " ].-infty,r.[ in Sigma )
assume
F is Real-Valued-Random-Variable of Sigma
; 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 ;
( z in F " ].-infty,r.[ iff z in ([#] Sigma) /\ (less_dom (F,r)) )
assume
z in ([#] Sigma) /\ (less_dom (F,r))
;
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;
verum
end;
hence
F " ].-infty,r.[ in Sigma
by A2, TARSKI:2; verum