Distributivity of a Heyting algebra (source code)

= Distributivity of a Heyting algebra

In a <Heyting algebra>, meet with a fixed element is left adjoint to Heyting implication, so it preserves joins:
$$
a\wedge(b\vee c)=(a\wedge b)\vee(a\wedge c).
$$
The dual distributive law follows from this one by the lattice absorption laws.