Mathlib Map

Structures · Order

OrderTop

An order is an OrderTop if it has a greatest element. We state this using a data mixin, holding the value of ⊤ and the greatest element constraint.

Defined in
Mathlib.Order.BoundedOrder.Basic
Shape
One type argument · adds le_top
Open in Mathlib docs

Extends1

Extended by5

Concrete types that are instances53

  • TopCat.carrier
  • ENNReal
  • Filter.Germ
  • NonemptyInterval
  • ENat
  • MeasureTheory.SimpleFunc
  • TopologicalSpace.NonemptyCompacts
  • Tropical
  • AlgebraicGeometry.Scheme.IdealSheafData
  • Associates
  • PrimeSpectrum
  • Ordinal.ToType
  • ArchimedeanClass
  • TopologicalSpace.OpenNhdsOf
  • Partition
  • Finpartition
  • MulArchimedeanClass
  • ClosedSubmodule
  • CategoryTheory.Subobject
  • Order.Ideal
  • StructureGroupoid
  • CategoryTheory.Pretopology
  • OpenSubgroup
  • OpenAddSubgroup
  • ValuationSubring
  • Semiquot
  • DiscreteQuotient
  • TopHom
  • TopologicalSpace.PositiveCompacts
  • InfHom
  • SupHom
  • Order.PFilter
  • BoxIntegral.Prepartition
  • InfTopHom
  • TopologicalSpace.OpenNhds
  • CategoryTheory.GrothendieckTopology.Cover
  • sInfHom
  • SemilatInfCat.X
  • Subtype
  • Prod
  • OrderDual
  • Set.Elem
  • ULift
  • Lex
  • Shrink
  • WithTop
  • WithBot
  • Colex
  • Multiplicative
  • Additive
  • Submodule
  • Set
  • OrderHom

How is a type an instance?

Loading the hierarchy index…

Assumed by578

Ancestors2