English
Let α be a preorder and s ⊆ α a nonempty finite set. For every index set ι and every function f: ι → α, there exists i ∈ ι such that f(i) ∈ s and f(i) is minimal among {f(j) | f(j) ∈ s}. In other words, there is an index whose image lies in s and attains the minimum value (within s) of the function f.
Русский
Пусть α — предпорядок и s ⊆ α — непустое конечное множество. Для любого множества индексов ι и любой функции f: ι → α существует элемент i ∈ ι такой, что f(i) ∈ s и значение f(i) минимально среди всех f(j), если f(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
theorem exists_minimalFor (f : ι → α) (s : Finset ι) (hs : s.Nonempty) : ∃ i, MinimalFor (· ∈ s) f i :=
exists_maximalFor (α := αᵒᵈ) f s hs
