Directed.finset_le

theorem Directed.finset_le : ∀ {α : Type u} {r : α → α → Prop} [inst : IsTrans α r] {ι : Type u_1} [hι : Nonempty ι] {f : ι → α}, Directed r f → ∀ (s : Finset ι), ∃ z, ∀ i ∈ s, r (f i) (f z)

This theorem, `Directed.finset_le`, states that for any type `α`, a relation `r` on `α` which is transitive, a type `ι` that is nonempty, and a function `f` mapping elements of `ι` to `α`, if the function `f` is directed with respect to the relation `r`, then for any finite set `s` of elements of type `ι`, there exists an element `z` such that for every element `i` in the finite set `s`, the relation `r` holds between the image of `i` under `f` and the image of `z` under `f`. In other words, the function `f` has an element `z` that is `r`-above all elements of the finite set `s`.

More concisely: For any transitive relation `r` on type `α`, function `f` mapping a nonempty `ι` to `α`, and finite set `s` of elements from `ι`, if `f` is directed with respect to `r`, then there exists an element `z` in `α` such that `r(fi, z)` holds for all `i` in `s`.