Module docstring
{"# Finsets of ordered types "}
Directed.finset_le
theorem
{r : α → α → Prop} [IsTrans α r] {ι} [hι : Nonempty ι] {f : ι → α} (D : Directed r f) (s : Finset ι) :
∃ z, ∀ i ∈ s, r (f i) (f z)
Full source
theorem Directed.finset_le {r : α → α → Prop} [IsTrans α r] {ι} [hι : Nonempty ι] {f : ι → α}
(D : Directed r f) (s : Finset ι) : ∃ z, ∀ i ∈ s, r (f i) (f z) :=
show ∃ z, ∀ i ∈ s.1, r (f i) (f z) from
Multiset.induction_on s.1 (let ⟨z⟩ := hι; ⟨z, fun _ ↦ by simp⟩)
fun i _ ⟨j, H⟩ ↦
let ⟨k, h₁, h₂⟩ := D i j
⟨k, fun _ h ↦ (Multiset.mem_cons.1 h).casesOn (fun h ↦ h.symm ▸ h₁)
fun h ↦ _root_.trans (H _ h) h₂⟩Informal description
Let $\alpha$ be a type equipped with a transitive relation $r$, and let $\iota$ be a nonempty type. Given a directed family of elements $f \colon \iota \to \alpha$ (with respect to $r$) and a finite subset $s \subseteq \iota$, there exists an index $z \in \iota$ such that for every $i \in s$, the relation $f(i) \preccurlyeq f(z)$ holds.
Finset.exists_le
theorem
[Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)] (s : Finset α) : ∃ M, ∀ i ∈ s, i ≤ M
Full source
theorem Finset.exists_le [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)] (s : Finset α) :
∃ M, ∀ i ∈ s, i ≤ M :=
directed_id.finset_le _Informal description
Let $\alpha$ be a nonempty type equipped with a preorder $\leq$ such that $\alpha$ is directed with respect to $\leq$. For any finite subset $s \subseteq \alpha$, there exists an element $M \in \alpha$ such that $i \leq M$ for all $i \in s$.