Theorems · Inductive type · order theory
GeneralizedHeytingAlgebra
Type u_4 → Type u_4
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
- Cited by
- 68 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by85
Results whose statement or proof uses this declaration.
- le_himp_iffstatement and proof · cited by 19
- bihimp_commstatement and proof · cited by 8
- himp_inf_lestatement and proof · cited by 6
- himp_selfstatement and proof · cited by 6
- le_himpstatement and proof · cited by 5
- himp_eq_top_iffstatement and proof · cited by 5
- Codisjoint.himp_eq_rightstatement and proof · cited by 4
- le_himp_iff'statement and proof · cited by 4
- himp_le_himp_leftstatement and proof · cited by 4
- bihimp_topstatement and proof · cited by 3
- inf_le_bihimpstatement and proof · cited by 3
- sup_himp_distribstatement and proof · cited by 3