:: deftheorem Def20 defines max FINANCE4:def 6 :
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₅ = max (k1,k2) iff for w being Element of Omega holds b₅ . w = max ((k1 . w),(k2 . w)) );