English
Let l be a list and m a fixed element. The statement argmin f l = some m holds exactly when m ∈ l and the three conditions described for argmin_iff hold: m is in l, and f values are bounded by f m from both sides with respect to l.
Русский
Пусть список l и элемент m. Утверждение argmin f l = some m эквивалентно тому, что m ∈ l и выполняются три условия, описанные в равенстве argmin_iff: m ∈ l, а значения f ограничены слева и справа относительно f m.
LaTeX
$$$\operatorname{argmin} f l = \text{some } m \iff m \in l \land (\forall a \in l, f m \le f a) \land (\forall a \in l, f a \le f m \rightarrow l.idxOf m l \le l.idxOf a l)$$$
Lean4
theorem argmin_eq_some_iff :
argmin f l = some m ↔ m ∈ l ∧ (∀ a ∈ l, f m ≤ f a) ∧ ∀ a ∈ l, f a ≤ f m → l.idxOf m ≤ l.idxOf a :=
mem_argmin_iff
