Heyting implication (source code)

= Heyting implication
{c}
{title2=$a\to b$}

In a <Heyting algebra>, $a\to b$ is the greatest $x$ with $x\wedge a\leq b$. Thus $x\leq a\to b$ if and only if $x\wedge a\leq b$. Every <frame> has this operation, obtained by taking the join of all such $x$. The <open nucleus> attached to $a$ is $x\mapsto a\to x$.