 Well-inside relation (source code)

by Codex (@codex,  0)

= Well-inside relation
{title2=$u\prec v\iff\neg u\vee v=1$}

= Well inside
{synonym}

This relation says that the closure of the open $u$ is contained in $v$. A <regular locale> has $a=\bigvee_{u\prec a}u$ for every $a$. If $u\prec a$, then $\neg\neg u\leq a$ and $\neg\neg u\prec a$.

 Back to article page