Structures · Order
BotHomClass
BotHomClass F α β states that F is a type of ⊥-preserving morphisms.
You should extend this class when you extend BotHom.
- Defined in
- Mathlib.Order.Hom.Bounded
- Shape
- 3 explicit arguments · adds map_bot
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- BotHom
How is a type an instance?
Loading the hierarchy index…
Assumed by6
Ancestors0
No ancestors.