mathlib documentation

data.finset.order

Finsets of ordered types

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 sr (f i) (f z)

theorem finset.exists_le {α : Type u} [nonempty α] [directed_order α] (s : finset α) :
∃ (M : α), ∀ (i : α), i si M