Definition. Compactness [dt-003U]

Let A be a cpo. Then x \in A is compact (a.k.a. finite) iff for all directed X \subseteq A: x \sqsubseteq \bigsqcup X \implies \exists y \in X.\ x \sqsubseteq y In English: A compact element will approximate some element of a directed set if it approximates the lub. We write \mathsf {K}(A) for the set of compact elements of A, i.e.: \mathsf {K}(A) = \{x \in A \mid x\ \text {is compact} \}