:: deftheorem Def2 defines min_p MEASUR12:def 2 :
for f being FinSequence of ExtREAL
for b₂ being Nat holds
( b₂ = min_p f iff ( ( len f = 0 implies b₂ = 0 ) & ( len f > 0 implies ( b₂ in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b₂ holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b₂ holds
b₂ <= j ) ) ) ) );