exists_mem_eq_inf — Mathlib

English

Let α be a linear order with a top element, S be a nonempty finite subset of ι, and f : ι → α. Then there exists an index i ∈ S with s.inf f = f(i); i.e., the minimal value of f on S is attained at some i in S.

Русский

Пусть α — линейный порядок с верхней границей, S — ненужное конечное подмножество ι, и f : ι → α. Тогда существует i ∈ S такое, что s.inf f = f(i); то есть минимум значений f на S достигается в некотором i ∈ S.

LaTeX

$$$\\exists i \\in s,\\ s.\\inf f = f(i).$$$

Lean4

theorem exists_mem_eq_inf [OrderTop α] (s : Finset ι) (h : s.Nonempty) (f : ι → α) : ∃ i, i ∈ s ∧ s.inf f = f i :=
  exists_mem_eq_sup (α := αᵒᵈ) s h f

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