Theorems · Theorem · order theory

Finset.le_inf_of_directed_le

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

Defined in

Mathlib.Data.Finset.Lattice.Fold

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemilatticeInfOrderTop