argminOn_mem

Mathlib.Order.WellFounded

URI: https://scilib.ai/kg/mathlib#Function.argminOn_mem

English

For any nonempty subset s of α, the argminOn f s hs lies in s.

Русский

Для любого непустого подмножества s пространства α, минимальный аргумент argminOn принадлежит s.

LaTeX

$$$\\forall s,\\; s.Nonempty \\Rightarrow s\\ni\\text{argminOn } f\\; s\\; hs$$$

Lean4

@[simp]
theorem argminOn_mem (s : Set α) (hs : s.Nonempty) : argminOn f s hs ∈ s :=
  WellFounded.min_mem _ _ _

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

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

Разделы

Аффилиация

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