exists_mem_eq_sup — Mathlib

English

Let α be a linear order with a bottom element, S be a nonempty finite subset of ι, and f : ι → α. Then there exists i ∈ S such that s.sup f = f(i); i.e., the maximal value of f on S is attained at some i in S.

Русский

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

LaTeX

$$$\\exists i \\in s,\\ s^{\\!\\uparrow} f = f(i).$$$

Lean4

theorem exists_mem_eq_sup [OrderBot α] (s : Finset ι) (h : s.Nonempty) (f : ι → α) : ∃ i, i ∈ s ∧ s.sup f = f i :=
  sup'_eq_sup h f ▸ exists_mem_eq_sup' h f

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