:: Set Sequences and Monotone Class :: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura :: :: Received August 12, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users
begin
Lm1:
for t, p, s being realnumber st 0< s & t <= p holds ( t < p + s & t - s < p )
for n being Nat for Omega being non emptyset for Sigma being SigmaField of Omega for ASeq, BSeq being SetSequence of Sigma for P being Probability of Sigma st ASeq . n c= BSeq . n holds (P * ASeq). n <=(P * BSeq). n
for X being set for Si being SigmaField of X for FSi being FinSequence of Si ex ASeq being SetSequence of Si st ( ( for k being Nat st k indom FSi holds ASeq . k = FSi . k ) & ( for k being Nat st not k indom FSi holds ASeq . k ={} ) )