Structures · Order
CoheytingAlgebra
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
- Shape
- One type argument · adds top_sdiff
Extends3
Extended by2
Concrete types that are instances3
- Prod
- OrderDual
- Fin
How is a type an instance?
Loading the hierarchy index…
Assumed by110
- Coheyting.boundary
- top_sdiff'
- hnot_le_iff_codisjoint_left
- codisjoint_hnot_left
- hnot_le_iff_codisjoint_right
- hnot_anti
- codisjoint_hnot_right
- CoheytingHom.comp
- hnot_inf_distrib
- CoheytingHom.toLatticeHom
- CoheytingHom.id
- sdiff_top
- hnot_hnot_le
- hnot_le_comm
- hnot_hnot_hnot
- Coheyting.hnot_boundary
- hnot_symmDiff_self
- le_hnot_self
- CoheytingHom.copy
- CoheytingAlgebra.top_sdiff
- sup_hnot_self
- Coheyting.boundary_le_boundary_sup_sup_boundary_inf_left
- Coheyting.boundary_boundary
- Coheyting.hnot_hnot_sup_boundary
- hnot_top
- Codisjoint.hnot_le_left
- hnot_sup_self
- Coheyting.boundary_sup_le
- ne_hnot_self
- top_symmDiff
- symmDiff_top
- IsCompl.eq_hnot
- Coheyting.inf_hnot_self
- codisjoint_hnot_hnot_left_iff
- sdiff_le_hnot
- Codisjoint.hnot_le_right
- CoheytingHom.comp_apply
- hnot_sdiff_comm
- hnot_sdiff
- hnot_hnot_sup_distrib
- Coheyting.boundary_le_boundary_sup_sup_boundary_inf_right
- le_hnot_inf_hnot
- symmDiff_hnot_self
- Coheyting.boundary_le
- isLeast_hnot
- Coheyting.boundary_inf
- Coheyting.boundary_inf_le
- CoheytingHom.instPartialOrder
- toDual_hnot
- CoheytingHom.toFun_eq_coe