Structures · Order
InfTopHomClass
InfTopHomClass F α β states that F is a type of finitary infimum-preserving morphisms.
You should extend this class when you extend SupBotHom.
- Defined in
- Mathlib.Order.Hom.BoundedLattice
- Shape
- 3 explicit arguments · adds map_top
Extends1
Extended by1
Concrete types that are instances1
- InfTopHom
How is a type an instance?
Loading the hierarchy index…
Assumed by10
- map_finset_inf
- Set.map_finite_biInf
- CategoryTheory.Limits.CompleteLattice.preservesLimitsOfShape_finite_toFunctor
- Set.map_finite_iInf
- instCoeTCInfTopHomOfInfTopHomClass
- CategoryTheory.Limits.CompleteLattice.instPreservesFiniteLimitsToFunctorToOrderHom
- CategoryTheory.Limits.CompleteLattice.preservesLimit_finite_toFunctor
- InfTopHomClass.toTopHomClass
- InfTopHomClass.map_top
- InfTopHomClass.toInfHomClass