Structures · Order
Preorder
A preorder is a reflexive, transitive relation ≤.
In a preorder, a < b means a ≤ b ∧ ¬b ≤ a, and < is defined this way by default.
You can override this definition to set a better def-eq.
- Defined in
- Mathlib.Order.Defs.PartialOrder
- Shape
- One type argument · adds le_refl, le_trans, lt_iff_le_not_ge
Extends2
Extended by1
Forgetful instances
Every Preorder is also a
Concrete types that are instances66
- Nat
- Real
- Rat
- TopCat.carrier
- Filter.Germ
- WithVal
- NonemptyInterval
- ENat
- Units
- MeasureTheory.SimpleFunc
- Finsupp
- Zsqrtd
- Interval
- AddUnits
- DFinsupp
- CauSeq
- Tropical
- CategoryTheory.PreZeroHypercover.I₀
- MeasureTheory.AEEqFun
- Associates
- WithTopology
- ValuativeRel.WithPreorder
- OrderRingHom
- MulArchimedeanOrder
- ArchimedeanOrder
- OrderType
- NONote
- DyckWord
- ONote
- Booleanisation
- PSet
- Topology.WithUpper
- Topology.WithLower
- PFun
- TopHom
- BotHom
- SSet.N
- Topology.WithScott
- Topology.WithUpperSet
- Topology.WithLawson
- Topology.WithLowerSet
- CategoryTheory.GrothendieckTopology.Cover
- CategoryTheory.ThinSkeleton
- ContinuousOrderHom
- AlgebraicGeometry.Scheme.AffineZariskiSite
- SSet.S
- Order.PartialIso
- Specialization
- Preord.carrier
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Lex
- AddOpposite
- Shrink
- WithTop
- WithBot
- Sum
- Multiplicative
- Additive
- Sigma
- WithZero
- Quotient
- OrderHom
How is a type an instance?
Loading the hierarchy index…
Assumed by9,289
- LE.le.trans
- Filter.atTop
- LT.lt.le
- le_refl
- Set.Icc
- le_rfl
- Set.Ioi
- LT.lt.ne'
- Monotone
- Set.Ioo
- le_of_lt
- Set.Iio
- Set.Iic
- Set.Ici
- le_trans
- Set.Ioc
- LT.lt.ne
- Set.Ico
- LE.le.trans_lt
- StrictMono
- LT.lt.trans_le
- add_le_add
- ne_of_gt
- Order.succ
- Eq.le
- le_imp_le_of_le_of_le
- Antitone
- CategoryTheory.homOfLE
- Filter.atBot
- Finset.Ico
- lt_of_lt_of_le
- lt_of_le_of_lt
- mul_nonneg
- Eq.ge
- mul_pos
- LT.lt.trans
- le_of_eq
- mul_le_mul_of_nonneg_left
- Finset.Icc
- MonotoneOn
- LT.lt.not_ge
- mul_le_mul_of_nonneg_right
- Finset.Ioc
- Finset.Iic
- mul_le_mul'
- Order.pred
- AntitoneOn
- GaloisConnection
- StrictAnti
- ne_of_lt