Structures · Order
BiheytingAlgebra
A bi-Heyting algebra is a Heyting algebra that is also a co-Heyting algebra.
- Defined in
- Mathlib.Order.Heyting.Basic
- Shape
- One type argument · adds sdiff_le_iff, top_sdiff
Extends2
Extended by4
Forgetful instances
Provided automatically by
Concrete types that are instances4
- Prod
- OrderDual
- Fin
- PUnit
How is a type an instance?
Loading the hierarchy index…
Assumed by39
- BiheytingHom.comp
- BiheytingHom.toLatticeHom
- BiheytingHom.id
- BiheytingAlgebra.toSDiff
- BiheytingHom.copy
- BiheytingHom.comp_apply
- BiheytingAlgebra.toHNot
- BiheytingAlgebra.sdiff_le_iff
- BiheytingHom.map_himp'
- BiheytingHom.copy_eq
- Prod.instBiheytingAlgebra
- BiheytingHomClass.toHeytingHomClass
- BiheytingAlgebra.toHeytingAlgebra
- BiheytingHom.comp_id
- BiheytingHom.toFun_eq_coe_aux
- Pi.instBiheytingAlgebra
- OrderIsoClass.toBiheytingHomClass
- BiheytingAlgebra.top_sdiff
- BiheytingHom.cancel_right
- BiheytingHom.comp_assoc
- BiheytingHom.coe_copy
- BiheytingHom.map_sdiff'
- BiheytingHom.instInhabited
- BiheytingHom.coe_id
- BiheytingHom.id_comp
- BiheytingHom.instFunLike
- BiheytingHom.instPartialOrder
- BiheytingAlgebra.toCoheytingAlgebra
- BiheytingHom.instBiheytingHomClass
- instCoeTCBiheytingHomOfBiheytingHomClass
- compl_le_hnot
- Function.Injective.biheytingAlgebra
- BiheytingHomClass.toCoheytingHomClass
- BiheytingHom.coe_comp
- Equiv.biheytingAlgebra
- BiheytingHom.cancel_left
- BiheytingHom.id_apply
- OrderDual.instBiheytingAlgebra
- BiheytingHom.toFun_eq_coe