Structures · Lean core

Std.IsPreorder

This typeclass states that the order structure on α, represented by an LE α instance, is a preorder. In other words, the less-or-equal relation is reflexive and transitive.

Defined in: Init.Data.Order.Classes
Shape: One type argument · adds le_refl, le_trans

Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by3

Std.IsLinearPreorder
Std.IsPartialOrder
Std.PreorderPackage

Concrete types that are instances5

Nat
Dyadic
Lean.Grind.Ring.OfSemiring.Q
Lean.Grind.IntModule.OfNatModule.Q
Subtype

How is a type an instance?

Loading the hierarchy index…

Assumed by0

No theorem or definition in Mathlib takes this class as a hypothesis.

Ancestors0

No ancestors.