A directed family in a well-founded meet-semilattice attains its bound

In a complete meet-semilattice whose strict order is well founded, a nonempty downward-directed family of elements contains its own infimum: a minimal member of the family is below every other member, by directedness, so it is the infimum.

Mathlib's nearest statement is CompleteLattice.IsSupClosedCompact, which concludes sSup s ∈ s from WellFoundedGT for a set closed under binary suprema. It is phrased for sup-closed sets, so it does not directly cover an arbitrary directed family — a chain is directed but rarely closed — and a directed family is what a descending filtration supplies.

Main results

• Directed.exists_eq_iInf: a nonempty downward-directed family in a complete meet-semilattice with WellFoundedLT attains its infimum.

theorem Directed.exists_eq_iInf {α : Type u_1} [CompleteSemilatticeInf α] [WellFoundedLT α] {ι : Sort u_2} [Nonempty ι] {f : ι → α} (hf : Directed (fun (x1 x2 : α) => x1 ≥ x2) f) : ∃ (i : ι), f i = ⨅ (j : ι), f j

A nonempty downward-directed family in a well-founded complete meet-semilattice attains its infimum.

Only arbitrary infima are used, so CompleteSemilatticeInf is the natural hypothesis; a complete lattice is the case of interest.

Nonemptiness of the index is needed: over an empty index the infimum is the greatest element and no member attains it.