Structures · Order
HeytingAlgebra
A Heyting algebra is a bounded lattice with an additional binary operation ⇨ called Heyting
implication such that (a ⇨ ·) is right adjoint to (a ⊓ ·).
- Defined in
- Mathlib.Order.Heyting.Basic
- Shape
- One type argument · adds himp_bot
Extends3
Extended by2
Concrete types that are instances6
- Nucleus
- HeytAlg.carrier
- Subtype
- Prod
- OrderDual
- Fin
How is a type an instance?
Loading the hierarchy index…
Assumed by136
- disjoint_compl_right
- disjoint_compl_left
- IsCompl.compl_eq
- compl_le_compl
- Heyting.Regular.val
- Heyting.Regular
- le_compl_iff_disjoint_right
- HeytAlg.of
- himp_bot
- HeytingHom.comp
- compl_sup
- HeytAlg.ofHom
- compl_anti
- compl_bot
- le_compl_iff_disjoint_left
- HeytingHom.id
- LE.le.disjoint_compl_right
- compl_sup_distrib
- compl_top
- inf_compl_eq_bot
- IsCompl.eq_compl
- le_compl_comm
- HeytingHom.toLatticeHom
- compl_compl_compl
- Disjoint.le_compl_left
- Disjoint.le_compl_right
- le_compl_iff_le_compl
- bot_himp
- le_compl_self
- inf_compl_self
- le_compl_compl
- Heyting.Regular.toRegular
- map_compl
- compl_compl_inf_distrib
- compl_le_himp
- HeytingHom.copy
- compl_bihimp_self
- LE.le.disjoint_compl_left
- disjoint_compl_compl_left_iff
- compl_compl_himp_distrib
- lt_compl_self
- compl_inf_self
- Heyting.Regular.coe_injective
- HeytingHom.comp_apply
- bihimp_compl_self
- compl_unique
- HeytingAlgebra.himp_bot
- compl_inf_eq_bot
- ne_compl_self
- himp_compl