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 ∈ s, r (f i) (f z)

theorem Finset.exists_le {α : Type u} [Nonempty α] [Preorder α] [IsDirectedOrder α] (s : Finset α) : ∃ (M : α), ∀ i ∈ s, i ≤ M

theorem Finset.exists_ge {α : Type u} [Nonempty α] [Preorder α] [IsCodirectedOrder α] (s : Finset α) : ∃ (M : α), ∀ i ∈ s, M ≤ i