Structures · Order
InfHomClass
InfHomClass F α β states that F is a type of ⊓-preserving morphisms.
You should extend this class when you extend InfHom.
- Defined in
- Mathlib.Order.Hom.Lattice
- Shape
- 3 explicit arguments · adds map_inf
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Concrete types that are instances1
- InfHom
How is a type an instance?
Loading the hierarchy index…
Assumed by13
Ancestors0
No ancestors.