Finsets of ordered types #

source

theorem directed.finset_le {α : Type u} {r : α → α → Prop} [is_trans α r] {ι : Type u_1} [hι : nonempty ι] {f : ι → α} (D : directed r f) (s : finset ι) :

∃ (z : ι), ∀ (i : ι), i ∈ s → r (f i) (f z)

source

theorem finset.exists_le {α : Type u} [nonempty α] [preorder α] [is_directed α has_le.le] (s : finset α) :

∃ (M : α), ∀ (i : α), i ∈ s → i ≤ M