Theorems · Definition · order theory

List.Shortlex

{α : Type u_1} → (α → α → Prop) → List α → List α → Prop

Given a relation r on α, the shortlex order on List α, for which [a0, ..., an] < [b0, ..., b_k] if n < k or n = k and [a0, ..., an] < [b0, ..., bk] under the lexicographic order induced by r.

Defined in

Mathlib.Data.List.Shortlex

Cited by

13 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms