Documentation

Mathlib.Data.Finset.Order

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 : ι), is, r (f i) (f z)
theorem Finset.exists_le {α : Type u} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (s : Finset α) :
∃ (M : α), is, i M