:: deftheorem Def2000 defines Filtration FINANCE3:def 9 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for I being non empty real-membered set
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) );