Nice description of the Heyting implication for clopen upsets By the Priestley duality, we know that a lattice can be represented as the clopen upsets of its prime filters space $X$, namely via the map
$$ \eta: a \in L \longmapsto \lbrace x \in X \mid x \ni a \rbrace. $$
Now, Pultr and Sichler gave a characterisation of the Priestley spaces which were dual to a frame (the adherence of an open upset must be an open upset). In particular, every frame is a Heyting algebra with the implication defined as
$$ a \rightarrow b = \bigvee \lbrace c \mid a \wedge c \leq b \rbrace. $$
Now my question is: is there a nice description of $\eta(a\rightarrow b)$ in terms of $\eta(a)$ and $\eta(b)$ ?
 A: Yes there is:
$$
\eta(a \to b) = X - \downarrow(\eta(a) - \eta(b)),
$$
where $\downarrow A$ for $A \subseteq X$ means the downward closure of $A$.
Let us prove this. First note that a prime filter $F$ is in $X - \downarrow(\eta(a) - \eta(b))$ if and only if there is no prime filter $F' \supseteq F$ such that $a \in F'$ while $b \not \in F'$. Or put differently: for every prime filter $F' \supseteq F$ we have that $a \in F'$ implies $b \in F'$. We will show that this happens if and only if $a \to b \in F$.
If $a \to b \in F$ and $F' \supseteq F$ with $a \in F'$ then $a \wedge (a \to b) \in F'$. As $a \wedge (a \to b) = a \wedge b \leq b$, we conclude that $b \in F'$, as required.
For the other direction, we consider
$$
F' = \{ d : c \wedge a \leq d \text{ for some } c \in F \}.
$$
So either $F'$ is the entire lattice or $F'$ is the prime filter generated by $F \cup \{a\}$. Either way we have $b \in F'$. So $a \wedge c \leq b$ for some $c \in F$ and hence $c \leq a \to b$. Since $F$ is a filter we conclude that indeed $a \to b \in F$.
