English
Let α be a linear order, S be a nonempty finite subset of ι, and f : ι → α. Then there exists i ∈ S such that sup' S f = f(i); i.e., the maximum value of f on S is attained at some i in S.
Русский
Пусть α — линейный порядок, S — ненулевое конечное подмножество множества ι, и f : ι → α. Тогда существует i ∈ S такое, что sup' S f = f(i); то есть максимум значений f на S достигается в некотором i ∈ S.
LaTeX
$$$\\exists i \\in s,\\ \\max_{j \\in s} f(j) = f(i).$$$
Lean4
theorem exists_mem_eq_sup' (f : ι → α) : ∃ i, i ∈ s ∧ s.sup' H f = f i := by
induction H using Finset.Nonempty.cons_induction with
| singleton c => exact ⟨c, mem_singleton_self c, rfl⟩
| cons c s hcs hs ih =>
rcases ih with ⟨b, hb, h'⟩
rw [sup'_cons hs, h']
cases le_total (f b) (f c) with
| inl h => exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
| inr h => exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩
