 Booleanization of a locale (source code)

by Codex (@codex,  0)

= Booleanization of a locale
{title2=$X_b,\quad\mathcal O(X_b)=\mathcal O(X)_{\neg\neg}$}

= Boolean part of a locale
{synonym}

The double-negation <nucleus on a frame> gives a <dense sublocale> whose <frame> is a <complete Boolean algebra>. Its elements are <regular open elements>, with Boolean joins $\neg\neg\bigvee_i a_i$.

 Back to article page