argmin_mem

Mathlib.Data.List.MinMax

URI: https://scilib.ai/kg/mathlib#List.argmin_mem

English

If m ∈ argmin f l, then m ∈ l.

Русский

Если m ∈ argmin f l, то m ∈ l.

LaTeX

$$$ m \in \operatorname{argmin} f l \Rightarrow m \in l $$$

Lean4

theorem argmin_mem : ∀ {l : List α} {m : α}, m ∈ argmin f l → m ∈ l :=
  @argmax_mem _ βᵒᵈ _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru