Commit 2022-08-24 18:34 96ed4226
View on Github →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