:: deftheorem Def2000 defines Filtration FINANCE3:def 10 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for I being non empty Subset of REAL
for b₄ being ManySortedSigmaField of I,Sigma holds
( b₄ is Filtration of I,Sigma iff ( ( for s, t being Element of I st s <= t holds
b₄ . s is Subset of (b₄ . t) ) & ( for t being Element of I holds b₄ . t c= Sigma ) ) );