Theorems · Inductive type · order theory
CoheytingAlgebra
Type u_4 → Type u_4
A co-Heyting algebra is a bounded lattice with an additional binary difference operation \
such that (· \ a) is left adjoint to (· ⊔ a).
- Defined in
- Mathlib.Order.Heyting.Basic
- Cited by
- 96 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 by128
Results whose statement or proof uses this declaration.
- Coheyting.boundarystatement and proof · cited by 24
- CoheytingHomstatement · cited by 20
- top_sdiff'statement and proof · cited by 13
- hnot_le_iff_codisjoint_leftstatement and proof · cited by 8
- hnot_le_iff_codisjoint_rightstatement and proof · cited by 7
- codisjoint_hnot_leftstatement and proof · cited by 7
- codisjoint_hnot_rightstatement and proof · cited by 7
- CoheytingHom.compstatement and proof · cited by 7
- hnot_antistatement and proof · cited by 7
- hnot_inf_distribstatement and proof · cited by 6
- CoheytingHom.extstatement and proof · cited by 5
- hnot_le_commstatement and proof · cited by 4