English
Let α be a preorder and f: ι → α. If s ⊆ ι is such that (f''s) is finite and s ≠ ∅, then there exists i ∈ ι with f i ∈ s and f i is maximal among {f j | j ∈ s}. In other words, there is an index whose image is maximal among the image of s.
Русский
Пусть α — предордер и f: ι → α. Пусть s ⊆ ι таково, что (f''s) конечно и s непусто; тогда существует i ∈ ι such that f i ∈ s и f i максимален среди {f j | j ∈ s}. Иными словами, существует индекс, чье изображение является максимальным по образу 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
theorem exists_maximalFor (f : ι → α) (s : Set ι) (h : s.Finite) (hs : s.Nonempty) : ∃ i, MaximalFor (· ∈ s) f i := by
lift s to Finset ι using h; exact s.exists_maximalFor f hs
