:: deftheorem Def8869 defines Sigma_tauhelp2 FINANCE5:def 9 :
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
for A1 being SetSequence of Omega st rng A1 c= { A where A is Element of Sigma : for t2 being Element of I holds A /\ { w where w is Element of Omega : tau . w <= t2 } in MyFunc . t2 } holds
for t being Element of I
for n being Nat holds Sigma_tauhelp2 (tau,A1,n,t) = ((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } ;