Co-Heyting algebra

Remarks

The operation is unique when it exists, since it is a least element. A bounded lattice is a co-Heyting algebra if and only if its order dual is a Heyting algebra. The element $\neg a = 1 \setminus a$ is called the supplement of $a$; it is the least $c$ with $a \vee c = 1$.

Example: let $X$ be a topological space and $L$ its family of closed sets, ordered by inclusion. For closed $A, B$, put $A \setminus B = \overline{A - B}$, the closure of the set difference. If $A \subseteq B \cup C$ with $C$ closed, then $A - B \subseteq C$, so $\overline{A - B} \subseteq C$. If $\overline{A - B} \subseteq C$, then $A \subseteq B \cup (A - B) \subseteq B \cup C$. So the defining equivalence holds.

Non-example: the diamond lattice $M_3$, with atoms $p, q, r$, is bounded but has no such operation. Every co-Heyting algebra is distributive, and $M_3$ is not, since $p \vee (q \wedge r) = p$ while $(p \vee q) \wedge (p \vee r) = 1$. Directly: the elements $c$ with $1 \le p \vee c$ are $q$, $r$ and $1$, and they have no least one.

In Mathlib the notion is CoheytingAlgebra, with difference \ and supplement ￢.