:: deftheorem defines set_of_constant_RV FINANCE6:def 3 :
for Omega being non empty set
for F being SigmaField of Omega holds set_of_constant_RV F = { f where f is Function of Omega,REAL : ( f is random_variable of F, Borel_Sets & f is constant ) } ;