Commit 2022-08-24 18:34 96ed4226

feat(order/heyting_algebra): Heyting algebras (#15305) Define (generalized) Heyting, co-Heyting and bi-Heyting algebras. No lemma has been renamed, even though this might look like so from the diff. himp is now a field of boolean_algebra, with default value λ x y, y ⊔ xᶜ.

Duplicated lemmas

Those lemmas have been duplicated because they are true for Heyting algebras but are also used to prove that Boolean algebras are Heyting algebras:

• sdiff_le'
• inf_compl_eq_bot'

Changes to argument implicitness

• sdiff_inf_self_left
• sdiff_inf_self_right