Category:Locales

From ProofWiki
Jump to navigation Jump to search

This category contains results about Locales.
Definitions specific to this category can be found in Definitions/Locales.

An object of $\mathbf{Loc}$ is called a locale.


That is, a locale is a complete lattice $\struct {L, \preceq}$ satisfying the infinite join distributive law:

  \(\ds \forall a \in L, S \subseteq L:\) \(\ds a \wedge \bigvee S = \bigvee \set {a \wedge s : S \in S} \)      

where $\bigvee S$ denotes the supremum $\sup S$.