English
Let f: ι → α and s ⊆ ι be nonempty with (f '' s) finite. Then there exists i ∈ ι such that f i ∈ s and f i is maximal among {f j | j ∈ s}. This is a version where the maximality is determined by the finite image.
Русский
Пусть f: ι → α и s ⊆ ι непусто, причём (f '' s) конечно. Тогда существует i ∈ ι такое, что f i ∈ s и f i максимален среди {f j | j ∈ s}. Это версия, где отображение образа задаёт максимум.
LaTeX
$$$\exists i \in \iota,\ f(i) \in s \wedge \forall j \in \iota,\ f(j) \in s \rightarrow f(j) \le f(i).$$$
Lean4
/-- A version of `Finite.exists_maximalFor` with the (weaker) hypothesis that the image of `s`
is finite rather than `s` itself. -/
theorem exists_maximalFor' (f : ι → α) (s : Set ι) (h : (f '' s).Finite) (hs : s.Nonempty) :
∃ i, MaximalFor (· ∈ s) f i :=
by
obtain ⟨_, ⟨a, ha, rfl⟩, hmax⟩ := Finite.exists_maximalFor id (f '' s) h (hs.image f)
exact ⟨a, ha, fun a' ha' hf ↦ hmax (mem_image_of_mem f ha') hf⟩
