Structures · Order
GeneralizedHeytingAlgebra
A generalized Heyting algebra is a lattice with an additional binary operation ⇨ called
Heyting implication such that (a ⇨ ·) is right adjoint to (a ⊓ ·).
This generalizes HeytingAlgebra by not requiring a bottom element.
- Defined in
- Mathlib.Order.Heyting.Basic
- Shape
- One type argument · adds le_himp_iff
Extends3
Extended by1
Forgetful instances
Every GeneralizedHeytingAlgebra is also a
Concrete types that are instances2
- Prod
- OrderDual
How is a type an instance?
Loading the hierarchy index…
Assumed by77
- le_himp_iff
- bihimp_comm
- himp_self
- himp_inf_le
- le_himp
- himp_eq_top_iff
- Codisjoint.himp_eq_right
- himp_le_himp_left
- le_himp_iff'
- inf_le_bihimp
- himp_himp
- himp_inf_distrib
- sup_himp_distrib
- himp_inf_self
- bihimp_top
- bihimp_self
- inf_himp
- inf_himp_le
- sup_himp_self_left
- isGreatest_himp
- bihimp_inf_sup
- himp_le_himp_right
- Codisjoint.himp_eq_left
- top_himp
- bihimp_triangle
- himp_top
- top_bihimp
- le_bihimp_inf_right
- himp_idem
- himp_bihimp
- GeneralizedHeytingAlgebra.le_himp_iff
- bihimp_himp_eq_inf
- sup_himp_self_right
- himp_bihimp_eq_inf
- bihimp_bihimp_sup
- le_himp_comm
- gc_inf_himp
- himp_eq_himp_iff
- le_himp_himp
- himp_triangle
- sup_himp_bihimp
- himp_le_himp_himp_himp
- himp_left_comm
- Function.Injective.generalizedHeytingAlgebra
- himp_ne_himp_iff
- sup_inf_bihimp
- ofDual_symmDiff
- bihimp_snd
- Codisjoint.bihimp_eq_inf
- le_bihimp_iff