Structures · Order
Compl
Set / lattice complement
- Defined in
- Mathlib.Order.Notation
- Shape
- One type argument · adds compl
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances16
- SimpleGraph
- Digraph
- SubMulAction
- TopologicalSpace.Clopens
- SimpleGraph.Finsubgraph
- Class
- SubAddAction
- TopologicalSpace.CompactOpens
- FirstOrder.Language.DefinableSet
- Heyting.Regular
- Booleanisation
- DFA
- Subtype
- Prod
- ULift
- Set
How is a type an instance?
Loading the hierarchy index…
Assumed by23
- Compl.compl
- Heyting.IsRegular
- Heyting.IsRegular.eq
- Equiv.compl
- Prod.instCompl
- Function.Injective.completeBooleanAlgebra
- Function.Injective.heytingAlgebra
- Function.Injective.booleanAlgebra
- Pi.compl_apply
- fst_compl
- Equiv.compl_def
- ULift.up_compl
- Function.Injective.completelyDistribLattice
- Pi.instCompl
- ULift.instCompl
- ULift.down_compl
- Function.Injective.completeAtomicBooleanAlgebra
- Function.Injective.frame
- Function.Injective.biheytingAlgebra
- Function.Injective.completeDistribLattice
- Heyting.IsRegular.decidablePred
- Pi.compl_def
- snd_compl
Ancestors0
No ancestors.