:: deftheorem defines Sigma_tau FINANCE5:def 11 :
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 Filtration of I,Sigma
for tau being StoppingTime_Func of MyFunc holds Sigma_tau tau = { A where A is Element of Sigma : for t being Element of I holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t } ;