:: deftheorem Def30 defines Put-Option FINANCE6:def 1 :
for Omega being non empty set
for F being SigmaField of Omega
for RV being random_variable of F, Borel_Sets
for K being Real
for b₅ being Function of Omega,REAL holds
( b₅ = Put-Option (RV,K) iff for w being Element of Omega holds
( ( ((Omega --> K) - RV) . w >= 0 implies b₅ . w = ((Omega --> K) - RV) . w ) & ( ((Omega --> K) - RV) . w < 0 implies b₅ . w = 0 ) ) );