Theorems · Inductive type · order theory
HeytingAlgebra
Type u_4 → Type u_4
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
- Cited by
- 108 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · 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 by156
Results whose statement or proof uses this declaration.
- disjoint_compl_rightstatement and proof · cited by 47
- HeytingHomstatement · cited by 45
- disjoint_compl_leftstatement and proof · cited by 17
- IsCompl.compl_eqstatement and proof · cited by 16
- compl_le_complstatement and proof · cited by 14
- Heyting.Regularstatement and proof · cited by 14
- Heyting.Regular.valstatement and proof · cited by 14
- le_compl_iff_disjoint_rightstatement and proof · cited by 10
- HeytAlg.ofstatement and proof · cited by 9
- HeytingHom.compstatement and proof · cited by 9
- himp_botstatement and proof · cited by 9
- compl_antistatement and proof · cited by 8