Theorems · Theorem · order theory

CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le

∀ (α : Type u_2) [inst : CompleteLattice α] (k : α),
  IsCompactElement k ↔ ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

An element k is compact if and only if any directed set with sSup above k already got above k at some point in the set.

Defined in

Mathlib.Order.CompactlyGenerated.Basic

Cited by

6 results in Mathlib

Foundations

Depth 10 from the axioms · uses propext

Assumes

CompleteLattice