:: deftheorem Def10 defines Argmin GRAPHSP:def 10 :
for X being finite Subset of NAT
for f being Element of REAL *
for n, b₄ being Nat holds
( b₄ = Argmin (X,f,n) iff ( ( X <> {} implies ex i being Nat st
( i = b₄ & i in X & ( for k being Nat st k in X holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) ) & ( X = {} implies b₄ = 0 ) ) );