English
Let f: ι → α and s ⊆ ι be nonempty with (f '' s) finite. Then there exists i ∈ ι such that f i ∈ s and f i is minimal among {f j | j ∈ s}. This is the dual of the previous statement.
Русский
Пусть 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(i) \le f(j).$$$
Lean4
/-- A version of `Finite.exists_minimalFor` with the (weaker) hypothesis that the image of `s`
is finite rather than `s` itself. -/
theorem exists_minimalFor' (f : ι → α) (s : Set ι) (h : (f '' s).Finite) (hs : s.Nonempty) :
∃ i, MinimalFor (· ∈ s) f i :=
h.exists_maximalFor' (α := αᵒᵈ) f s hs
