Definition:Compact Regular Locale

Definition

Let $L = \struct {S, \preceq}$ be a locale.

Then $L$ is said to be a compact regular locale if and only if $L$ is both a regular locale and a compact locale.

That is, $L$ is a compact regular locale if and only if:

$(1) \quad$ the greatest element $\top$ is a compact element

$(2) \quad$ $\forall a \in S : a = \sup \set {b \in S : b \eqslantless a}$

where $\eqslantless$ is the well inside relation on $L$.

Sources

• 1982: Peter T. Johnstone: Stone Spaces: Chapter $\text {III}$: Compact Hausdorff Spaces, $\S1.8$