let Omega be non empty set ; for Sigma being SigmaField of Omega
for T being Nat
for MyFunc being Filtration of StoppingSet T,Sigma
for k being Function of Omega,(StoppingSetExt T) holds
( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )
let Sigma be SigmaField of Omega; for T being Nat
for MyFunc being Filtration of StoppingSet T,Sigma
for k being Function of Omega,(StoppingSetExt T) holds
( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )
let T be Nat; for MyFunc being Filtration of StoppingSet T,Sigma
for k being Function of Omega,(StoppingSetExt T) holds
( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )
let MyFunc be Filtration of StoppingSet T,Sigma; for k being Function of Omega,(StoppingSetExt T) holds
( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )
let k be Function of Omega,(StoppingSetExt T); ( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )
thus
( k is_StoppingTime_wrt MyFunc,T implies for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )
( ( for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t ) implies k is_StoppingTime_wrt MyFunc,T )
assume ASSJ1:
for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t
; k is_StoppingTime_wrt MyFunc,T
for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w = t } in MyFunc . t
hence
k is_StoppingTime_wrt MyFunc,T
; verum