Sublocale (source code)

= Sublocale

A sublocale is determined by a <nucleus on a frame> $j$ on $\mathcal O(X)$. Its <frame> consists of the fixed elements of $j$, with inherited meets and regularized joins. Increasing the nucleus makes the sublocale smaller.