Mathlib Map

Structures · Order

LinearOrder

A linear order is reflexive, transitive, antisymmetric and total relation ≤. We assume that every linear ordered type has decidable (≤), (<), and (=).

Defined in
Mathlib.Order.Defs.LinearOrder
Shape
One type argument · adds le_total, toDecidableLE, toDecidableEq, toDecidableLT, min_def, max_def, compare_eq_compareOfLessAndEq
Open in Mathlib docs

Extends4

Extended by5

Forgetful instances

Every LinearOrder is also a

Provided automatically by

Concrete types that are instances68

  • Int
  • Nat
  • Real
  • Rat
  • Bool
  • NNReal
  • ENNReal
  • Filter.Germ
  • NNRat
  • ENat
  • Units
  • EReal
  • Hyperreal
  • ArchimedeanClass.FiniteResidueField
  • Zsqrtd
  • ZNum
  • Localization
  • ArchimedeanClass.FiniteElement
  • AddUnits
  • PNat
  • Tropical
  • Ordinal
  • Empty
  • UpperSet
  • LowerSet
  • Cardinal
  • PEmpty
  • Num
  • SignType
  • Ordinal.ToType
  • Char
  • ArchimedeanClass
  • String
  • WithTopology
  • ValuativeRel.ValueGroupWithZero
  • ValuationRing.ValueGroup
  • PosNum
  • DedekindCut
  • MulArchimedeanClass
  • AddLocalization
  • MonomialOrder.syn
  • Antisymmetrization
  • DegLex
  • NONote
  • LinOrd.carrier
  • Topology.WithUpper
  • Topology.WithLower
  • LinearExtension
  • DivisibleHull
  • WellOrderExtension
  • Profinite.NobelingProof.Products
  • OrderType.ToType
  • Subtype
  • OrderDual
  • ULift
  • Fin
  • PUnit
  • Lex
  • Shrink
  • WithTop
  • WithBot
  • Colex
  • Multiplicative
  • List
  • Additive
  • WithZero
  • Ideal
  • Quotient

How is a type an instance?

Loading the hierarchy index…

Assumed by9,501

Ancestors15