:: deftheorem Def21 defines min FINANCE4:def 7 :
for Omega being non empty set
for T being Nat
for k1, k2 being Function of Omega,(StoppingSetExt T)
for b₅ being Function of Omega,ExtREAL holds
( b₅ = min (k1,k2) iff for w being Element of Omega holds b₅ . w = min ((k1 . w),(k2 . w)) );