Finsets of ordered types

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

theorem Finset.exists_le {α : Type u} [Nonempty α] [Preorder α] [IsDirected α fun x x_1 => x ≤ x_1] (s : Finset α) : ∃ M, ∀ (i : α), i ∈ s → i ≤ M