Structures · Order
HNot
Syntax typeclass for Heyting negation ￢.
The difference between Compl and HNot is that the former belongs to Heyting algebras,
while the latter belongs to co-Heyting algebras. They are both pseudo-complements, but compl
underestimates while HNot overestimates. In Boolean algebras, they are equal.
See hnot_eq_compl.
- Defined in
- Mathlib.Order.Notation
- Shape
- One type argument · adds hnot
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances3
- SimpleGraph.Finsubgraph
- Prod
- Filter
How is a type an instance?
Loading the hierarchy index…
Assumed by15
- HNot.hnot
- Equiv.hnot
- fst_hnot
- Pi.hnot_apply
- Pi.hnot_def
- Function.Injective.completelyDistribLattice
- Function.Injective.completeAtomicBooleanAlgebra
- Prod.instHNot
- snd_hnot
- Equiv.hnot_def
- Function.Injective.coframe
- Function.Injective.biheytingAlgebra
- Function.Injective.completeDistribLattice
- Function.Injective.coheytingAlgebra
- Pi.instHNot
Ancestors0
No ancestors.