# Proving every totally ordered and bounded lattice set is a Heyting Algebra

I am trying to prove that given some bounded lattice $(L, \vee, \wedge, \top, \bot)$, where $(L, \leq )$ is a totally ordered set with \begin{align} a \leq b : a \wedge b = a \end{align} Implies that $L$ is a Heyting algebra with the Heyting implication \begin{align} a \rightarrow b = \left\{ \begin{array}{l l} \top & \quad a\leq b\\ b & \quad \text{else} \end{array} \right. \end{align} I figured that in order to prove it I need to prove that the implication satisfies

\begin{align} (x \wedge a) \leq b \Leftrightarrow x \leq ( a \rightarrow b) \end{align} However I seem to get stuck.

• Of course you are absolutely right. I am trying to prove it in coq, so I guess my mind was on a different level. If you create a answer I would be delighted to mark it. – budde Mar 21 '14 at 20:20
• Okay, I'll change my comment to an answer, so the question can be marked answered. By the way, I recently started learning Coq, so if you implement this proof, could you share it? Thanks! – William DeMeo Mar 23 '14 at 15:33
• I will do that :) – budde Mar 24 '14 at 7:52

You are right, according to the definition of Heyting algebra, you must check that the $\Leftrightarrow$ in your last displayed equation holds. This follows from the fact that your lattice is totally ordered, arguing by cases.
For example, suppose $x\wedge a \leq b$.
If $a\leq b$, then $a \rightarrow b$ is top, so it is certainly above $x$. If not $a \leq b$, then, since the lattice is totally ordered, $b< a$. This and $x\wedge a \leq b$ imply that $x$ is below $b$, hence $x \leq (a \rightarrow b)$ in this case.
The $\Leftarrow$ direction is similar.