Structures · Lean core

Std.LinearOrderPackage

This class entails LE α, LT α, BEq α, Ord α, Min α and Max α instances as well as proofs that these operations represent the same linear order structure on α.

Defined in: Init.Data.Order.PackageFactories
Shape: One type argument · adds le_antisymm

Open in Mathlib docs

Extends7

Std.LinearPreorderPackage
Std.PartialOrderPackage
Min
Max
Std.LawfulOrderMin
Std.LawfulOrderMax
Std.IsLinearOrder

Extended by0

Nothing extends this class yet.

Concrete types that are instances3

String.Pos.Raw
String.Slice.Pos
String.Pos

How is a type an instance?

Loading the hierarchy index…

Assumed by0