argmin_le

Mathlib.Order.WellFounded

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

English

For any a, f(argmin f) ≤ f(a).

Русский

Для любого a выполнено f(argmin f) ≤ f(a).

LaTeX

$$$\\forall a\\, [Nonempty \\;\\alpha],\\; f(\\mathrm{argmin}\\; f) \\le f(a)$$$

Lean4

theorem argmin_le (a : α) [Nonempty α] : f (argmin f) ≤ f a :=
  not_lt.mp <| not_lt_argmin f a

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

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

Разделы

Аффилиация

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