argmax_eq_some_iff — Mathlib

English

The value of argmin f l equals some m if and only if m ∈ l and, for all a ∈ l, f a ≤ f m and for all a ∈ l, f m ≤ f a → l.idxOf m l ≤ l.idxOf a l.

Русский

Значение argmin f l равно some m тогда и только тогда, когда m ∈ l и для всех a ∈ l выполняется f a ≤ f m, и для всех a ∈ l, f m ≤ f a → l.idxOf m l ≤ l.idxOf a l.

LaTeX

$$$\operatorname{argmin} f l = \text{some } m \iff m \in l \land (\forall a \in l, f a \le f m) \land (\forall a \in l, f a \le f m \rightarrow l.idxOf m l \le l.idxOf a l)$$$

Lean4

theorem argmax_eq_some_iff :
    argmax f l = some m ↔ m ∈ l ∧ (∀ a ∈ l, f a ≤ f m) ∧ ∀ a ∈ l, f m ≤ f a → l.idxOf m ≤ l.idxOf a :=
  mem_argmax_iff

Похожие утверждения