Structures · Order
Top
Typeclass for the ⊤ (\top) notation
- Defined in
- Mathlib.Order.Notation
- Shape
- One type argument · adds top
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Every Top is also a
Concrete types that are instances75
- ENNReal
- Filter.Germ
- ENat
- EReal
- TopologicalSpace.NonemptyCompacts
- Tropical
- UpperSet
- LowerSet
- LieSubalgebra
- LieSubmodule
- Associates
- TopologicalSpace.Compacts
- AddSubgroup
- AddSubmonoid
- Sublattice
- BooleanSubalgebra
- UniformSpace
- SimpleGraph.Subgraph
- SubMulAction
- TopologicalSpace.Clopens
- TwoSidedIdeal
- HomogeneousIdeal
- SimpleGraph.Finsubgraph
- Class
- NonUnitalSubring
- NonUnitalSubsemiring
- Nucleus
- SubAddAction
- SaturatedAddSubmonoid
- AddSubsemigroup
- SaturatedSubmonoid
- TopologicalSpace.CompactOpens
- CategoryTheory.Subgroupoid
- FirstOrder.Language.Substructure
- DividedPowers.SubDPIdeal
- AbstractSimplicialComplex
- PreAbstractSimplicialComplex
- MeasureTheory.Filtration
- FirstOrder.Language.DefinableSet
- CategoryTheory.Precoverage
- Ideal.Filtration
- GroupTopology
- AddGroupTopology
- OpenSubgroup
- OpenAddSubgroup
- Heyting.Regular
- Booleanisation
- ValuationSubring
- ClopenUpperSet
- FirstOrder.Language.ElementarySubstructure
- TopologicalSpace.PositiveCompacts
- InfHom
- SupHom
- CompleteSublattice
- sInfHom
- FirstOrder.Language.BoundedFormula
- CategoryTheory.MonoOver
- WideSubquiver
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- Shrink
- WithTop
- WithBot
- Submodule
- Filter
- Subgroup
- OrderHom
- Subfield
- Submonoid
- Subring
- Subsemiring
- Subsemigroup
How is a type an instance?
Loading the hierarchy index…
Assumed by132
- Top.top
- InfTopHom.comp
- TopHom.comp
- InfTopHom.id
- InfTopHom.toInfHom
- TopHom.id
- InfTopHom.dual
- WithBot.coe_top
- Pi.top_def
- dite_ne_top
- InfTopHom.copy
- TopHom.copy
- TopHomClass.toTopHom
- InfTopHom.toTopHom
- Equiv.top
- InfTopHom.comp_apply
- TopHom.toFun
- TopHom.comp_apply
- InfTopHom.coe_top
- InfTopHom.instMin
- Function.Injective.generalizedHeytingAlgebra
- InfTopHom.coe_toTopHom
- TopHom.instFunLike
- WithBot.coe_eq_top
- Function.Injective.completeBooleanAlgebra
- Pi.instTopForall
- TopHom.coe_sup
- Tropical.instZeroTropical
- TopHom.instTopHomClass
- Prod.fst_top
- WithBot.instTop
- OrderDual.instBotOfTop
- OrderDual.ofDual_bot
- Prod.instTop
- Function.Injective.heytingAlgebra
- TopHom.sup_apply
- InfHom.coe_top
- TopHom.instMax
- Function.Injective.booleanAlgebra
- Equiv.top_def
- TopHom.instSemilatticeSup
- SupHom.coe_top
- InfTopHom.coe_mk
- top_nonempty
- InfTopHom.toFun_eq_coe
- OrderTop.lift
- InfTopHom.coe_comp
- Function.Injective.completelyDistribLattice
- equivShrink_top
- OrderDual.toDual_top