:: deftheorem defines Sigma_tau FINANCE5:def 23 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for S being non empty Subset of REAL
for MyFunc being Filtration of S,Sigma
for tau being StoppingTime_Func of Sigma,MyFunc holds Sigma_tau (MyFunc,tau) = { A where A is Element of Sigma : for t being Element of S holds A /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t } ;