English
Let r be a transitive relation on α and f a function from γ to α, with γ nonempty. If D is a directed family (r, f), then for every finite subset s of γ there exists an index z such that f(i) ≤ f(z) for all i in s (i.e., r(f(i), f(z)) holds for all i ∈ s).
Русский
Пусть r — переходящее отношение на α и f: γ → α, причём γ непустое. Если существует направленная семейство (r, f), то для любого конечного подмножества s ⊆ γ существует z ∈ γ такое, что f(i) ≤ f(z) для всех i ∈ s (то есть r(f(i), f(z)) выполняется для всех i ∈ s).
LaTeX
$$$\\\\exists z \\\\in \\\\\\gamma \\\\text{ such that } \u2203 z, \\\\forall i \\\\in s, \\\\ r(f(i), f(z)).$$$
Lean4
theorem finite_set_le (D : Directed r f) {s : Set γ} (hs : s.Finite) : ∃ z, ∀ i ∈ s, r (f i) (f z) := by
convert D.finset_le hs.toFinset using 3; rw [Set.Finite.mem_toFinset]
