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