argmin_concat — Mathlib

English

NotMemFoldlArgAux: (duplicate style) If a ∈ l and m ∈ foldl(argAux r) o l, then not r a m.

Русский

NotMemFoldlArgAux: если a ∈ l и m ∈ foldl(argAux r) o l, то не r a m.

LaTeX

$$$ a \in l \to m \in \operatorname{foldl}(\operatorname{argAux}(r), o, l) \to \neg r\ a\ m $$$

Lean4

theorem argmin_concat (f : α → β) (a : α) (l : List α) :
    argmin f (l ++ [a]) = Option.casesOn (argmin f l) (some a) fun c => if f a < f c then some a else some c :=
  @argmax_concat _ βᵒᵈ _ _ _ _ _

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