English
For the dual order βᵒᵈ, the argmin statements mirror the argmax statements with reversed inequalities. In particular, m ∈ argmin f l iff 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.
Русский
Для двойственного порядка βᵒᵈ утверждения об аргмин повторяются зеркально относительно аргмакса: m ∈ argmin f l тогда и только тогда, когда m ∈ l, и для всех a ∈ l справедливо f a ≥ f m, а для всех a ∈ l, если f m ≥ f a, то l.idxOf m l ≤ l.idxOf a l.
LaTeX
$$$\forall {l\, m}, m \in \operatorname{argmin} f l \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 mem_argmin_iff : m ∈ argmin f l ↔ m ∈ l ∧ (∀ a ∈ l, f m ≤ f a) ∧ ∀ a ∈ l, f a ≤ f m → l.idxOf m ≤ l.idxOf a :=
@mem_argmax_iff _ βᵒᵈ _ _ _ _ _
