:: deftheorem defines is_StoppingTime_wrt FINANCE5:def 7 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for r being Real
for I being TheEvent of r
for MyFunc being Function
for k being random_variable of Sigma, BorelSubsets I holds
( k is_StoppingTime_wrt MyFunc iff for t being Element of I holds { w where w is Element of Omega : k . w <= t } in MyFunc . t );