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