mathlib3 documentation

data.finset.order

Finsets of ordered types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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)
theorem finset.exists_le {α : Type u} [nonempty α] [preorder α] [is_directed α has_le.le] (s : finset α) :
(M : α), (i : α), i s i M