Theorems · Definition · order theory

Ordering.Compares

{α : Type u_1} → [LT α] → Ordering → α → α → Prop

Compares o a b means that a and b have the ordering relation o between them, assuming that the relation a < b is defined.

Defined in

Mathlib.Data.Ordering.Basic

Cited by

31 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

LT