Theorems · Theorem · order theory

Finset.sup_le_of_le_directed

∀ {α : Type u_7} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Set α),
  s.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) s → ∀ (t : Finset α), (∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x

Defined in

Mathlib.Data.Finset.Lattice.Fold

Cited by

2 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemilatticeSupOrderBot