English
Let s be a nonempty finite set and f: β → α with α linearly ordered. There exists y ∈ s such that f(y) is maximal among {f(x) : x ∈ s}. Moreover, for any x' ∈ s, f(x') ≤ f(y).
Русский
Пусть s — непустое конечное множество и f: β → α отображена в линейно упорядоченную α. Существует y ∈ s, такое что f(y) максимален на {f(x) : x ∈ s}, и для любого x' ∈ s выполняется f(x') ≤ f(y).
LaTeX
$$$\\exists y \\in s, \\forall x' \\in s, f(x') \\le f(y)$$$
Lean4
theorem exists_max_image (s : Finset β) (f : β → α) (h : s.Nonempty) : ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x :=
by
obtain ⟨y, hy⟩ := max_of_nonempty (h.image f)
rcases mem_image.mp (mem_of_max hy) with ⟨x, hx, rfl⟩
exact ⟨x, hx, fun x' hx' => le_max_of_eq (mem_image_of_mem f hx') hy⟩
