Proving that the pointful and the pointless forms of the well-inside relation coincide

Question

In Stone Spaces by Johnstone, a pointless version of the well-inside order is given:

Definition 1. Let $L$ be a locale and let $x, y \in L$. $x$ is said to be well-inside $y$ iff \begin{equation*} x \eqslantless y \quad:=\quad \exists z \in L.\; x \wedge z = \bot \;\text{and}\; y \vee z = \top. \end{equation*}

My understanding of Johstone is that this is a pointless manifestation of the following relation we can define on topological spaces (as pointed by Johnstone on pg. 80 of Stone Spaces).

Definition 2. Let $X$ be a topological space and let $U, V \in \Omega(X)$. $U$ is well-inside $V$ iff $\mathsf{Clos}(U) \subseteq V$ (where $\mathsf{Clos}$ denotes the usual closure of a set).

Proposition. Let $X$ be a topological space and let $U, V \in \Omega(X)$. $U$ is well-inside $V$ (by Defn. 2) iff $U \eqslantless V$ with respect to the locale $\Omega(X)$ of open sets of $X$ (Defn. 1).

Johnstone says that this is a direct consequence of the fact that $x \eqslantless y$ iff $\neg x \vee y = \top$ in any Heyting algebra and that $\neg U$ is the interior of the complement of $U$. I don't understand this and the validity of this proposition is not apparent to me. Can someone please a provide a proof for this claim?

Answer 1

Suppose $U$ is well-inside $V$ by Definition 2. Let $W = X\setminus\text{Clos}(U)$, the complement of the closure of $U$. We have $U\subseteq \text{Clos}(U)\subseteq V$, so $\emptyset \subseteq U\cap W \subseteq \text{Clos}(U) \cap W = \emptyset$, and $X\supseteq V\cup W \supseteq \text{Clos}(U)\cup W = X$. Thus $U$ is well-inside $V$ by Definition 1.

Conversely, suppose $U$ is well-inside $V$ by Definition 1. Then there is some open set $W$ such that $U\cap W = \emptyset$ and $V\cup W = X$. Let $C = X\setminus W$, and note that $C$ is closed. Since $U\cap W = \emptyset$ and $V\cup W = X$, we have $U\subseteq C\subseteq V$. Since $C$ is a closed set containing $U$, $\text{Clos}(U)\subseteq C\subseteq V$, so $U$ is well-inside $V$ by Definition 2.

---

That was a direct proof - it's worthwhile understanding Johnstone's comment, though. It breaks down into the following pieces:

1. In any Heyting algebra (and thus in any locale), $x$ is well-inside $y$ (Definition 1) if and only if $\lnot x\vee y = \top$.
2. In the locale of open sets in a topological space, $\lnot U$ is the interior of the complement of $U$ (which is equal to the complement of the closure of $U$).
3. Thus, $U$ is well-inside $V$ by Definition 1 iff $\lnot U \cup V = X$ iff $\text{Clos}(U)\subseteq V$ iff $U$ is well-inside $V$ by Definition 2.

The first two points are rather important facts - which are worth spending some time to internalize if you haven't already - and the third point is an easy verification.