Structures · Order
GeneralizedCoheytingAlgebra
A generalized co-Heyting algebra is a lattice with an additional binary
difference operation \ such that (· \ a) is left adjoint to (· ⊔ a).
This generalizes CoheytingAlgebra by not requiring a top element.
- Defined in
- Mathlib.Order.Heyting.Basic
- Shape
- One type argument · adds sdiff_le_iff
Extends3
Extended by2
Forgetful instances
Every GeneralizedCoheytingAlgebra is also a
Provided automatically by
Concrete types that are instances3
- SimpleGraph.Finsubgraph
- Prod
- OrderDual
How is a type an instance?
Loading the hierarchy index…
Assumed by104
- sdiff_self
- sdiff_le
- symmDiff_comm
- sdiff_le_iff'
- Disjoint.sdiff_eq_left
- sdiff_le_sdiff
- sdiff_bot
- sdiff_idem
- sdiff_le_sdiff_right
- sdiff_eq_bot_iff
- sup_sdiff_self
- sdiff_le_iff
- symmDiff_eq_sup_sdiff_inf
- sup_sdiff
- symmDiff_self
- le_sdiff_sup
- sdiff_sup_cancel
- sdiff_le_sdiff_left
- sdiff_sup_self
- Disjoint.sdiff_eq_right
- sup_sdiff_right_self
- sup_sdiff_cancel_right
- sdiff_inf
- symmDiff_triangle
- Disjoint.sup_sdiff_cancel_right
- sdiff_inf_self_left
- bot_sdiff
- le_sup_sdiff
- sup_sdiff_distrib
- sup_sdiff_left_self
- sdiff_sdiff_self
- sdiff_sdiff_comm
- sdiff_inf_distrib
- symmDiff_bot
- sdiff_inf_self_right
- symmDiff_of_le
- symmDiff_le_sup
- sdiff_right_comm
- sup_sdiff_eq_sup
- sdiff_triangle
- sup_sdiff_self_right
- sdiff_le_comm
- sdiff_sdiff
- sdiff_sup_sdiff_cancel
- sdiff_sdiff_left
- sup_sdiff_cancel'
- Disjoint.symmDiff_eq_sup
- sdiff_sdiff_sdiff_le_sdiff
- symmDiff_sdiff
- inf_sdiff_sup_right